[FOM] Concerning definition of formulas

[Allen Hazen]

Saurav Bhaumik asks about the definition of 
formulas.  Well-Formed Formula is typically 
defined inductively, and inductive definitions 
(since Frege's "Begriffschrift" and Dedekind's 
"What are... numbers") have typically been 
converted into explicit definitions set 
theoretically, the defined class being 
characterized as the smallest class containing 
the base cases of the induction and closed under 
its inductive clauses.  Bhaumik (like such 
earlier philosophers as Poincare and 
Wittgenstein!) sees a potential circularity here: 
we study set theory in terms of a formalized 
axiomatic system whose set of well-formed 
formulas is itself defined in terms of sets!

Andrej Bauer and Richard Heck have already 
responded to Bhaumik's query: I like their 
replies, and this is meant to supplement rather 
than to compete with them!

The attitude you take to a definition depends in 
part on what you want to do with it!  I would 
distinguish two possibilities:

	(FIRST): We want to define the formulas 
of a formal language for a practical reason: 
because we want to start USING the language.  (It 
is, of course, an idealization to think set 
theorists actually communicate by means of 
formulas of the formalized First-Order language 
of ZF, but they DO use them, both as a supplement 
to natural language when a potentially confusing 
point has to be stated, and also as a sort of 
guide: they think of an intuitive statement or 
proof as legitimate if it is (intuitively!) clear 
how to translate it into the formal language or a 
formalized derivation.)  For THIS purpose, we 
don't need to worry about formulating the 
"closure" clause of the definition: in PRACTICE 
we will only have to deal with particular 
formulas, not with the infinite set of all 
formulas, and it is enough that we can 
effectively recognize those formulas which ARE 
generated by the inductive process.  Even 
logicians (Edward Nelson, in his monograph 
"Predicative Arithmetic") comes to mind who are 
sceptical of the meaningfulness of inductively 
defined notions (who are, that is, sceptical that 
the "closure" condition defines a genuine set) 
are happy to use the inductively defined notions 
of formula and derivation in practice.

	(SECOND): We want to define the notion of 
formula for theoretical reasons, because we want 
to prove metamathematical theorems about 
formulas.  Here it IS important that the 
definition be seen as unambiguously defining a 
(potentially) infinite set.  But here again there 
are different attitudes, adopted by different 
logicians or the same logicians in different 
parts of their work.

		(2A)  Inductive Definition 
doesn't HAVE to be converted into explicit 
set-theoretic definition: it is considered 
perfectly legitimate, in some forms of 
constructive mathematics, to introduce a new 
notion by giving an inductive definition.  This 
is independent of set theory, and can be accepted 
by constructivists who are sceptical of set 
theory.  Most of the elementary results of 
logical "syntax," including such powerful results 
as Gentzen's "Hauptsatz," could be formalized  in 
a system like Primitive Recursive Arithmetic, 
which postulates no infinite sets and severely 
restricts the use of quantifiers ranging over 
infinite domains, but allows the introduction of 
new, inductively defined, concepts and the use of 
a principle of induction in reasoning about them. 
(Historical introduction of Primitive Recursive 
Arithmetic, and still a good first thing to look 
at to get a feel for how it works in practice, is 
Skolem's paper of 1923, "The foundations of 
elementary...," which is in J. Van Heijenoort, 
ed., "From Frege to Gödel: a sourcebook in 
mathematical logic 1879-1931."  William Tait 
argued in his paper "Finitism," in the "Journal 
of Philosophy" vol. 78 (1981) that this is the 
most natural understanding of what Hilbert meant 
by "finitistic" reasoning-- Tait's paper is 
difficult but interesting.)

    		(2B) For other theoretical 
approaches-- particularly semantic or 
model-theoretic ones-- it's nicer to have set 
theory.  It is still, I think, not circular to 
use the inductive definition of the First-Order 
language to get started in set theory, and then-- 
after learning to use the language and learning 
what sorts of theorems we can, in practice, give 
formalized (or "in principle" formalizABLE) 
proofs of-- to use set theoretic concepts in 
reasoning about (and proving deeper results 
about, such as the independence proofs) the 
set-theoretic formalism itself... though I think 
the potential circularity here did worry some 
great thinkers of the past!   There is a two-page 
appendix to Quine's (1940; this was not changed 
in the revised edition now in print) 
"Mathematical Logic" that attempts to dispel the 
worry.  For an extended philosophical discussion, 
see Mark Steiner's book "Mathematical Knowledge" 
(Cornell U.P., 1975).

--

Allen Hazen
Philosophy Department
University of Melbourne