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

[Vladimir Sazonov]

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 
this set theory any theorem about your N. Whenever possible we 
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 
term. This is misleading. 

> 
> 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.) 


> 
> --
> Robin Adams


Vladimir Sazonov