Definition·D078
Alphabet of a language
The variables, the eight fixed logical symbols, and a language's own function and relation symbols, combined into one set with no collisions.
For a language
, its alphabet is
where
and
(eight logical symbols, indexed
). Write
,
,
,
for the embeddings of a variable, logical symbol, function symbol, and relation symbol respectively.
In words
The alphabet of a language is the union of its variables, tagged 0, the eight fixed logical symbols, tagged 1, its own function symbols, tagged 2, and its own relation symbols, tagged 3, so the pieces never collide.
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
: variable number
is just the natural number
itself, so there are infinitely many variables, one for each natural number (T20).
(the natural number
, i.e.
) fixes eight logical symbols once and for all, present in every language by convention:
,
,
,
,
,
,
,
(equality).
and
are
's own function and relation symbols (D077).
and
already collide badly as raw sets (
is literally a subset of
, so "variable
" and
would be the very same set without tagging), and nothing stops
or
from containing naturals too; the four tags
, themselves distinct naturals, keep every piece disjoint regardless. This is a direct 4-way tagged union: each piece
is a product, and their union exists by Union - no iterated pairwise disjoint union needed for this specific fixed-size case, though that construction stays useful whenever the number of pieces is not fixed in advance. Terms and formulas over
are built next, as members of
satisfying formation rules, using
etc. to place symbols into the alphabet unambiguously.