Definition·D090
Formula parse balance of an alphabet sequence
The same running parse-balance idea as for terms, extended to also account for equality, relation symbols, connectives, and quantifiers.
For a language
and
, define
by
The formula parse balance of
is the function
characterized by
and, for every
:
In words
At each position, the step contribution is the number of pieces the symbol found there still demands: the arity of a function or relation symbol, two terms for equality, one formula for negation, two formulas for a binary connective, one variable and one formula for a quantifier, or zero for anything else. The balance starts at one - one formula is needed overall - and reading one more symbol removes one pending need and adds back however many new pieces that symbol demands.
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
Exactly the term parse balance's recursive shape, with the weight function extended to cover the logical symbols and relation symbols that occur in formulas but never in bare terms. For
built entirely from variable and function symbols (no logical or relation symbols),
agrees with the term weight
symbol for symbol, so
throughout - in particular, T31 applies unchanged to any term regarded as a sequence here. Existence and uniqueness of
, for fixed
, is the recursion theorem exactly as for
(D088).