The Curry's Paradox in Fitch Style #paradox

Introduction

We present a little tour de force in implementing a Prolog technology theorem prover for intuitionistic propositional and first order logic. The main idea was already demonstrated by John Slaney in his MINLOG System.

Instead of transforming a proof from NJ to LJ as in cut elimination, we transform a proof back from LJ to NJ. What helps us doing this transformation is extracting and rendering proof terms from the Curry-Howard isomorphism.

Searching LJ

We only consider the implicational fragment from the connective (=>). We use the following inference rules for this connective. A double line (=) indicates that this inference rule is invertible. In Prolog invertible inference rule can be greedily applied with a cut (!) reducing backtracking:

      ------------ (Ax)
       Γ, P |- P

       Γ, A => B |- A    Γ, B |- C                Γ, A |- B
      ----------------------------- (L=>)       ============= (R=>)
          Γ, A => B |- C                         Γ |- A => B

       Γ, (A=>f) |- f
      ---------------- (RAA)
            Γ |- A

The intuitionistic calculus consists of the rules (Ax), (L=>) and (R=>). To spice up things we also provide reduction ad absurdum (RAA), making the calculus also find classical logic proofs. The Prolog implementation was guided by Jens Ottens leanseq_v2.p for classical LK.

But unlike classical LK, the intuitionistic LJ differs in a few points. First we deal with sequents that are not multiple consequence but have only a single formula as consequence. Second the inference rules (L=>) and (RAA) are not terminating.

The intuitionistic version of left implication rule (L=>) might loop, because A => B appears again in the premisses. The classical reduction ad absurdum rule (RAA) might also loop. To nevertheless provide some proof search we already use iterative deepening in the propositional case:

% implication left
prove(G > E, I, app(lam(V:B,P2),app(U:(A=>B),P1))) :- I > 0,
                select(U:(A=>B),G,G1),
                I2 is I-1,
                prove(G > A, I2, P1),
                prove([V:B|G1] > E, I2, P2).

% Reductio Ad Absurdum
prove(G > A, I, 'C'(lam(U:(A=>f),P))) :- I > 0,
                I2 is I-1,
                prove([U:(A=>f)|G] > f, I2, P).

The above Prolog code shows how iterative deepening is done. We have a counter I, which is decremented for every potentially looping inference rule. So that for a given depth the search terminates. Then the depth is gradually incremented and search is restarted.

Rendering NJ

The previous Prolog code also shows the Proof terms that we extract. We use Prolog terms of the form lam(U:A,B) to represent the simple type Lambda abstraction λU:A.B and Prolog terms of the form app(A,B) to represent the simple type application (A B).

Reduction ad absurdum has its own combinator 'C', with the typing rule of double negation elimination. This means it sends the type judgement T:((A=>f)=>f) to the type judgement 'C'(T):A. Proof rendering is then done based on the extracted proof terms.

render(lam(K1:X,P), O, N, K, K) :-
   render_line(O, K1:X, assume, N, K1),
   I is O+1,
   render(P, I, K1, J, K2),
   render_line(O, lam(K1:X,P), imp(K1,K2), J, K).
render(app(P1,P2), O, N, K, K) :-
   render(P2, O, N, H, K2),
   render(P1, O, H, J, K1),
   render_line(O, app(P1,P2), mp(K1,K2), J, K).

The above shows the rendering code for the basic simple types. To render intuitionistic and classical proofs we have also rendering code for the combinator 'C'. Further we apply the detection of chaining so that we can render step by step application in Fitch style:

Curry's Paradox

The below shows a proof of Peirce's Law. Although the formula is from the (=>) fragment, it is not intuitionistically valid. In our system a classical proof is found using reduction ad absurdum rule (RAA). It has a Fitch style rendering similar to the implication introduction rule:

We can also proof Curry's Paradox. A little obstacle is the lack of conjunction, otherwise we could model the bicondional according to the identity (A<=>B) -||- (A=>B)&(B=A). We worked around the problem using the identity (A&B=>C) -||- (A => (B => C)) from residuated lattices.

The paradoxical situation here is here, that we can find a proof that doesn't use reduction ad absurdum rule (RAA). This means the Curry's Paradox is intuitionistically valid and doesn't need some special inference rule dealing with negation. Running counter to intuitions about negative vicious circles.

Adding Quantifiers

The final piece was adding quantifiers to our proof search and rendering. The propositional calculus LJ was first extended into a first order calculus LJ by adding these two inference rules. We only add the forall quantifier. Again we use double line (=) to indicate invertible rules:

        Γ, A[X/T], ∀X.A |- B               Γ |- A    x ∉ Γ 
      ------------------------ (L∀)       ================= (R∀)
             Γ, ∀X.A |- B                     Γ |- ∀X.A

To implement these inference rules we use all the precautions and spectacle from Jens Ottens ileanSeP prover. For the propositional rules the precautions mean we have to use unify_with_occurs_check/2 in the (Ax) rule. And the (L=>) rules needs a copy_term/2 of the sub formulas A and B.

The spectacle for the new (L∀) and (R∀) rule is the same as in Jens Ottens leanSeq prover, i.e. copy_term/2 and Skolem term to realize the side condition x ∉ Γ. Extracting simple terms was a little tricky, and we cheated heavily to avoid getting into dependent types:

% universal quantifier right
prove(G > (![X]:A), FV,I,J,K, lam(f_sk(J,FV):t(![X]:A),P)) :- !,
                copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
                J1 is J+1,
                prove(G > A1,FV,I,J1,K,P).

% universal quantifier left
prove(G > D,FV,I,J,K,app(lam(V:A1,P),app(U:(![X]:A),Y:t(A1)))) :- I > 0,
                member(U:(![X]:A),G),
                I2 is I-1,
                copy_term((X:A,FV),(Y:A1,FV)),
                prove([V:A1|G] > D,[Y|FV],I2,J,K,P).

Basically we use a non-standard type t(Q) to indicate that a term is from another kind than formulas. The argument Q in this terms helps us sorting out the bound variable renaming in Jens Ottens leanSeq. It will short cut some type inference so that the right formulas are rendered.

Barber Paradox

Lets first do a little Fitch style warm up. Because we only have forall quantifier, we need to use negation to model the exists quantifier. Since our t(Q) types are always accepted we are not inside a free logic with non-denoting terms and can establish the theorem that ∀X:p(X) => ∃X:p(X) in natural deduction:

The labels ins/1 and abs/1 indicate forall quantifier rules instantion respectively abstraction, whereas mp/2 and imp/2 indicate the conditional rules modus ponens respectively implication introduction. The proof is intuitionistically valid. The Barber Paradox has now the propositional shape as the Curry's Paradox:

The Barber Paradox is used as an illustration of Russell's Paradox. In the above we show intuitionistic validity of the formula ∀X:∀Y:((s(X, X) => q) <=> s(Y, X)) => q. Read s/2 as shaves and q/0 as falsum to get the rejection of the Barber sentence, since our non-free logic assumes at least one Barber.

Conclusions

Drawing upon Jens Ottens ileanSeP and leanSeq we deviced propositional and first order proof search for LJ. We can render Fitch Style proofs of Curry's Paradox and the propositionally resembling Barber Paradox, whereby our logic assumes at least one Barber. Both are intuitionistically valid.