[FOM] Formation Rules

[Neil Tennant]

On Mon, 16 Oct 2006, Edwin Mares wrote:

> Who was the first logician to present rigorous formation rules for
> a formal language? And where (and when) did they do it?   

Ed,

I hope the following cut-and-paste from a work in progress might help.
I'm afraid that all the LaTeX formatting commands are included.

Neil

_______________________________

This survey of the literature is by no means exhaustive, but it does cover
many of the titles with which the reader is likely to be familiar.

Some early classics do not so much as contain a definition---rigorous or
otherwise---of the notion of sentence in a formal language. Among these
are Hilbert and Ackermann  \cite{hilbert_ackermann1950},  Lewis and
Langford \cite{lewis_langford1932}, Tarski \cite{tarski1965},
\mbox{Carnap~\cite{carnap1957}}, Quine \cite{quine1950}, Suppes
\cite{suppes1957} and Goodstein \cite{goodstein1961}.

Works that provide an inductive definition with conditional (not:
biconditional) inductive clauses, but that omit explicit formulation of a
closure clause, include Jeffrey \cite{jeffrey1967}, at p.~13; Shoenfield
\cite{shoenfield1967}, at p.~15;\footnote{In fairness, it should be
pointed out that the author writes `Corresponding to these two generalized
definitions [of `term' and `formula'] we have forms of proof by
induction.' This could be construed as a gesture towards the need for a
closure clause. } Kalish, Montague and Mar \cite{kalish_montague_mar1980},
at p.~4;\footnote{In fairness, it should be pointed out that the authors
write `the class of symbolic sentences can be {\em exhaustively\/}
characterized' [emphasis added] by the basis clause and the inductive
clauses in conditional form.' This too could be construed as a gesture
towards the need for a closure clause. }; Goldfarb \cite{goldfarb2003}, at
p.~80;\footnote{In fairness, it should be pointed out that the author
writes `Our \ldots formal language['s] \ldots formulas are the
truth-functional schemata constructed from the sentence letters by means
of the two connectives ``--" and ``$\supset$".' This too could be
construed as a gesture towards the need for a closure clause.} and Hedman
\cite{hedman2004}, at~p.~2.\footnote{In fairness, it should be pointed out
that the author writes `The syntax of propositional logic tells us which
strings of symbols are permissible as formulas.' This too could be
construed as a gesture towards the need for a closure clause. }Just on the
fringe of this company is Quine~\cite{quine1940}, at~p.~73, whose
definition of formulae reads `\ldots we are to think of the totality of
formulae as comprising some manner of {\em atomic formulae\/}---formulae
containing no shorter formulae as parts---and in addition {\em just\/} the
expressions thence constructible by continued application of joint denial
and quantification.' [Second emphasis added.]

Works that provide an inductive definition with conditional (not:
biconditional) inductive clauses, and that mention closure explicitly,
include 
Church \cite{church1951}, at p.~70; Kleene \cite{kleene1952}, at p.~72;
Enderton \cite{enderton1972}, at p.~20; Crossley at al.
\cite{crossley1972}, at p.~12; Mendelson \cite{mendelson1979}, at
pp.~46-7; Tennant \cite{tennant1978eup}, at pp.~19, 89; Allen and Hand
\cite{allen_hand1992}, at pp.~5--6; and Boolos, Burgess and Jeffrey
\cite{boolos_burgess_jeffrey2002}, at pp.~106--7.

There are also texts in mathematical logic that treat inductive
definitions as though they are definitions of a particular kind of
set---the intersection of all classes (of finite strings of symbols) that
contain the atomic sentences and are closed under the operations for
forming compound sentences. Such an approach, of course, presupposes a
great deal of set theory, thereby making the circularity problem acute.
Among such treatments is Monk \cite{monk1976}, at~p.~116. Enderton
\cite{enderton1972} also gives this set-theoretic version of the
definition, calling it `top down' (as opposed to the non-set-theoretic
method of inductive definition, which he calls `bottom up'). 

END