Definition·D083
Formula-admissible set
A set of alphabet-sequences that spells out every atomic formula and is closed under negation, binary connectives, and quantification.
For a language
, a set
is formula-admissible (for
)
it is closed under:
In words
A set of alphabet-sequences is formula-admissible when it is closed under: spelling out the equality of any two terms, applying any relation symbol to the right number of terms, negating any formula already in the set, joining any two formulas already in the set with a binary connective, and, or, if-then, or iff, and quantifying any formula already in the set over any variable, with the universal or existential quantifier.
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
spells out
in prefix notation (logical symbol index
is equality, D078); similarly index
is negation,
are
respectively, and
are
. Here
is the singleton sequence,
is concatenation, and
is n-ary concatenation, exactly as for term-admissible sets. Prefix notation needs no parentheses: every symbol has a fixed, known arity - equality and each binary connective take exactly two formulas or terms, negation takes exactly one formula, and each quantifier takes one bound variable plus one formula. The whole ambient set
is itself formula-admissible (every atomic formula and every formula built from its members by these five rules lands back inside it), so formula-admissible sets exist. The formulas of L are the smallest one, exactly as terms are the smallest term-admissible set.