## Abstract

I introduce the falsifier calculus, a new deep-inference proof system for first-order predicate logic in the language of Hilbert's epsilon-calculus. It uses a new inference rule, the falsifier rule, to introduce epsilon-terms into a proof, distinct from the critical axioms of the traditional epsilon-calculus. The falsifier rule is a generalisation of one of the quantifier-shifts, inference rules for shifting quantifiers inside and outside of formulae. Like the epsilon-calculus and proof systems which include quantifier-shifts, the falsifier calculus admits non-elementarily shorter cut-free proofs of certain first-order theorems than the sequent calculus.Analogous to the way in which Herbrand's Theorem decomposes a proof into a first-order and a propositional part, connected by a Herbrand disjunction as an intermediate formula, I prove a decomposition theorem for the falsifier calculus which gives rise to a new notion of intermediate formula in the epsilon-calculus, falsifier disjunctions. I then prove that certain first-order theorems admit non-elementarily smaller falsifier disjunctions than Herbrand disjunctions.

Original language | English |
---|---|

Title of host publication | Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science |

Place of Publication | U. S. A. |

Publisher | IEEE |

ISBN (Electronic) | 9798400706608 |

DOIs | |

Publication status | Published - 8 Jul 2024 |

Event | 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024 - Tallinn, Estonia Duration: 8 Jul 2024 → 11 Jul 2024 |

### Publication series

Name | Proceedings - Symposium on Logic in Computer Science |
---|---|

ISSN (Print) | 1043-6871 |

### Conference

Conference | 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024 |
---|---|

Country/Territory | Estonia |

City | Tallinn |

Period | 8/07/24 → 11/07/24 |

### Bibliographical note

For the purpose of Open Access the author has applied a CC BY public copyright licence to any Author Accepted Manuscript version arising from this submission.### Acknowledgements

This work would not have been possible without Alessio Guglielmi, who was watching over me while this research was taking place and whose loss has been felt deeply across the MathFound group in Bath. I would also like to thank my supervisor Willem Heijltjes for his invaluable guidance and support throughout the writing of this paper.### Funding

This work was funded by the United Kingdom Research & Innovation (UKRI) under Engineering and Physical Sciences Research Council (EPSRC) grant EP/T518013/1, studentship 2601979.

Funders | Funder number |
---|---|

UK Research & Innovation | |

Engineering and Physical Sciences Research Council | EP/T518013/1, 2601979 |

## Keywords

- deep inference
- epsilon-calculus
- first-order logic
- Herbrand's theorem

## ASJC Scopus subject areas

- Software
- General Mathematics