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 section 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;

Go to the first, previous, next, last section, table of contents.