# [FOM] Query for Martin Davis. was:truth and consistency

Sun Jun 15 11:35:05 EDT 2003

```Robin Adams wrote:

I was trying to show that,
> if one is allowed to reason *about* formal systems, not just within them,
> then one can do number theory; one can read number theory as statements
> about a formal system N, not merely the derivation of strings within the
> formal system PA.  Your answer seems to be that it is illegitimate to
> reason about formal systems; what seems to be reasoning about formal
> systems should be read just as the derivation of strings within another
> formal system, such as ZF (the metatheory).  Have I understood you
> correctly?

Of course, we can reason about a formal system informally, say,
about the intuitive meaning of its axioms and rules, how they
are related to the reality (if some applications are assumed).
But when you introduce your formal system like N for numerals
(0 is a numeral, and if n is a numeral then n' is numeral) and
additionally say that the set of numerals is the least one
satisfying the above rules, then it is required to fix a set
theory where this phrase makes sense. Then you can derive in
should be precise. Also we should not allow a reasoning based
on a vicious circle.

>From your question and the previous message I could conclude
that you want to reason about a formalism quite informally,
freely using even the concept of an (infinite) set. I insist
that such a liberty in understanding what is a metatheory
is not allowed. This may lead to a big mess, at least to
misunderstanding between people. (For example, I am not sure
that I understand you well.)

>
> If so, why am I not allowed to reason about formal systems the way I
> reason about any other activity?  When playing chess, if I am left with a
> king and two knights, I am able to deduce that, no matter what moves I
> make, I will never be able to produce a position in which my opponent is
> checkmated.  Likewise, when deriving strings in N, I am able to deduce
> that, whatever string I produce, I will be able to produce a longer string
> that is prime, in the sense I defined above.  Why not?  Or is it your
> position that I can only reason about chess within some formal system,
> too?

You are using the term "deduce" about chess. This means that,
explicitly or not, your reasoning about chess is based on a formal
theory, at least on a formal logic. The precise details of this
formal theory may be not very important. But some evidently could
be fixed. For example, PA can be used to deduce theorems about chess
(but FOL is also appropriate). If your term "deduce" does not mean
anything like this and you are unable in principle to produce a formal
system where you "deduce" something about chess then do not use this

>
> Turning the question round, suppose one does maintain the discipline of
> only ever doing the metatheory of one system within another; say, one
> considers the metatheory of PA as formalised within ZF.  How does the
> derivation of strings within ZF tell us anything about PA?
>
> For example, I have read and understood the proof of Godel's theorem, and,
> since I believe PA is consistent, I now believe that PA is incomplete.
> Let us even say I perform the Herculean labour of writing down the Godel
> sentence G as a string of PA.  Now, I think that I have proved that it is
> impossible to prove G in PA --- `prove' in the same sense that I can prove
> a checkmate impossible from a given chess position, or a Rubik cube
> impossible to solve from a given position.
>
> However, according to you, what I have really been doing is deriving
> strings in ZF.  Well, why should the fact that
>
> The string ~(PA |- G) is derivable in ZF
>
> cause me to believe that
>
> The string G is underivable in PA
>
> ?  These are not the same statement.  How do I infer the second from the
> first?

This is the question on applied mathematics in this concrete
situation.

The formal sentece ~(PA |- G) derivable in ZF may be rewritten
as an equivalent simple universal formula about finite (in the
sense of ZF) derivations in PA ("each derivation in PA has not
G as the last formula"). We have informal semantics (intution)
of ZF which agrees in the case of small finite sets representing
strings of symbols (derivations in PA) with the real (feasible)
strings of simbols. This way we come to the conclusion that the
string G is (physically) underivable in PA. However, strictly
speaking, we have no guarantee that ZF or PA are really consistent
formalisms, and the above conclusion may be in principle falsified
(as classical mechanics was falsified by some experiments).
However, to this moment ZF and PA seem sufficiently reliable
and based on a sufficiently coherent (although vague) intuition
on sets and numbers formalized in these theories. (No assumption
on any "standard" models for ZF or PA is made.)

>
> To summarise: if I am allowed to reason about formal systems, then I
> maintain my position that number theory is better read as reasoning
> *about* N, rather than reasoning *within* PA.  If I am not allowed to
> reason about formal systems, then how can metatheory ever be useful?

Mathematical reasoning *about* N is (explicitly or not) a reasoning
*within* PA or ZF or any other appropriate formal (meta)theory of
your formalism N for numerals. I do not understand why are you
trying to avoid this "within". Any rigorous mathematical proof
may be eventually considered as a proof *within* a formal system.
This is the nature of mathematics. This distinguishes it from
any other science or activity and may be considered as the main
point in a definition what mathematics is.

Additionally, we may use some informal reasoning, like that above,
when we want to apply our theory to the physical reality. But this
informal reasoning is analogous to that used in (simple) physics.
(Nothing about standard model of PA or arbitrary sets, large
cardinals, etc. having no real, physical sense.)

I would suggest you another test question (to mutually understand
your and my positions). Let us assume we have a (feasible and
formal) proof in PA that there exists a formal proof in PA of a
theorem. How do you think, in which sense this theorem may be
considered as proved?

Another question: Let us assume we have a (feasible and formal)
proof of a tautology in FOL based on the Gentzen's sequent
calculus with the cut rule. Does it mean that we also have a
proof of this tautology in FOL withot the cut rule? (You know,
there is a cut elimination (meta)theorem and even a cut
elimination algorithm.)

>
> --