What is the precise definition of the notion of a 'theorem'?

It is given by a proof system, which specifies

• a set of axioms
• a set of proof rules for deriving new theorems from existing theorems

Theorems are all possible roots of proof trees, where proof trees have axioms in leaves and proof rules in the nodes.

Key Idea:

Introduce theorem as an ADT whose operations correspond to axioms and proof rules.

Then we can write arbitrary programs that compute values of 'theorem' type. All such values will be theorems.

Soundness of the approach: if a value of type 'theorem' is computed, we know there exists an expression formed from ADT operations. This means that there is a proof tree, so the value is a theorem.

Often proof manipulating or even ADT functions are partial. We can express this using algebraic data types with alterbatives (e.g. option types), or using exceptions. These features, as implemented in ML do not compromise type safety. We illustrate this using propositional logic.

abstype theorem
groundT : formula -> theorem option // returns a theorem if given formula is ground and evaluates to true
inspect : theorem -> formula // return formula for theorem so we can decide how to prove it
cases : theorem -> theorem -> formula -> variable -> theorem option
andI : theorem -> theorem -> theorem 
andE1 : theorem -> theorem option

Here 'cases t1 t2 f x' will compute f[x:=true] and check that it is identical to t1, then compute f[x:=false] and check it is identical to t2. If both tests succeed, it will return f as a theorem.

The 'andI' (and introduction) function takes two theorems and computes their conjunction, which is also a theorem.

The 'andE1' (first and-elimination) takes a theorem, checks whether it has the form 't1 & t2'. If so, it returns t1.

Using such ADT we can build a prover that is guaranteed to either produce correct result or fail (it will never produce a formula that is a non-theorem).

let rec prove (f : form) : theorem option =
  if (isGround f) then (groundT f)
  else (let v = getOneFreeVar f in
       match (prove (subst [(v,True)] f), prove (subst [(v,False)] f)) with
       | (Some t1, Some t2) -> cases t1 t2 f v
       | _ -> None)

It can be tedious to propagate possible errors. This is why exceptions are so useful.

Tactics accept formulas and try to produce the theorem containing this formula.

Tatics can often be combined into bigger tatics using higher-order functions called tacticals (for example, alternative, sequencing, repetition).