Definition·D084
Formula of a language
A formula is a sequence belonging to every formula-admissible set: the smallest one, built from atomic formulas via negation, connectives, and quantifiers.
For a language
:
In words
A sequence is a formula of L exactly when it belongs to every formula-admissible set: the formulas are the smallest formula-admissible set.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
Existence:
is itself formula-admissible, so Separation carves
out of it, exactly mirroring the construction of Term(L) (itself mirroring the construction of ω). The result does not depend on which formula-admissible set was used to start, by Extensionality, since the displayed condition already forces membership in every formula-admissible set. That
is itself formula-admissible, and is contained in every formula-admissible set, is L63, mirroring L62; this licenses structural induction on formulas, the tool a satisfaction relation will need to be defined by recursion on formula structure.