![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Entry tags:
Formulae-as-Types for an Involutive Negation
https://hal.inria.fr/hal-00996742v1/document
Negation is not involutive in the ππ calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access to the stacks studied by Felleisen and Clements.
We introduce polarised, untyped, calculi compatible with exten- sionality, for both of classical sequent calculus and classical natural deduction, with connectives for an involutive negation. The invol- ution is due to the l delimited control operator that we introduce, which allows us to implement the idea that captured stacks, unlike continuations, can be inspected. Delimiting control also gives a con- structive interpretation to falsity. We describe the isomorphism there is between π΄ and ¬¬π΄, and thus between Β¬β and βΒ¬.
One way to provide constructive contents to classical proofs is by considering variants of the GΓΆdel-Gentzen double-negation translations, such as Friedmanβs [13]. We can translate classical proofs of β’ π into intuitionistic proofs of β’ (πβ² β π ) β π , where πβ² is the translation of π and where π is chosen arbitrarily. When π is purely positive, then π β² does not depend on π and, furthermore, we have πβ² = π. Therefore, in this special case we can take π = π and deduce an intuitionistic proof of β’ (π β π ) β π and, in turn, one of β’ π . In the other cases, the translation describes in fact how the behaviour of classical proofs depends on the context in which classical axioms are invoked. Thus the interpretation does not contradict intuitionism: the latter assumes that the behaviour of proofs is referentially transparent, while here we do not make such an assump- tion. This is why proofs of βπ΄, π΄ β¨ Β¬π΄ do not provide a decision procedure for π΄ in general.
As we will see, the computational contents of the De Morgan law is as simple to understand as: 1) capturing the stack of the form πβ π that appears during the head reduction of the argument; 2) decomposing it into head and tail, and return a pair (π, ππ ) where ππ is the captured form of the tail. This contrasts with the proof in the ππ cal- culus, which is convoluted because captured contexts are identified with continuations. By continuation we mean the functional abstrac- tion of the remainder of a computation. Thus, the contents of the captured context, which is represented by a functional value, cannot be accessed in an immediate way.
Negation is not involutive in the ππ calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access to the stacks studied by Felleisen and Clements.
We introduce polarised, untyped, calculi compatible with exten- sionality, for both of classical sequent calculus and classical natural deduction, with connectives for an involutive negation. The invol- ution is due to the l delimited control operator that we introduce, which allows us to implement the idea that captured stacks, unlike continuations, can be inspected. Delimiting control also gives a con- structive interpretation to falsity. We describe the isomorphism there is between π΄ and ¬¬π΄, and thus between Β¬β and βΒ¬.
One way to provide constructive contents to classical proofs is by considering variants of the GΓΆdel-Gentzen double-negation translations, such as Friedmanβs [13]. We can translate classical proofs of β’ π into intuitionistic proofs of β’ (πβ² β π ) β π , where πβ² is the translation of π and where π is chosen arbitrarily. When π is purely positive, then π β² does not depend on π and, furthermore, we have πβ² = π. Therefore, in this special case we can take π = π and deduce an intuitionistic proof of β’ (π β π ) β π and, in turn, one of β’ π . In the other cases, the translation describes in fact how the behaviour of classical proofs depends on the context in which classical axioms are invoked. Thus the interpretation does not contradict intuitionism: the latter assumes that the behaviour of proofs is referentially transparent, while here we do not make such an assump- tion. This is why proofs of βπ΄, π΄ β¨ Β¬π΄ do not provide a decision procedure for π΄ in general.
As we will see, the computational contents of the De Morgan law is as simple to understand as: 1) capturing the stack of the form πβ π that appears during the head reduction of the argument; 2) decomposing it into head and tail, and return a pair (π, ππ ) where ππ is the captured form of the tail. This contrasts with the proof in the ππ cal- culus, which is convoluted because captured contexts are identified with continuations. By continuation we mean the functional abstrac- tion of the remainder of a computation. Thus, the contents of the captured context, which is represented by a functional value, cannot be accessed in an immediate way.