[FOM] N vs. FOL

[Vladimir Sazonov]

Dear Professor Scott, 

Thanks for your reply! 

Dana Scott wrote:
> 
> Vladimir Sazonov wrote (in part):
> 
>   >> Say, PA consists of several axioms and one axiom schema. It is
>   >> based on FOL based on several (schematic) rules. We easily
>   >> understand how to use these rules.  All of this is quite
>   >> concrete, unlike N, which is both illusive and not determined
>   >> enough (as ANY illusion).
> 
> In order to understand fully schematic rules, one has to understand
> syntax.  A theory of syntax 

I doubt that we really need to understand fully the syntax 
in the sense to have corresponding theory of syntax, if we 
only are using the formal rules for concrete deductions. 
We even may have very vague idea about the syntax and formal 
rules (as at school lessons on geometry). We just need 
to be TRAINED enough to make no mistakes in semi-formal 
inferences or to be able to recognize them. We just follow 
unconsciously some formal rules. A logician observing our 
activity will easily recognize this fact. 

It seems this is in a coherence with what you are writing below 
on PARTICULAR proofs. 

(just as arithmetic) could be based on
> finite strings of 0s and 1s under concatenation.  Call this domain B
> (for "binary").  I say, B and N amount to the same thing.
> 
> Now for PARTICULAR strings (formulae) I can see how to operate on them
> following the rules of FOL -- just as I can see how to use the rules
> of arithmetic to operate on certain particular numbers met in everyday
> life in the way we learn in school.  I agree these particullar
> operations are "concrete".  However, for any GENERAL RESULTS, say even
> for the Deduction Theorem, I need some kind of induction principle to
> argue that some desirable property holds for ALL (provable) formulae
> -- just as I need induction to prove in PA that, say, addition is
> associative and commutative.

Completely agree, except some subtlety about identifying (binary) 
B with (essentially unary, based on the successor operation) N. 
This subtlety can be seen in the framework of Bounded Arithmetic 
where exponential required for this identification is not 
provably total. Here N is rather (unary) part of B. Of course, 
in the framework of PA this subtlety disappears, or arises only 
in complexity theoretic considerations. 

As to Deduction Theorem, we may take FOL in the form of Natural 
Deduction, may be extended by some formal rules for abbreviations 
to work with this system with sufficient comfort. 

> 
> Yes, I have gone up to the metalanguage here in discussing the
> formalization of theories.  But if B is "illusive and not determined
> enough", what justifies my using these syntactical arguments?

When we are using some PARTICULAR mechanical devices, like 
bicycle or any other, the justification is just the fact that 
we are moving much more fast than without any device. We need 
no (meta) theory of bicycles or mechanical devices for that. 
The same with the formal rules of FOL. 

This does not mean, of course, that I have something against 
metatheory for FOL or against model theory for FOL. This is 
a separate story. 

> 
> I sense an infinte regress.

A good point! I would also say, the crucial one. 


Vladimir Sazonov