First-Order Logic According to Fitting

Stefan Berghofer 🌐 with contributions from Asta Halkjær From 🌐

August 2, 2007

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We present a formalization of parts of Melvin Fitting's book "First-Order Logic and Automated Theorem Proving". The formalization covers the syntax of first-order logic, its semantics, the model existence theorem, a natural deduction proof calculus together with a proof of correctness and completeness, as well as the Löwenheim-Skolem theorem.

License

BSD License

History

July 21, 2018
Proved completeness theorem for open formulas. Proofs are now written in the declarative style. Enumeration of pairs and datatypes is automated using the Countable theory.

Topics

Session FOL-Fitting