Commenting proofs
James R. Geiser · International Joint Conference on Artificial Intelligence · 1975
The goal of this investigation is the development of a semantics for 1 order theories based on certain new syntactic structures in formal proofs which derive from their pragmatic and semantic aspects. The present report is mainly concerned with these new syntactic structures, the motivation behind them, their technical definition and their basic properties. Their role in a new semantics for Intuitiomistc Peano Arithmetic is indicated in the last section.