Soundness of first-order natural deduction with respect to Tarski satisfaction

Identifier: F:fo-soundness
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

If a formula is derivable from a context in the first-order natural-deduction calculus FO.Provable, then in every structure and at every valuation satisfying the context, the formula is satisfied. The calculus has the eleven intuitionistic propositional rules plus universal and existential introduction and elimination and reflexivity of equality; the semantics is the constructive Prop-valued Tarski definition.

Formal statement

theorem FO.soundness : ((x0 : Sort (1)) -> ((x1 : FO.Structure x0) -> ((x2 : FO.Context) -> ((x3 : FO.Formula) -> ((x4 : FO.Provable x2 x3) -> ((x5 : ((x5 : AxNat) -> x0)) -> ((x6 : FO.ctxSat x0 x1 x2 x5) -> FO.sat x0 x1 x3 x5)))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

1 direct dependencies 6 direct dependents

Evidence

kernel-FO.soundness

Kind: kernel-term
Status: checked

Supports: FO.soundness is admitted by the trusted kernel gate with the type recorded in formal.statement, and rests on no axiom. The proof is an application of FO.Provable.rec with one minor premise per rule -- sixteen of them -- so the prelude does not build unless every rule's case type-checks. A skipped case is not possible: the recursor's arity fixes the count.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example fo_soundness_inventory -- FO.soundness --exact --require-axiom-free

Evidence notes

The checker FAILS on absence rather than reporting an empty set: a named filter matching nothing exits 1 with 'an absent declaration is a failed check, not an empty report'. --exact matches the whole name, so this row checks FO.soundness and not the FO.sound* family. formal.statement is Kernel::render_lean of the admitted type, taken verbatim from that command's stdout. Declared in crates/axeyum-lean-kernel/src/fo_soundness.rs by declare_soundness.

statement-is-the-one-claimed

Kind: kernel-term
Status: checked

Supports: The theorem's inferred type is rebuilt in the test module from FO.Provable, FO.ctxSat and FO.sat and compared by Kernel::def_eq, so a soundness theorem that landed at a weaker-but-still-provable statement fails. The same test asserts the context-free variant -- 'Provable g p -> forall w, sat p w', which is FALSE since Provable (cons a nil) a holds for every a -- is NOT def_eq to what was proved.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_soundness::tests::soundness_states_the_theorem_it_claims --test-threads=4

Evidence notes

A theorem's statement is what the ledger claims; without this row the fact would rest on a rendered string nobody compared against a rebuilt term.

soundness-applies-to-a-real-derivation

Kind: kernel-term
Status: checked

Supports: POSITIVE CONTROL. A soundness theorem quantified over an inhabited-looking but unusable family would still admit. FO.provable_all_imp_ex is a genuinely first-order derivation -- (forall x. R(x)) -> (exists x. R(x)), built from all_elim and ex_intro at the same instance term -- and pushing it through FO.soundness at the concrete ℕ structure yields a term whose inferred type is exactly the satisfaction of that implication.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_soundness::tests::soundness_applies_to_the_first_order_example_derivation --test-threads=4

Evidence notes

Three example derivations are landed in fo_provable.rs and between them exercise all_intro, all_elim and ex_intro. FO.Provable is an inductive relation, so 'it type-checks' does not imply it is inhabited by anything interesting.

eigenvariable-condition-is-load-bearing

Kind: kernel-term
Status: checked

Supports: all_intro's premise is a derivation over FO.Context.shift g, not over g -- the de Bruijn form of 'the generalized variable is not free in the context'. The rule's inferred type is rebuilt in the test module and compared against the variant with the shift removed, which is the unsound rule (it derives forall y. p(y) from p(x)); the two must NOT be def_eq. ex_elim gets the same treatment on both of its shifts.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_provable::tests::all_intro_quantifies_over_the_shifted_context fo_provable::tests::ex_elim_shifts_both_the_context_and_the_conclusion --test-threads=4

Evidence notes

MUTATION-VERIFIED. See the fact notes for the measured kill counts of the two mutations lane model-theory ran: deleting the shift from all_intro, and making FO.sat's existential clause read the outer valuation.

ctx-sat-shift-instantiates

Kind: kernel-term
Status: checked

Supports: The bridge lemma the all_intro and ex_elim cases both consume: satisfaction of a context at w gives satisfaction of the SHIFTED context at Val.cons M a w. It is a Context.rec induction with two cases, and both are exercised -- at the empty context and at a one-entry one -- rather than only the whole lemma being admitted.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_soundness::tests::ctx_sat_shift_instantiates_at_nil_and_at_a_cons --test-threads=4

Evidence notes

The cons case is one application of FO.sat_shift's backward direction; the nil case is True.intro, since ctxSat of the empty context iota-reduces to True.

footprint-whole-fo-package

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- and not only for the headline theorem. All 76 declarations the FO package adds on top of the Nat prelude (the Term and Formula syntax with their recursors, the Structure record and its five projections, the substitution and valuation operations, the Context type, the Provable relation with its sixteen constructors and its recursor, the natStructure, and every theorem above) have an empty Kernel::axiom_footprint.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example fo_soundness_inventory -- --require-axiom-free --expect-count 76

Evidence notes

The row set is a SET DIFFERENCE against a kernel carrying only build_nat_prelude, recomputed on every run, so it is derived from the environment rather than from a hand-maintained list -- a declaration nobody remembered to list still appears. --expect-count fails on drift in EITHER direction, so a declaration silently disappearing is a failure too. Measured 2026-09-05: '76 FO declarations' and 'axiom-free: yes (76 declarations checked)'.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum-lean-kernel build_fo_soundness_prelude, lane model-theory (W3-6, ADR-1636)",
  "source": "authored from the roadmap item; the statement is written here, not extracted",
  "prior_art": [
    {
      "who": "Alfred Tarski; Gerhard Gentzen",
      "what": "the satisfaction definition and the natural-deduction calculus; soundness is the textbook induction on derivations",
      "year": 1935,
      "where": "Tarski, 'Der Wahrheitsbegriff in den formalisierten Sprachen' (1935); Gentzen, 'Untersuchungen ueber das logische Schliessen' (1935)",
      "attribution": "standard textbook attribution; this lane did not consult the primary sources"
    }
  ]
}