V.Sazonov at csc.liv.ac.uk
Mon Nov 6 13:03:24 EST 2006
Quoting Rupert McCallum <rupertmccallum at yahoo.com> Sun, 05 Nov 2006:
>> The above definition does not require any metatheory. Formal systems
>> are assumed to be considered in a naive manner (to avoid the evident
>> vicious circle) as I described in another recent posting answering to
I think, I should clarify, that no metatheory is necessary to play with
formal rules. Just like children play with Lego, domino, like we use
key to unlock the door etc. ? quite naively.
> But what statements are accepted as known from this naive point of
If you succeeded to derive formally a theorem you definitely know about
this using only a quite naive understanding what your formal system is.
Additionally, you might have some idea what this formal system is
about: you are also able to see (quite informally) that the axiom and
proof rules (roughly) correspond to your imagination on the "world"
this theory is "describing". You will probably conclude that derived
theorems fit well in your picture of this imaginary "world". Otherwise,
if something will go not according to your intuition and expectations
you will think that it is an exception, like well-known counterexamples
in analysis. Most probably, you will not consider these exceptions as
sufficient reason to change the formal system and will learn how to
co-exist with these exceptions. May be you even will eventually find
these exception also natural in a sense. May be the formal system will
somewhat change your intuition and vision of this imaginary "world".
That is normal when your intuition is governed by formal rules.
That is basically all. In this sense formalism is even not about
consistency of the formal systems you are working with. You just see
that it agrees with your imagination (at least to some degree). You can
discuss this with other people by appealing to their intuition.
Probably you will find that you understand one another. Probably the
illusion will appear that you are discussing about "the same" imaginary
world (because you ground your discussion and intuition on the same
formal system or a similar range of formal systems) and because your
fantasies are somewhat related with (or are natural extrapolations
from) our joint REAL WORLD.
If you want to prove consistency of one formal system in another one -
do this as usually. The full existing mathematical practice (and
probably much more) is included in this picture.
Edward Nelson considers the consistency of Robinson Arithmetic to
> be an open problem. Do you?
In principle, any sufficiently nontrivial formal system can be
suspected to be contradictory, even if we have some imaginary world
which this system seemingly describes. But our imagination is, in
general, so vague. In some cases it seems solid enough and we are
inclined to believe that the formal system is therefore consistent. But
nobody can give a full, absolute guarantee. Any proofs of consistency
are based on some other, stronger formalisms. This gives only a
relative guarantee and depends on some (may be subjective) preferences
to consider some theories as having a better intuitive background and
believed as more reliable.
For me personally, it is sufficient to prove consistency of a new
formal system in ZFC. If it seems impossible, the intuition plays the
role of a guarantee.
Another thing, if by some reason I am interested in fantasies of a
special kind such as feasibility.
Supposing a dispute arose between two
> formalists about that issue, wouldn't it have to be settled by a choice
> of metatheory?
If both like the same metatheory. . . But formalist point of view, in
my understanding, is not and should not be related with some specific
preferences to such or other formalisms and intuitions. It is quite a
general view - a full freedom, except always being based on formal
systems (once it is called mathematics, once it is not just a free art).
It seems to me that Nelson's preferences to some formal systems and and
his intuitions on arithmetic are not a direct consequence of his
formalist view on mathematics. Rather formalist view is a necessary (or
desirable) condition for taking his preferences (related with some
doubts in natural numbers). Formalist is not necessarily an
ultrafinitist, or the like. It is just a general view on mathematics in
its widest sense.
This message was sent using IMP, the Internet Messaging Program.
More information about the FOM