Proof Structure

Proofs  are tree structures. Using term notation, the class of proofs is the least set of terms such that

• is a proof.

• if are proofs, , then is a proof,

where:

• g is a sequent.
• r is a refinement rule. See Section

The sequent g in the proof or is referred to as the root goal  , or simply the goal of the proof. Similarly, the goals of the proofs are referred to as the subgoals  of the proof .

A proof is good  when is satisfies various conditions, including

1. every sequent in the proof is closed ; every free variable of a sequent clause is bound by some declaration of the sequent,
2. at every refined node of the proof tree, the rule proves the goal sequent, assuming the provability of the subgoal sequents.

A proof is complete  exactly when it is good and contains no unrefined nodes. A proof is incomplete  if it is good but does contain unrefined nodes.

Each theorem object in Nuprl's library contains one proof. The root goal of this proof is sometimes referred to as the main goal  of the theorem. It always has no hypotheses.