PFPL Chapter 13 Classical Logic

Posted on In Disqus:

The part is not shown on PFPL preview version.

From Constructive Logic to Classical Logic

Constructive logic is a logic of positive evidence, as stated in last chapter.

In contrast, classical logic is a logic of perfect information where every proposition is either true or false.

This casts a “god’s view” of the world, where there are no open problems, all propositions converge to a result. The symmetry between truth and falsity is appealing, but the logical connectives are weaker in classical case.

In Exercise 12.1 for LEM, LEM is not universally valid. It is valid only under classical case.

Constructive logic is stronger (more expressive) than classical logic since it can express more distinctions (between affirmation and irrefutability) and it is consistent with classical logic.

A proof in classical logic is a computation that cannot be refuted.

Computationally, a refutation consists of a continuation, or control stack, that takes a proof of proposition and derives a contradiction. A proof in classical logic is a computation that, when given a refutation of that proposition derives a contradiction, witnessing the impossibility of refuting it.

Classical Logic

The connective in classical logic is defined by giving its truth and falsity conditions.

The truth rules correspond to introduction, falsity rules correspond to elimination (view Proof and Refutations syntax). The symmetry between is expressed by the principle of indirect proof.

To show $\phi \text{ true}$ it is enough to show $\phi \text{ false}$ entails a contradiction and conversely, to show $\phi \text{ false}$ it is enough to show $\phi\text{ true}$ leads to contradiction.

The first one is fundamentally classical, expressing the principle of indirect proof.

Provability and Refutability

Three basic judgment forms in classical logic:

  • $\phi \text{ true}$ for proposition $\phi$ is provable.
  • $\phi \text{ false}$ for proposition $\phi$ is refutable.
  • # states that a contradiction has been derived.

These are extended to hypothetical judgments in which we admit both provability and refutability assumptions:
$$
\phi_1\text{ false},\dots,\phi_m\text{ false},\psi_1\text{ true},\dots,\psi_n\text{ true}\vdash J
$$
The hypotheses are divided into $\Delta$ for falsity assumptions and $\Gamma$ for truth assumptions.

The rules of classical logic are organized around the symmetry between truth and falsity, which is mediated by contradiction judgments.

The hypothetical judgment is reflexive as:
$$
\displaylines{\dfrac{}{\Delta,\phi\text{ false }\Gamma\vdash \phi\text{ false}}\\
\dfrac{}{\Delta\space\Gamma,\phi\text{ true}\vdash\phi\text{ true}}}
$$
The remaining rule are stated so that structural properties of weakening, transitivity, contraction are admissible.

Contradiction

$$
\displaylines{\dfrac{\Delta\space\Gamma\vdash\phi\text{ false}\phantom{“”}\Delta\space\Gamma\vdash\phi\text{ true}}{\Delta\space\Gamma\vdash\sharp}\\
\dfrac{\Delta,\phi\text{ false }\Gamma\vdash \sharp}{\Delta\space\Gamma\vdash\phi\text{ true}}\\
\dfrac{\Delta\space\Gamma,\phi\text{ true}\vdash \sharp}{\Delta\space\Gamma\vdash\phi\text{ false}}}
$$

Truth and Falsity

$$
\displaylines{\dfrac{}{\Delta\space\Gamma\vdash\top\text{ true}}\\
\dfrac{}{\Delta\space\Gamma\vdash\bot\text{ false}}}
$$

Conjunction

$$
\displaylines{\dfrac{\Delta\space\Gamma\vdash\phi_1\text{ true}\phantom{“”}\Delta\space\Gamma\vdash\phi_2\text{ true}}{\Delta\space\Gamma\vdash\phi_1\wedge\phi_2\text{ true}}\\
\dfrac{\Delta\space\Gamma\vdash\phi_1\text{ false}}{\Delta\space\Gamma\vdash\phi_1\wedge \phi_2\text{ false}}\\
\dfrac{\Delta\space\Gamma\vdash\phi_2\text{ false}}{\Delta\space\Gamma\vdash\phi_1\wedge\phi_2\text{ false}}}
$$

Disjunction

$$
\displaylines{\dfrac{\Delta\space\Gamma\vdash\phi_1\text{ true}}{\Delta\space\Gamma\vdash\phi_1\vee\phi_2\text{ true}}\\
\dfrac{\Delta\space\Gamma\vdash\phi_2\text{ true}}{\Delta\space\Gamma\vdash\phi_1\vee\phi_2\text{ true}}\\
\dfrac{\Delta\space\Gamma\vdash\phi_1\text{ false}\phantom{“”}\Delta\space\Gamma\vdash\phi_1\text{ false}}{\Delta\space\Gamma\vdash\phi_1\vee\phi_2\text{ false}}}
$$

Negation

$$
\displaylines{\dfrac{\Delta\space\Gamma\vdash\phi\text{ true}}{\Delta\space\Gamma\vdash\phi\text{ false}}\\
\dfrac{\Delta\space\Gamma\vdash\phi\text{ false}}{\Delta\space\Gamma\vdash\phi\text{ true}}}
$$

Implication

$$
\displaylines{\dfrac{\Delta\space\Gamma,\phi_1\text{ true}\vdash\phi_2\text{ true}}{\Delta\space\Gamma\vdash \phi_1\supset\phi_2\text{ true}}\\
\dfrac{\Delta\space\Gamma\vdash\phi_1\text{ true}\phantom{“”}\Delta\space\Gamma\vdash\phi_2\text{ false}}{\Delta\space\Gamma\vdash\phi_1\supset\phi_2\text{ false}}}
$$

Proofs and Refutations

Introduce explicit syntax for proofs and refutations by defining three hypothetical judgments for classical logic with explicit derivations:

  • $\Delta\space\Gamma \vdash p:\phi$ stating $p$ is a proof of $\phi$.
  • $\Delta\space\Gamma\vdash k \div\phi$ stating $k$ is a refutation of $\phi$.
  • $\Delta\space\Gamma\vdash k\space\sharp\space p$ stating $k$ and $p$ are contradictory.

Falsity assumptions $\Delta$ are given by a context of form $\forall i \in \lbrace1,\dots,n\rbrace, u_i\div \phi_i$ ($u_i$ stands for refutation).

Truth assumptions $\Gamma$ are given by a context of form $\forall i \in\lbrace 1,\dots,m \rbrace,p_i:\psi_i$ ($p_i$ stands for proof).

The syntax of proof and refutation is defined with following grammar table:
$$
\begin{align}
\text{Prf}&&p&&::=&&\text{true-T}&&\langle\rangle&&\text{truth}\\
&&&&&&\text{and-T}(p_1;p_2)&&\langle p_1,p_2\rangle&&\text{contradiction}\\
&&&&&&\text{or-T}\lbrack l\rbrack(p)&&l \cdot p&&\text{disjunction left}\\
&&&&&&\text{or-T}\lbrack r\rbrack(p)&&r \cdot p&&\text{disjunction right}\\
&&&&&&\text{not-T}(k)&&\text{not}(k)&&\text{negation}\\
&&&&&&\text{imp-T}(x.p)&&\lambda(x)p&&\text{implication}\\
&&&&&&\text{ccr}(u.(k\space\sharp\space p))&&\text{ccr}(u.(k\space\sharp\space p))&&\text{contradiction}\\
\text{Ref}&&k&&::=&&\text{false-F}&&\text{abort}&&\text{falsehood}\\
&&&&&&\text{and-F}\lbrack l\rbrack(k)&&\text{fst};k&&\text{conjunction left}\\
&&&&&&\text{and-F}\lbrack r\rbrack(k)&&\text{snd};k&&\text{conjunction right}\\
&&&&&&\text{or-F}(k_1;k_2)&&\text{case}(k_1;k_2)&&\text{disjunction}\\
&&&&&&\text{not-F}(p)&&\text{not}(p)&&\text{negation}\\
&&&&&&\text{imp-F}(p;k)&&\text{ap}(p);k&&\text{implication}\\
&&&&&&\text{ccp}(x.(k\space\sharp\space p))&&\text{ccr}(x.(k\space\sharp\space p))&&\text{contradiction}\\
\end{align}
$$

Contradiction

$$
\displaylines{\dfrac{\Delta,u\div\phi\space\Gamma\vdash k\space\sharp\space p}{\Delta\space\Gamma\vdash\text{ccr}(u.(k\space\sharp\space p)):\phi}\\
\dfrac{\Delta\space\Gamma,x:\phi\vdash k\space\sharp\space p}{\Delta\space\Gamma\vdash\text{ccp}(x.(k\space\sharp\space p))\div\phi}}
$$

Truth and Falsity

$$
\displaylines{\dfrac{}{\Delta\space\Gamma\vdash\langle\rangle:\top}\\
\dfrac{}{\Delta\space\Gamma\vdash\text{abort}\div\bot}}
$$

Conjunction

$$
\displaylines{\dfrac{\Delta\space\Gamma\vdash p_1:\phi_1\phantom{“”}\Delta\space\Gamma\vdash p_2:\phi_2}{\Delta\space\Gamma\vdash\langle p_1,p_2\rangle:\phi_1\wedge\phi_2}\\
\dfrac{\Delta\space\Gamma\vdash k_1\div\phi_1}{\Delta\space\Gamma\vdash\text{fst};k_1\div\phi_1\wedge\phi_2}\\
\dfrac{\Delta\space\Gamma\vdash k_2\div\phi_2}{\Delta\space\Gamma\vdash\text{snd};k_2\div\phi_1\wedge\phi_2}}
$$

Disjunction

$$
\displaylines{\dfrac{\Delta\space\Gamma\vdash p_1:\phi_1}{\Delta\space\Gamma\vdash l\cdot p_1:\phi_1\vee\phi_2}\\
\dfrac{\Delta\space\Gamma\vdash p_2:\phi_2}{\Delta\space\Gamma\vdash r\cdot p_2:\phi_1\vee\phi_2}\\
\dfrac{\Delta\space\Gamma\vdash p_1\div\phi_1\phantom{“”}\Delta\space\Gamma\vdash p_2\div\phi_2}{\Delta\space\Gamma\vdash\text{case}(p_1;p_2)\div\phi_1\vee\phi_2}}
$$

Negation

$$
\displaylines{\dfrac{\Delta\space\Gamma\vdash k\div\phi}{\Delta\space\Gamma\vdash\text{not}(k):\neg\phi}\\
\dfrac{\Delta\space\Gamma\vdash k:\phi}{\Delta\space\Gamma\vdash\text{not}(k)\div\neg\phi}}
$$

Implication

$$
\displaylines{\dfrac{\Delta\space\Gamma,x:\phi_1\vdash p_2:\phi_2}{\Delta\space\Gamma\vdash\lambda(x)p_2:\phi_1\supset\phi_2}\\
\dfrac{\Delta\space\Gamma\vdash p_1:\phi_1\phantom{“”}\Delta\space\Gamma\vdash p_2\div\phi_2}{\Delta\space\Gamma\vdash\text{ap}(p_1);k_2\div\phi_1\supset\phi_2}}
$$

Deriving Elimination Forms

The price for a symmetry between truth and falsity in classical logic is that we must very often rely on the principle of indirect proof: to show a proposition is true, we often must derive a contradiction from assumption of its falsity.

Consider an example proof for $(\phi \wedge (\psi\wedge \theta))\supset(\theta\wedge\phi)$.

In constructive logic the proposition can have a direct proof to avoid circumlocutions of proof by contradiction by
$$
\lambda(w :(\phi\wedge(\psi\wedge\theta)))\langle w\cdot r\cdot r,w\cdot l\rangle
$$

Proof cannot be so expressive as is in classical logic, for classical logic lacks elimination forms of constructive logic.

Continue the previous example in classical logic, we know that “truth rules correspond to introduction, falsity rules correspond to elimination“. Thus we cannot avoid using contradiction to prove thing. The prototype for the proof is like
$$
\lambda(w:(\phi\wedge(\psi\wedge\theta)))\text{ ccr }((u\div(\theta\wedge\phi)) .(k\space\sharp\space w))
$$
where $k$ should be
$$
\text{fst; ccp }(x:\phi.\text{ snd; ccp }(y:(\psi\wedge\theta).\text{ snd; ccp }(z:\theta.u\space\sharp\space\langle z,x\rangle)\space\sharp\space y)\space\sharp\space w)
$$

We may package the use of indirect proof into a slightly more palatable form by deriving elimination rules of constructive logic.

$$
\dfrac{\Delta\space\Gamma\vdash\phi\wedge\psi\text{ true}}{\Delta\space\Gamma\vdash\phi\text{ true}}
$$

is derivable in classical logic
$$
\dfrac{\dfrac{\dfrac{}{\Delta,\phi\text{ false}\space\Gamma\vdash\phi\text{ false}}}{\Delta,\phi\text{ false}\space\Gamma\vdash\phi\wedge\psi\text{ false}}\phantom{“”}\dfrac{\Delta\space\Gamma\vdash\phi\wedge\psi\text{ true}}{\Delta,\phi\text{ false}\space\Gamma\vdash\phi\wedge\psi\text{ true}}}{\dfrac{\Delta,\phi\text{ false}\space\Gamma\vdash\sharp}{\Delta\space\Gamma\vdash\phi\text{ true}}}
$$

The derivation of elimination forms of constructive logic can be exhibited as follows
$$
\begin{align}
\text{abort}(p)&=\text{ccr}(u.(\text{abort}\space\sharp\space p))\\
p\cdot l&= \text{ccr}(u.(\text{fst};u\space\sharp\space p))\\
p\cdot r&= \text{ccr}(u.(\text{snd};u\space\sharp\space p))\\
p_1(p_2)&= \text{ccr}(u.(\text{ap}(p_2);u\space\sharp\space p_1))\\
\text{case }p_1\lbrace l\cdot r\hookrightarrow p_2 \shortmid r\cdot y\hookrightarrow p \rbrace&=\text{ccr}(u.(\text{case}(\text{ccp}(x.(u\space\sharp\space p_2));\text{ccp}(y.(u\space\sharp\space p)))\space\sharp\space p_1))
\end{align}
$$

Proof Dynamics

Dynamics of classical logic arises from simplification of contradiction between a proof and a refutation of a proposition.

The truth and falsity rules for the connectives play off one another in such way
$$
\begin{align}
\text{fst};k\space\sharp\space\langle p_1,p_2\rangle&\longmapsto k\space\sharp\space p_1\\
\text{snd};k\space\sharp\space\langle p_1,p_2\rangle&\longmapsto k\space\sharp\space p_2\\
\text{case}(k_1;k_2)\space\sharp\space l\cdot p_1&\longmapsto k_1\space\sharp\space p_1\\
\text{case}(k_1;k_2)\space\sharp\space r\cdot p_2&\longmapsto k_2\space\sharp\space p_2\\
\text{not}(p)\space\sharp\space\text{not}(k)&\longmapsto p\space\sharp\space k\\
\text{ap}(p_1);k\space\sharp\space\lambda(x)p_2&\longmapsto k\space\sharp\space\lbrack p_1/x\rbrack p_2
\end{align}
$$

The rules of indirect proof give rise to the following transitions
$$
\begin{align}
\text{ccp}(x.(k_1\space\sharp\space p_1))\space\sharp\space p_2&\longmapsto\lbrack p_2/x\rbrack k_1\space\sharp\space \lbrack p_2/x\rbrack p_1\\
k_1\space\sharp\space\text{ccr}(u.(k_2\space\sharp\space p_2))&\longmapsto \lbrack k_1/u\rbrack k_2\space\sharp\space \lbrack k_1/u\rbrack p_2
\end{align}
$$

The first one defines the behavior of the refutation of $\phi$ that proceeds by contradicting the assumption that $\phi$ true. Such refutation is activated by presenting it with a proof of $\phi$, which is substituted by assumption in the new state.

Thus, ccp stands for call with current proof.

Second transition defines the behavior of proof of $\phi$ by contradicting assumption $\phi$ false, which is activated by presenting it with a refutation of $\phi$, which is substituted by assumption in the new state.

Thus, ccr stands for call with current refutation.

The last 2 rules overlap in that there are two transitions for a state of form
$$
\text{ccp}(x.(k_1\space\sharp\space p_1))\space\sharp\space\text{ccr}(u.(k_2\space\sharp\space p_2))
$$

  • one to state $\lbrack p/x\rbrack k_1\space\sharp\space\lbrack p/x\rbrack p_1$ where $p$ is $\text{ccr}(u.(k_2\space\sharp\space p_2))$
  • one to state $\lbrack k/x\rbrack k_2\space\sharp\space\lbrack k/x\rbrack p_2$ where $k$ is $\text{ccp}(x.(k_1\space\sharp\space p_1))$

Non-Deterministic Dynamics

Dynamics of classical logic is non-deterministic. To avoid this one may impose priority order among the two cases

  • preferring the first corresponds to a lazy dynamics for proof, since we pass an unevaluated $p$ to left side refutation.
  • preferring the second corresponds to a eager dynamics for proof, since we pass unevaluated refutation $k$ to proof, which is thereby activated.

States and Theorems

All proofs in classical logic proceed by contradicting the assumption that it is false. In terms of classical logic the initial and final states of a computation are as follows
$$
\displaylines{\dfrac{}{halt_\phi\space\sharp\space p\text{ initial}}\\
\dfrac{p\text{ canonical}}{halt_\phi\space\sharp\space p\text{ final}}}
$$
where $\text{halt}_\phi$ is assumed refutation of $\phi$. Judgment $p \text{ canonical}$ states that $p$ is a canonical proof, which holds of any proof other than an indirect proof.

Execution consists of deriving a general proof to a canonical proof, under the assumption that the theorem is false.

Preservation

If $k\div\phi$, $p:\phi$, and $k\space\sharp\space p \longmapsto k’\space\sharp\space p’$, then there exists $\phi’$ such that $k’\div\phi’$ and $p’:\phi’$.

Progress

If $k \div\phi$ and $p:\phi$, then either $k\space\sharp\space p\text{ final}$ or $k\space\sharp\space p\longmapsto k’\space\sharp\space p’$.

Law of the Excluded Middle

$$
\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{}{\phi\vee\neg\phi\text{ false},\phi\text{ true}\vdash\phi\text{ true}}}{\phi\vee\neg\phi\text{ false},\phi\text{ true}\vdash\phi\vee\neg\phi\text{ true}}\space\space\dfrac{}{\phi\vee\neg\phi\text{ false},\phi\text{ true}\vdash\phi\vee\neg\phi\text{ false}}}{\phi\vee\neg\phi\text{ false},\phi\text{ true}\vdash\sharp}}{\phi\vee\neg\phi\text{ false}\vdash\phi\text{ false}}}{\phi\vee\neg\phi\text{ false}\vdash\neg\phi\text{ true}}}{\phi\vee\neg\phi\text{ false}\vdash\phi\vee\neg\phi\text{ true}}\phantom{“”}\dfrac{}{\phi\vee\neg\phi\text{ false}\vdash\phi\vee\neg\phi\text{ false}}}{\dfrac{\phi\vee\neg\phi\text{ false}\vdash\sharp}{\phi\vee\neg\phi\text{ true}}}
$$

We obtain the proof term $p_0:\phi\vee\neg\phi$ where $u \div\phi\vee\neg\phi$.
$$
\text{ccr}(u.(u\space\sharp\space r\cdot \text{not }(\text{ccp }(x.(u\space\sharp\space l\cdot x)))))
$$
To understand the computational meaning of the proof, let $k\div\phi\vee\neg\phi$ and simplify it with proof dynamics given.

The first step is the transition
$$
k \space\sharp\space\text{ccr}(u.(u\space\sharp\space r\cdot \text{not }(\text{ccp }(x.(u\space\sharp\space l\cdot x)))))\\
\longmapsto\\
k\space\sharp\space r\cdot\text{not }(\text{ccp }(x.(k\space\sharp\space l\cdot x)))
$$
Since $k \div\phi\vee\neg\phi$, then $k$ must have form $\text{case}(k_1;k_2)$ with $k_1\div\phi$ and $k_2\div\neg\phi$. Thus the next transition is
$$
\text{case}(k_1;k_2)\space\sharp\space r\cdot\text{not }(\text{ccp }(x.(\text{case}(k_1;k_2)\space\sharp\space l\cdot x)))\\
\longmapsto\\
k_2\space\sharp\space \text{not }(\text{ccp }(x.(\text{case}(k_1;k_2)\space\sharp\space l\cdot x)))
$$
By virtue of its type $k_2$ must have form $\text{not}(p_2)$ where $p_2:\phi$, hence the transition
$$
\text{not}(p_2)\space\sharp\space \text{not }(\text{ccp }(x.(\text{case}(k_1;k_2)\space\sharp\space l\cdot x)))\\
\longmapsto\\
p_2\space\sharp\space \text{ccp }(x.(\text{case}(k_1;k_2)\space\sharp\space l\cdot x))
$$
Since $p_2$ is a valid proof of $\phi$, the transition
$$
p_2\space\sharp\space \text{ccp }(x.(\text{case}(k_1;k_2)\space\sharp\space l\cdot x))\\
\longmapsto\\
\text{case}(k_1;k_2)\space\sharp\space l\cdot p_2\\
\longmapsto\\
k_1\space\sharp\space p_2
$$

LEM illustrates the classical proof are interactions between proofs and refutations, which is to say interactions between a proof and the context in which it is used.

In programming terms, this corresponds to an abstract machine with an explicit control stack, or continuation, representing the context of evaluation of an expression. The expression may access the context (stack, continuation) to backtrack so as to maintain the symmetry between truth and falsity.

The penalty is that a closed proof of a disjunction no longer need to show which disjunct it prove, since it may “change its mind” in the process of proof.

The Double-Negation Transition

One consequence of the greater expressiveness of constructive logic is that classical logic proof may be translated systemically into constructive proofs of a classically equivalent proposition.

Consequently, there is no loss in adhering to constructive proofs, since every every classical proof is a constructive proof of a constructively weaker, but classically equivalent, proposition.

Moreover, classical logic is weaker (less expressive) than constructive logic, contrary to a naive interpretation which would say that the added reasoning principles, such as LEM, afforded by classical logic makes it stronger.

In PL terms, adding a feature doesn’t necessarily strengthen (improve the expressive power) of your language; on the contrary, it might weaken it.

Trans between Constructive and Classical Logic

Define $\phi^\ast$ as a translation of proposition that interprets classical into constructive logic by following
$$
\begin{align}
Classical&&Constructive&&\\
\Delta\space\Gamma\vdash\phi\text{ true}&&\neg\Delta^\ast\space\Gamma^\ast\vdash\neg\neg\phi^\ast\text{ true}&&\text{truth}\\
\Delta\space\Gamma\vdash\phi\text{ false}&&\neg\Delta^\ast\space\Gamma^\ast\vdash\neg\phi^\ast\text{ true}&&\text{falsity}\\
\Delta\space\Gamma\vdash\sharp&&\neg\Delta^\ast\space\Gamma^\ast\vdash\bot\text{ true}&&\text{contradiction}\\
\end{align}
$$
And here is one choice for translation makes proof of correspondence between classical and constructive logic simple:
$$
\begin{align}
\top^\ast&=\top\\
(\phi_1\wedge\phi_2)^\ast&=\phi_1^\ast\wedge\phi_2^\ast\\
\bot^\ast&=\bot\\
(\phi_1\vee\phi_2)^\ast&=\phi_1^\ast\vee\phi_2^\ast\\
(\phi_1\supset\phi_2)^\ast&=\phi_1^\ast\supset\neg\neg\phi_2^\ast\\
(\neg\phi)^\ast&=\neg\phi^\ast
\end{align}
$$

DNE Transition

$$
\neg\neg\phi\text{ true}\space\neg\neg\psi\text{ true}\vdash\neg\neg(\phi\wedge\psi)\text{ true}
$$

The proof target can be transformed into $\neg\neg\phi\wedge\neg\neg\psi\supset\neg\neg(\phi\wedge\psi)\text{ true}$.

The proof term has shape like $\lambda(x:(\neg\neg\phi\wedge\neg\neg\psi))\text{ not }(\text{ ccp }((u:\neg(\phi\wedge\psi)).(\dots)))$.

The contradiction inside can be constructed as
$$
\langle\text{ccr }((u_0\div\phi).(\text{fst};x(\text{not}(u_0))\space\sharp\space\text{exfalso}));\text{ccr }((u_1\div\psi).(\text{fst};x(\text{not}(u_1))\space\sharp\space\text{exfalso}))\rangle\space\sharp\space u
$$
Thus the DNE here is transformed.

Exercises

Generate Proof Terms

  • $(\neg\neg\phi)\supset\phi$

    We can get a rough shape of the proof term like $\lambda(x:\neg\neg\phi)\text{ ccr }((u\div\phi).(\dots))$.

    Contradiction inside can be constructed as $\text{exfalso}\space\sharp\space x(\text{not}(u))$ since $x :(\tau\to\bot)\to\bot$ and $\text{not}(n) :\tau\to\bot$.

    Thus the proof term is $\lambda(x :\neg\neg\phi)\text{ ccr }((u\div\phi).(\text{exfalso}\space\sharp\space x(\text{not}(u))))$.

  • $(\neg\phi_2\supset\neg\phi_1)\supset(\phi_1\supset\phi_2)$

    The rough shape of the proof term is like $\lambda(x: (\neg\phi_2\supset\neg\phi_1))\lambda(x_0:\phi_1)\text{ ccr }((u\div\phi_2).(\dots))$.

    Contradiction can be formed as $\text{exfalso}\space\sharp\space x(\text{not}(u))(x_0)$.

    Thus $\lambda(x: (\neg\phi_2\supset\neg\phi_1))\lambda(x_0:\phi_1)\text{ ccr }((u\div\phi_2).(\text{exfalso}\space\sharp\space x(\text{not}(u))(x_0))):(\neg\phi_2\supset\neg\phi_1)\supset(\phi_1\supset\phi_2)$

  • $\neg(\phi_1\vee\phi_2)\supset(\neg\phi_1\wedge\neg\phi_2)$

    The rough shape can be $\lambda(x:\neg(\phi_1\vee\phi_2))\langle\dots,\dots \rangle$.

    The left hand side can be $\text{not}(\text{ccp}((x_1:\phi_1).(\text{exfalso}\space\sharp\space x(l\cdot x_1))))$, which proves $x_1:\phi_1$.

    Right hand side is similar $\text{not}(\text{ccp}((x_2:\phi_2).(\text{exfalso}\space\sharp\space x(r\cdot x_2))))$ for $x_2:\phi_2$.