FOM: Standards of mathematical rigour and logical consequence
sazonov at logic.botik.ru
Mon Nov 2 17:01:15 EST 1998
Charles Silver wrote:
> Thank you for your long post. I think I now understand your
> viewpoint better.
You are welcome!
> > 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"
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.
More information about the FOM