[FOM] Question about Set Theory as a formal basis for mathematics
Andrej Bauer
Andrej.Bauer at literal.si
Mon Feb 27 12:14:16 EST 2006
Dear Andrea,
here is a computer sciency point of view.
Firstly, ZFC is a formal system. It is a description of:
- which finite strings of symbols represent formulas (the grammar) - what
are the allowable rules for manipulating formulas (the production rules
for provable statements)
The axiom system is thus very much like a programming language: a bunch of
rules on how to manipulate strings of symbols. There is nothing sinister in
the _formulation_ of ZFC. In order to prove theorems of ZFC you need not know
any semantics or model theory. In fact, you can write a program which
searchers for a proof of any statement in ZFC and finds it if there is
one. I
think this proves that the formal system ZFC is well defined and involves no
circularity.
Things get interesting when we ask "what does ZFC mean"? There I think two
answers are important:
1) ZFC is usually accompanied by an _informal_ description of what its axioms
are about. This description relies on the fact that most people have some
idea of what "sets" are. A mathematician who works with ZFC for a while
will
develop intuitions about it. Even more, many mathematicians will claim that
ZFC precisely matches their idea of sets. This might be so because ZFC was
very cleverly chosen. This kind of meaning is not strictly mathematical, of
course, but the point is that mathematicians "understand" ZFC even if they
know no model theory or semantics.
2) We may also ask about a _mathematical_ meaning of a first-order theory.
Mathematicians (Tarski) invented "model theory" to answer this question.
Roughly speaking, a model of a first-order theory is a certain kind of
set-theoretic structure. As we immediately notice, model theory uses the
language of set theory, which begs the question: how can we speak about
models of ZFC, if we need ZFC to speak about models in general? This is
your
dilemma. Please note that the dilemma is not about whether the formulation of
ZFC is circular--it isn't--but rather how can we possibly explain the meaning
of ZFC in terms of ZFC.
I think your dilemma may go away after you compare the situation with
programming languages.
As a computer scientist you know well that it is not unusual to have a
programming language P such that it is possible to express an interpreter
for
P in P itself:
"There is a program I in P such that I interprets P." (1)
This in itself is not paradoxical, it is just an interesting form of
circulularity. Of course, you should not attempt to _define_ P in terms of
I,
-- that would be an evil form of circularity.
Similarly, ZFC is a powerful enough formal system so that you can encode
in it
the syntax and proof rules of ZFC. So in ZFC it is possible to _express_ the
statements
"The set M is a model of ZFC" (2)
and
"There is a set M such that M models ZFC." (3)
Compare (3) and (1) above. The fact that we have (2) and (3) in itself is not
paradoxical, it is just an interesting form of circularity. Of course, you
should not attempt to _define_ ZFC in terms of (3), and mathematician's
don't!
By the way, I did not claim that ZFC proves (3). I only claimed that with a
suitable encoding of syntax of first-order logic with sets it is possible to
express (3) in ZFC.
To summarize:
1) ZFC is a formal system which describes how to manipulate strings of
symbols
2) Mathematicians give an informal (but quite precise) meaning to ZFC 3)
Using model theory, mathematicians can use ZFC to study properties of any
system for manipulation of strings of symbols. ZFC is one such example.
We do not need 3) to do 1) and 2). Does this help?
Andrej
More information about the FOM
mailing list