Proof system of first-order logic #

This file formalizes a Hilbert-style proof system of first-order logic.

Axiom and Proof define the first-order axioms and Hilbert-style proofs as inductive families. Proof Γ p (or Γ ⊢ p) where Γ is a set of formulas, says that proposition p is provable from the first-order axioms and the propositions in Γ (hypotheses).
A few tactics are provided to facilitate proof writing -- e.g. pintro to introduce local hypothesis as a formula added to Γ, papply to apply a theorem onto the proof goal, and prw to rewrite the equalities or iffs in the proof goal.
A lot of theorems (e.g. principle of explosion Proof.false_elim) and metatheorems (e.g. deduction theorem Proof.deduction) are proved.

Design note #

There are different ways to design a proof system for first-order logic.

Hilbert-style systems, which promote minimality in their design, typically have a minimal set of axioms and minimal inference rules (typically, only Modus Ponens).
Natural deduction usually has a weak notion of axioms and focuses more on inference rules. Those rules include introduction and elimination rules for each logical connectives. Some metatheorems in Hilbert-style systems, like the deduction theorem, become rules in natural deduction.
Sequent calculus is similar to natural deduction, but has a more "bottom-up" style. In cut-free sequent calculus, a nice property, subformula property, holds, which makes it easy to do automated proof search. Gentzen's cut elimination, a standard result, ensures that any proof using cut can be transformed into a cut-free proof.

We are using Hilbert-style system because it's elegant, it can be easily applied to first-order theories with infinite axioms (since Γ can be any set) and it's easier to do encoding for proofs (since Γ does not change in the proof tree). Moreover, with the help of proof tactics, we are able to write proofs in the style of natural deduction (just as in Lean).

There are formalizations of other systems in Lean, e.g. FFL(lean4-logic) formalizes Tait calculus (a variant of sequent calculus) for first-order logic, and flypitch formalizes natural deduction.

Even within Hilbert-style systems, there are different choices on selecting the axioms and inference rules. The axioms and rules we selected have the following property:

The only inference rule is Modus Ponens (Proof.mp). Some systems (e.g. in Mendelson's book) include a GEN rule to introduce universal quantifiers, but in our system it's a metatheorem (Proof.generalization). Also in such systems, the deduction theorem is restricted (e.g. in Mendelson's system, the deduction theorem for Γ ⊢ p ⇒ q requires no free variable in p used by GEN rule in Γ, p ⊢ q), while ours (Proof.deduction) is not.
The logical axioms do not refer to propositional logic. Some systems (e.g. in Enderton's book) include all propositional tautologies as logical axioms.
Equality axioms are formalized as logical axioms, not as a theory, because we want equality to be a part of first-order logic itself. This also makes prw tactic usable for all first-order theories.
Empty structures are admitted (i.e. ∅ ⊬ ∃ x. ⊤ in general). This thanks to the "dependent type design" of Term and Formula: to prove ∃ x. ⊤ as a Sentence, a closed term t : L.Term 0 is needed for Proof.exists_intro; but in a language with no constants, no closed term exists.

References #

FFL (lean4-logic). https://github.com/FormalizedFormalLogic/Foundation
flypitch. https://github.com/flypitch/flypitch
Introduction to Mathematical Logic (fourth edition), Elliott Mendelson.
A Mathematical Introduction to Logic (second edition), Herbert B. Enderton.