KnowledgeBase » SEMINAR » ID = 478

Proof Polynomials: Cut Elimination

by Sergei Artemov
1997-1998

A proof from a set of hypotheses H is regarded as a function of the proofs of H. In particular, a proof from the empty set H (a pure proof) is a constant. As it was noticed recently, every absolute (i.e., independent of the formalism chosen) operation on proofs can be realized as a "proof polynomial" built from the variables and constants for pure proofs by three basic operations: "application;" "proof checker;" and "nondeterministic choice."

The entire variety of proof polynomials can be described within a framework of the Logic of Proofs, which is supplied with completness and decidability theorems. Today we present a cut-free axiom system for the Logic of Proofs.