[FOM] Question about Set Theory as a formal basis for mathematics

[Andrej Bauer]

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