[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

4. Proof Terms for Propositional Logic

We support two new methods how to give proofs: Annotated proofs and proof terms. Annotated proofs are Tutch proofs in which each line is annotated by a proof term. Since proof terms record all information necessary to reconstruct a proof, they alone (without a deduction tree) are sufficient as well. For the syntax see the section Proof Terms in the A. Reference. Here are two examples, annotating proofs from the last chapter.

 
% prop0-ann.tut
% Modus ponens

annotated proof mp: A & (A=>B) => B = 
begin
[ x : A & (A=>B);               
  fst x : A;                    
  snd x : A=>B;                 
  (snd x) (fst x) : B ];                        
fn x => (snd x) (fst x) : A & (A=>B) => B         
end;

 
% prop3-ann.tut
% Classical implication definition  ~A|B => A=>B

annotated proof classImpDef : ~A|B => A=>B =
begin
[ x : ~A|B;
  [ a : A;
    [ na : ~A;
      na a : F; 
      abort (na a) : B ];       
    [ b : B;
      b : B ];  
    case x of inl na => abort (na a) | inr b => b end : B ];            
  fn a => case x of inl na => abort (na a) | inr b => b end : A=>B ];   
fn x => fn a => case x of inl na => abort (na a) | inr b => b end : ~A|B => A=>B        
end;

term classImpDef : ~A|B => A=>B =
  fn x => fn a => case x of inl na => abort (na a) | inr b => b end;


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Andreas Abel on October, 24 2002 using texi2html