Substitutionless First-Order Logic: A Formal Soundness Proof

Research output: Contribution to conferencePaperResearchpeer-review

128 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
CountryUnited Kingdom
Internet address

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

Cite this