[FOM] Formation Rules

[Neil Tennant]

This is a continuation of my response by cut-and-paste to Ed Mares's
question about formation rules.

Neil Tennant

________________________________________________

It is only when well-foundedness is somehow ensured for a chosen kind $K$
of inductively definable entities that one can take the liberty of
`inductively' defining, by means of the appropriate general equivalence,
yet further predicates whose extensions are to lie wholly within $K$. 

Such, for example, was Tarski's method in his celebrated paper
\cite{tarski1936}, `The Concept of Truth in Formalized Languages'.
...
Axioms (I)--(V) of Tarski's paper
(pp.~173--4) ensured the well-foundedness of `expressions', i.e., finite
strings of certain expressions specified as basic. Compound expressions
could be generated only by juxtaposition (concatenation) of expressions.
Axiom (V), a very powerful class-theoretically formulated induction
principle, ensured that the resulting strings would be of finite length.
Having thus ensured well-foundedness (and unique composition) of
expressions, Tarski was subsequently able to afford himself the luxury of
defining the notion of sentential function (Definition 10, p.~77), and
then the notion of the satisfaction of a sentential function by an
infinite sequence of objects (Definition 22, p.~193), by employing the
appropriate {\em general equivalences}, rather than by inductive
definitions in the canonical form of a basis clause; one-way conditional
clauses for compound cases; and a closure clause. In the context of the
foregoing considerations, one reads with renewed appreciation Tarski's
careful concern to stress, at p.~174, n.~1, that his axiom system for
expressions was categorical. Had it not been, then Tarski's subsequent
definitions {\em via\/} general equivalences of the notions of sentential
function and of satisfaction would have been bedevilled by a problem
analogous to that ... for the attempt to define the
natural-number predicate $N$ by means of the general
equivalence.\footnote{Not so fortunate is the definition of the notion of
formula to be found in Grandy~\cite{grandy1977}, at p.~1, which employs a
general equivalence within a domain of (undefined) {\em symbol sequences},
which are not specified as being finite.}