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.