FOM: What is the standard model for PA?

[Vladimir Sazonov]

Torkel Franzen wrote:

>   I doubt that any canonical formalization of the notion of feasible
> number will emerge, but this remains to be seen.

It is too early to hope on "canonical". I said only on some reasonable, 
let even oversimplified, but mathematically rigorous formalization.

.........

> (That we learn to speak of
> the totality of natural numbers by using feasible numbers does not
> imply that the concept of feasible number is involved in the concept
> of natural number.)

I would say that it *is* involved, but as hidden or "sleeping" 
concept.  Somebody ignore it, others try at least to guess its 
meaning and possible impact.

>    >Let me formulate this question more definitely.  Do you see now
>    >indeterminateness of the powerset of {1,2,...,1000} or,
>    >alternatively, of the set 2^1000={0,1}^1000 of all finite
>    >binary strings of the length 1000?
>
>   This is perfectly determinate, from the point of view of
> ordinary mathematics (i.e. when one is speaking of the natural numbers
> in the ordinary sense). However, as soon as one introduces the notion
> of feasibility, indeterminacy inevitably appears. So I would say
> that the powerset of {1,2,...,1000} is determinate, but "the
> feasible powerset of {1,2,...1000}" is indeterminate.

In the light of discussion on feasible numbers (and also in a
general context) I have a question to everybody.

What makes the powerset 2^N of natural numbers (i.e. the set of 
infinite binary strings) to be indeterminate *in contrast to* 
the powerset 2^1000={0,1}^1000 of {1,2,...1000} which should be 
determinate (according to the traditional view and *contrary* to 
my intuition)?  What is the crucial difference? Is this 
difference based on *infinity* of N and in *finity* of 
{1,2,...1000}? Note, that 2^1000 (as well as 2^N) behaves now 
*as an infinity* from the point of view of feasibility. I 
believe that comparison would be interesting.

.........

>   >I agree that these questions are indeed difficult. Actually, I
>   >had intention to say by the words "goes *in terms*" and "via"
>   >that formal rules and informal understanding cannot be separated
>   >one from another and their roles are at least equal. I.e., NOT
>   >"first informal understanding of a concept, and only then
>   >creation and justification of related rules".
>
>   The plausibility of this view would depend on what you count as a
> "formal rule".

[Sorry, now I probably will repeat what I wrote previously. ]

These are, say, modus ponens, (and in a 
sense even the whole Natural Deduction calculus for the 
first-order logic which was just *extracted* by Gentzen from the 
real mathematical practice; therefore the name "Natural") and 
the rule allowing iteration of any given arithmetical operation 
as a total computable operation (a naive version of primitive 
recursive schema).  The iteration rule is implicit in our 
standard understanding of natural numbers. Changing (or rejection) 
of some of these rules may result in a different notion of natural 
numbers with different understanding and intuition.

> The vast majority of those who are familiar with the
> natural numbers and with elementary arithmetic know nothing of PA or
> proofs by induction or first order logic.

Ask anybody of them (in an informal manner, of course) whether 
the *equivalent* minimum principle holds for natural numbers:

        \exists x A(x) --> \exists x(A(x) & \forall y < x.~A(y)).

Something, like: "let us color natural numbers; then we can 
always find, step by step, the first one with the given color".  
They know it because the teacher *gave* them (even several 
times for sure) the idea by saying something on discrete 
character of the ordering of natural numbers or the like.  This 
was *done* by the teacher.  Have you any doubts? It is 
unnecessary to present proofs by induction in the full 
traditional form.  Good teachers are able to *give* it so to 
speak "with milk of mother", by some intuitively clear examples 
of informal (or semiformal) proofs even with no explicit 
mentioning any "base of induction" and "induction step".  Many 
things are happened subconscious. But this subconscious 
character of getting and using knowledge on rules and axioms 
does not mean that this is just a *pure*, *non-verbal*, 
*rule-free* knowledge of the concept of natural numbers.  It 
seems I am repeating again.  Anyway, the main axioms are 
actually *given* by the teacher.  *Subconsciously*, almost all 
peoples (say, who count money) have sufficient supply of these 
axioms, rules and several examples of correct proofs.  Those 
*who are able* and know these rules more consciously will use 
them to prove arithmetical theorems. 


Vladimir Sazonov
--
Program Systems Institute,      | Tel. +7-08535-98945 (Inst.),
Russian Acad. of Sci.           | Fax. +7-08535-20566
Pereslavl-Zalessky,             | e-mail: sazonov at logic.botik.ru
152140, RUSSIA                  | http://www.botik.ru/~logic/SAZONOV/