First-Order Logic According to Fitting

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

August 2, 2007


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.


BSD License


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.


Session FOL-Fitting