Substitutionless First-Order Logic: A Formal Soundness Proof

Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull, Jørgen Villadsen

Research output: Contribution to conferencePaperResearchpeer-review

216 Downloads (Pure)


Substitution under quantifiers is non-trivial and may obscure a proof system for newcomers. Monk (Arch. Math. Log. Grundl. 1965) successfully eliminates
substitution via identities and also uses a so-called normalization of formulas as a further simplification. We formalize the substitutionless proof system in Isabelle/HOL, spelling out its side conditions explicitly and verifying its soundness
Original languageEnglish
Publication date2018
Number of pages3
Publication statusPublished - 2018
EventIsabelle Workshop 2018 - Oxford, United Kingdom
Duration: 13 Jul 201813 Jul 2018


WorkshopIsabelle Workshop 2018
Country/TerritoryUnited Kingdom
Internet address


Dive into the research topics of 'Substitutionless First-Order Logic: A Formal Soundness Proof'. Together they form a unique fingerprint.

Cite this