Modular Normalisation of Classical Proofs

  • Benjamin Ralph

Student thesis: Doctoral ThesisPhD

Abstract

The main contribution of this thesis is to present a study of two normalisation theorems and proofs in classical logic: one propositional, one first-order. For propositional logic, we show a local cycle removal procedure through reductions on merge contractions that ensures that proofs can be decomposed—that contractions can be pushed to the bottom of a proof—in a straightforward way. For first-order logic, we show how decomposition of proofs can correspond to two presentations of Herbrand’s Theorem, and how we can use translations into expansion proofs to give a new, indirect cut elimination theorem for first-order logic.
In addition, an old but interesting cut elimination method for propositional logic, the experiments method, is formally presented for the first time, and we extend the theory of merge contractions to first-order logic.
Date of Award3 Apr 2019
LanguageEnglish
Awarding Institution
  • University of Bath
SupervisorJames Laird (Supervisor) & Alessio Guglielmi (Supervisor)

Keywords

  • proof theory
  • deep inference
  • normalisation
  • propositional logic
  • first-order logic
  • herbrand's theorem

Cite this

Modular Normalisation of Classical Proofs
Ralph, B. (Author). 3 Apr 2019

Student thesis: Doctoral ThesisPhD