Expansion trees with cut

Herbrand’s theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher-order logics by recording the information of which instances have been chosen for which quantifiers. This compact representation is known in the literature as Miller’s expansion tree proof. It is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cuts have been proposed. These extensions are based on graphical formalisms similar to proof nets and are limited to prenex formulas.In this paper, we present a new syntactic approach that directly extends Miller’s expansion trees by cuts and also covers non-prenex formulas. We describe a cut-elimination procedure for our expansion trees with cut that is based on the natural reduction steps and shows that it is weakly normalizing.

Deep inference and expansion trees for second-order multiplicative linear logic

In this paper, we introduce the notion of expansion tree for linear logic. As in Miller's original work, we have a shallow reading of an expansion tree that corresponds to the conclusion of the proof, and a deep reading which is a formula that can be proved by propositional rules. We focus our attention to MLL2, and we also present a deep inference system for that logic. This allows us to give a syntactic proof to a version of Herbrand's theorem.

Herbrand’s theorem

According to Herbrand’s theorem, each formula F of quantification theory can be associated with a sequence F1, F2, F3,… of quantifier-free formulas such that F is provable just in case Fn is truth-functionally valid for some n. This theorem was the centrepiece of Herbrand’s dissertation, written in 1929 as a contribution to Hilbert’s programme. It provides a finitistically meaningful interpretation of quantification over an infinite domain. Furthermore, it can be applied to yield various consistency and decidability results for formal systems. Herbrand was the first to exploit it in this way, and his work has influenced subsequent research in these areas. While Herbrand’s approach to proof theory has perhaps been overshadowed by the tradition which derives from Gentzen, recent work on automated reasoning continues to draw on his ideas.

FROM STENIUS’ CONSISTENCY PROOF TO SCHÜTTE’S CUT ELIMINATION FOR ω-ARITHMETIC

The book Das Interpretationsproblem der Formalisierten Zahlentheorie und ihre Formale Widerspruchsfreiheit by Erik Stenius published in 1952 contains a consistency proof for infinite ω-arithmetic based on a semantical interpretation. Despite the proof’s reference to semantics the truth definition is in fact equivalent to a syntactical derivability or reduction condition. Based on this reduction condition Stenius proves that the complexity of formulas in a derivation can be limited by the complexity of the conclusion. This independent result can also be proved by cut elimination for ω-arithmetic which was done by Schütte in 1951.In this paper we interpret the syntactic reduction in Stenius’ work as a method for cut elimination based on invertibility of the logical rules. Through this interpretation the constructivity of Stenius’ proof becomes apparent. This improvement was explicitly requested from Stenius by Paul Bernays in private correspondence (In a letter from Bernays begun on the 19th of September 1952 (Stenius & Bernays, 1951–75)). Bernays, who took a deep interest in Stenius’ manuscript, applied the described method in a proof Herbrand’s theorem. In this paper we prove Herbrand’s theorem, as an application of Stenius’ work, based on lecture notes of Bernays (Bernays, 1961). The main result completely resolves Bernays’ suggestions for improvement by eliminating references to Stenius’ semantics and by showing the constructive nature of the proof. A comparison with Schütte’s cut elimination proof shows how Stenius’ simplification of the reduction of universal cut formulas, which in Schütte’s proof requires duplication and repositioning of the cuts, shifts the problematic case of reduction to implications.

HERBRAND’S THEOREM AND NON-EUCLIDEAN GEOMETRY

We use Herbrand’s theorem to give a new proof that Euclid’s parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simple, and intuitively appealing proof.