Abstract
We present a proof system for a conservative extension of propositional clas-sical logic with decision trees that is strictly linear. This means that not
only there are no structural rules such as contraction and weakening but
there are no rules for unit equalities either, and there is no negation. Yet, its
classical semantics and proof-theoretic properties can be recovered via an in-
terpretation map at a polynomial cost. Moreover, this system can p-simulate
substitution Frege. Those results are made possible primarily by two tech-
nical advances: 1) an ‘Eversion Lemma’, that guarantees extreme flexibility
in manipulating formulae to match a given logical context, and 2) a form
of explicit substitution for derivations into derivations. We argue that this
proof system represents a significant step towards a notion of factorisation
for proofs. That will hopefully lead us to a semantics of proofs adequate to
solve the proof identity problem.
| Date of Award | 11 Dec 2024 |
|---|---|
| Original language | English |
| Awarding Institution |
|
| Supervisor | Alessio Guglielmi (Supervisor) & Willem Heijltjes (Supervisor) |