[Prev][Next][Index][Thread]

proof terms for classical logic in natural deduction formulation


PROOF TERM ASSIGNMENT for CLASSICAL LOGIC in NATURAL DEDUCTION  
FORMULATION

In this note we will define a proof term calculus for First Order
Classical Logic (CL) in a Natural Deduction Formulation (as can be
found in several recent papers of Michel Parigot). But instead of
using Parigot's mu-calculus we stick to a more traditional language
for proof terms, namely a fragment of Martin-Loef's Type Theory.
Actually it is a rather poor fragment. Besides \-calculus we simply
use the pairing function <_,_> (which is a constructor) and
Martin-Loef's eliminator pattern-matching. It is just the operator
defined by the semantics :

          p => <a,b>  e[a,b/x,y] => c
         -----------------------------
           E(p , (x,y) e) => c

In a more traditional (SML-style notation one could write 


     let  <x,y> = p  in  e    instead of  E(p , (x,y) e)  .

Our proof term assignment is inspired by the negative polarity  
fragment of Girard's LC. This gives rise to the following improved   
~~-translation :

   G(A) := ~ A*

where  (_)*  is defined inductively as follows :

   A*  :=  ~ A    (A atomic)

   (A=>B)* :=  G(A) and B*

   (~ A)*  :=  ~ A*

   (All x. A)*  :=  Exist x. A*

The translation (_)* has to be thought of as translating the
{=>,~,All} fragment of classical logic to the {and,~,Exist} fragment
of intuitionistic logic.  Notice that on the intuitionistic level
~ A := A -> R where R is a generic intuitionistic type representing
'falsity'.  The translation of a classical sequent

      A_1 , ... , A_n  |-  B_1 , ... , B_m

to its intuitionistic counterpart is 

      G(A_1) , ... , G(A_n) , B_1* , ... , B_m* |- R      

Now it is straightforward to have a proof term assignment for the  
translations of classical to intuitionistic sequents.  Accordingly,
instead of

  u1 : G(A_1) ,..., un : G(A_n) , k1 : B_1* ,..., km : B_m* |- p : R 

we simply write

  u1 : A_1 , ... , un : A_n  |- k1 : B1 , ... , km : B_m  |  p

Thus the turnstile simply serves as an indication of which formulas C  
of the context are intended to represent the propositional type  G(C)   
(namely those left of the turnstile) and which of the formulas C of  
the context are intended to represent the propositional type  C* .

Thus from the term assignment for proofs in intuitionistic first  
order logic we immediately get the following proof term assignment  
calculus for first order classical logic :


(=>I)        Gamma , u : A |- k : B , Delta | p
          ----------------------------------------------
             Gamma |- w : A => B , Delta | E(w, (u,k) p)


(=>E)      Gamma |- k : A => B , Delta | p   

           Gamma |- h : A , Delta | q
         -------------------------------------------
           Gamma |- w : B , Delta | (\k.p) <\h.q,w>


(~I)           Gamma , u : A |- Delta | p
           --------------------------------
              Gamma |- u : ~ A , Delta | p


(~E)       Gamma |- k : ~ A , Delta | p   

	   Gamma |- h : A , Delta | q
         ------------------------------------
             Gamma |- Delta | (\k.p) (\h.q)


(All-I)    Gamma |- k : A[x] , Delta | p
         -----------------------------------------------
           Gamma |- w : All x. A , Delta | E(w, (x,k) p)


(All-E)    Gamma |- k : All x. A , Delta | p
          --------------------------------------------
           Gamma |- w : A[t/x] , Delta | (\k.p) <t,w>


Thomas Streicher

P.S.  Our work seems to be strongly related to seminal work of Chet
Murthy. He probably knows all that. But in his LICS'90 paper there is
missing an explicit proof term assignment calculus (I guess it is
assumed implicitly).

Maybe the observations above could serve as a basis to provide
Parigot's mu-calculus with a more traditional semantics translating
terms of the mu-calculus to a fragemt of Maertin-Loefs type theory.