A Calculus of Falsifiers

Abstract

The falsifier calculus, a deep-inference proof system for first-order predicate logic in thelanguage of Hilbert’s epsilon-calculus, is introduced. It uses a novel inference rule, thefalsifier rule, to introduce epsilon-terms into proofs, distinct from the critical axioms ofthe traditional epsilon-calculus. The falsifier rule is a generalisation of one of the quantifiershifts, inference rules for shifting quantifiers inside and outside of formulae. Like the epsiloncalculus and proof systems which include quantifier-shifts, the falsifier calculus admits nonelementarily smaller cut-free proofs of certain classes of first-order theorems than the sequentcalculus.Analogous to the way in which Herbrand’s Theorem decomposes a proof into a first-orderand a propositional part, connected by a Herbrand disjunction as an intermediate formula,the falsifier calculus provides a new decomposition theorem for first-order proofs whichinduces a new notion of intermediate formula in the epsilon-calculus, falsifier disjunctions.It is demonstrated that certain classes of first-order theorems admit non-elementarily smallerfalsifier disjunctions than Herbrand disjunctions.Through these properties, the falsifier calculus contributes new insights to our understanding of the structure and complexity of proofs in first-order predicate logic. The phenomenon of the non-elementary compression of cut-free proofs has long been of interest instructural proof theory, and the falsifier calculus provides a new perspective on what properties make a proof system admit this compression as well as the role of epsilon-terms inthis compression. Furthermore, the decomposition theorem admitted by the falsifier calculusprovides a novel perspective on the structure of Herbrand disjunctions and their complexity,yielding new insights into one of the fundamental theorems of classical proof theory.

Date of Award	20 May 2026
Original language	English
Awarding Institution	University of Bath
Supervisor	Willem Heijltjes (Supervisor) & Alessio Guglielmi (Supervisor)