LARA

This is an old revision of the document!


Theorems as Abstract Data Types

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.