[FOM] Concerning definition of formulas
Allen Hazen
allenph at unimelb.edu.au
Sun Sep 30 02:23:05 EDT 2007
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
More information about the FOM
mailing list