FOM: Standards of mathematical rigour and logical consequence

[Vladimir Sazonov]

Charles Silver wrote:
>         Thank you for your long post.  I think I now understand your
> viewpoint better.

You are welcome! 

> 
> V.S:
> > Is FOL
> > "really" complete? (Cf. also my paper in LNCS 118 (1981)).  May
> > be we "really" should have a kind of incompleteness of FOL?  Or
> > should/can we just consistently(?) *postulate* completeness
> > which also seems plausible and is very desirable?
> 
>         I would like to understand in what sense FOL is not "really"
> complete.  

Of course, I consider and practically always use the terms "really", 
"all", "true" and especially "absolutely true" with some irony. 

Completeness or incompleteness should be formulated in a framework 
of a metatheory. The traditional well-known metatheory is ZFC. Here 
completeness of FOL is proved. If we take, say, Bounded Arithmetic 
as metatheory then we are unable even to prove that a complete 
Propositional Calculus exists essentially because in this theory it 
is unprovable the statement EXP which asserts that exponential is 
total function. I consider this feature of BA more realistic than PA. 
Therefore the word "real". 

> Could you please furnish the title and page numbers of your
> article?  Thank you.

"On existence of complete predicate calculus in metamathematics 
without exponentiation", MFCS'81, LNCS N.118, pp. 483-490. 

It is shown that in such a (formally second-order) metatheory 
completeness of FOL is (quite naturally!) equivalent to 
completeness of Prop. Logic. Therefore the problem CoNP=?NP, 
which is "essentially" equivalent to existence of a complete 
Prop. Calculus, is equivalent to the analogous problem of 
completeness for FOL. This means that complexity theoretic 
problem CoNP=?NP has a foundational flavour related not only 
with Propositional Logic. 


Vladimir Sazonov