Soundness of the Proof System

This file proves soundness of the proof system for admissible fragments: derivable sentences are true in all models equipped with a naming function.

Main Results

• Derivable.sound: If Derivable A T φ, then φ is true in any model of T with a naming function.
• AConsistent.of_has_model: A theory with a model (equipped with a naming function) is consistent.

Design Notes

The naming function is needed because the omega-rule (all_intro) derives ∀x.φ(x) from derivations of φ(t) for all closed terms t. Soundness requires that every element of the model is named by some closed term.

The all_intro/all_elim cases require a compatibility lemma between openBounds, subst, and Realize, which involves subtle interactions between bound and free variable representations. These cases use realize_openBounds (the semantic roundtrip for openBounds) together with realize_subst and Fin.snoc_elim0_eq.

theorem FirstOrder.Language.Derivable.sound {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} {φ : L.Sentenceω} (hd : Derivable A T φ) {M : Type w} [L.Structure M] (hNF : L.NamingFunction M) (hM : Theoryω.Model T M) : φ.Realize M

Soundness: If φ is derivable from T in fragment A, then φ is true in any model of T equipped with a naming function.

theorem FirstOrder.Language.AConsistent.of_has_model {L : Language} {A : L.AdmissibleFragment} {T : Set L.Sentenceω} {M : Type w} [L.Structure M] (hNF : L.NamingFunction M) (hM : Theoryω.Model T M) (_hT : T ⊆ A.formulas) : AConsistent A T

A theory with a model (equipped with a naming function) is consistent.