ABSTRACT

Throughout this chapter we fix a language L as in the previous chapter (i.e., equipped with the standard 5 connectives ∧,∨,¬,→,↔, quantifiers ∀,∃, equality =, definitions, and witnesses) and we also fix a theory T in L with (specific) axioms A,B, .... Recall the metadefinition of a proof 7.8. In this chapter we want to discuss this concept in some detail, and to give the first examples of proofs.