Formalized First-Order Logic |
| | Abstract | The goal of this thesis is to formalize first-order logic, specifically the natural deduction proof system NaDeA, in the proof assistant Isabelle. The syntax and semantics are formalized as Isabelle data types and functions and the inference rules of NaDeA are defined as an inductive set.
The soundness of these inference rules is formally verified, ensuring only valid formulas can be derived in the proof system.
A textbook proof of completeness for sentences in natural deduction using abstract consistency properties is explained before this proof is formalized. This formalization is based on existing work, but modernized for this thesis. It is described in depth and a version of the completeness result using any countably infinite domain is developed by proving that the semantics respect the bijection between this and the domain of Herbrand terms. Next the problem of open formulas is discussed and a solution provided by an extension to NaDeA. This extension allows the derivation of the original formula from its universal closure, enabling us to close the formula, apply the original completeness result and derive the original one in the extended system. Assumptions are handled by turning them into implications and back again, a technique that requires a proof of weakening to be formalized first. It is unlikely that this extension is actually necessary for completeness for open formulas, but it makes the otherwise subtle interaction between substitution and de Bruijn indices more manageable.
Finally insights gained while working with the formalization and extending it are shared, in the hope that it may help other formal verification efforts. | | Type | Bachelor thesis [Academic thesis] | | Year | 2017 | | Publisher | Technical University of Denmark, Department of Applied Mathematics and Computer Science | | Address | Richard Petersens Plads, Building 324, DK-2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk | | Series | DTU Compute B.Sc.-2017 | | Note | | | Electronic version(s) | [pdf] | | Publication link | http://www.compute.dtu.dk/English.aspx | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|