IV. Logic and proofs

This chapter is dedicated to logical languages and concept of "proofs".

1. The first/simplest language is the one of Propositional calculus defined as follow:

type Prop = Prop of string | Imp of (Prop * Prop);;
let A,B,C = Prop "A", Prop "B", Prop "C";;
let (==>) x y = Imp (x,y);;
let p1 = A ==> A;;
let p2 = A ==> ((A==>B) ==> B);;
let p3 = (A==>B) ==> ((B==>C) ==> (A==>C));;

Thus, a "language" is simply a "set of terms" that can be specified by a "type".

Prop = {A, B, A=>A, A=>(A=>B), (A=>B)=>A, ...}

1 - 12