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.


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

Change 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.


Theories of FOL-Fitting