Primitive Proofs

Essentially, a proof is a finite tree whose notes are sequents and justifications connected in certain ways. The definitions can be given in the form

$$\times \times$$

The justifications explain why the goal sequent follows from the subgoals. We allow incomplete proofs; they are recognizable because the justification is a special element and no subgoals are generated.

Another kind of justification is a primitive rule name. These are the simple justifications, and if we were not interested in automating the development of proofs, this would be all that is necessary to completely define the concept of a proof. The only condition to be checked by the predicate $IsAProo\!f$ would be that the right subgoals were generated by the rules. We call such proofs primitive.