Lemma·L63
Formula(L) is the least formula-admissible set
The set of formulas is itself formula-admissible, and it is contained in every formula-admissible set: it is built from atomic formulas and nothing more.
For a language
: (i)
is formula-admissible for
; (ii)
for every
formula-admissible for
.
In words
The set of formulas is itself closed under formula formation, and it sits inside every other set with that closure property: it is the smallest one there is.
Rests onF09
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Proof
- 1
- 2
- 3(i), rel clause: for with , and with : every formula-admissible set contains (the rel clause of D083), so this sequence lies in .
- 4(i), neg clause: let . Let be any formula-admissible set; by part (ii), , so . By the neg clause of D083 applied to : . As was an arbitrary formula-admissible set (universal generalization), this sequence belongs to every formula-admissible set, i.e. it lies in .
- 5(i), bin clause: let and . Let be any formula-admissible set; by part (ii), . By the bin clause of D083 applied to : . As was arbitrary, this sequence lies in .
- 6(i), quant clause: let , , and . Let be any formula-admissible set; by part (ii), . By the quant clause of D083 applied to : . As was arbitrary, this sequence lies in .
- 7All five clauses of D083 hold for : it is formula-admissible.
∎
Remarks
The two parts together say
is the least formula-admissible set, the precise sense in which the formulas of
are "atomic formulas, negations, binary connectives, and quantifications, and nothing more". This licenses structural induction on formulas: to prove a property holds of every formula, it suffices to prove it holds of every atomic formula and is preserved by negation, each binary connective, and each quantifier - exactly the same principle for terms, one level up, and proved the same way. A structure and a satisfaction relation are built next, over both terms and formulas, toward Gödel's completeness and incompleteness theorems.