Classical proof forestry

Classical proof forests are a proof formalism for first-order classical logic based on Herbrand's Theorem and backtracking games in the style of Coquand. First described by Miller in a cut-free setting as an economical representation of firstorder and higher-order classical proof, defining features of the forests are a strict focus on witnessing terms for quantifiers and the absence of inessential structure, or `bureaucracy'. This paper presents classical proof forests as a graphical proof formalism and investigates the possibility of composing forests by cut-elimination. Cut-reduction steps take the form of a local rewrite relation that arises from the structure of the forests in a natural way. Yet reductions, which are significantly different from those of the sequent calculus, are combinatorially intricate and do not exclude the possibility of infinite reduction traces, of which an example is given. Cut-elimination, in the form of a weak normalisation theorem, is obtained...

• Type: Journal
• Year: 2010
• Where: APAL
• Authors: Willem Heijltjes
• Keywords: APAL 2010, Classical Proof Forests, First-order Classical Logic, Proof Formalism