FOM: Re: SOL confusion

[Harvey Friedman]

Reply to Insall 1:18AM 9/10/00:

>Matt:
>I guess I have chosen an unfortunate wording.  What I have felt for several
>years is that all of mathematics can be done using first order logic.

Systems based on first order logic are the standard scientific models of
mathematical practice, and are of course augmented with proper axioms. This
is a very successful scientific model for providing large upper bounds on
extrapolated mathematical practice.

>It
>seems to me that if others either believe this to be true or would like it
>to be true, then they would consider the lack of a set of axioms for
>finiteness in FOL to be a drawback, in this regard.

I don't regard it as a drawback, since it is entirely irrelevant. OK, here
is a relevance: it can be argued that if finiteness had an appropriate
formalization that was externally correct, then all statements of finite
mathematics would be provable or refutable in, say, ZFC, and that would
make the large upper bounds on mathematical practice even larger and more
convincing as upper bounds than they are in reality. But let's work with
reality.

>Perhaps I tried to
>``overload'' the word ``trouble'' with some pre-suppositions I had, in
>particular about the purposes of FOL.

Yes, your pre-suppositions may have to be reconsidered.

>Matt:
>I mean SOL.  Actually, in light of the discussion about ``semantic'' versus
>``deductive'' SOL, I should say ``This is the reason I consider DSOL
>(deductive SOL) to be incomplete.''

Much better. There are too many reasons to consider DSOL incomplete to
begin to list them on the FOM.

>It seems to me
>that in any finitary deductive system, the compactness principle is
>equivalent to the combination of soundness and completeness.

Meaningless or false.

>Thus, if the completeness and soundness principles
>hold, then the compactness principle holds, because of the finitary nature
>of proofs, coupled with the soundness to relate the semantics to the
>deductions.

If compactness means that a set of sentences is deductively consistent if
and only if every finite subset is, then one needs only the finitary nature
of proofs, and no semantical considerations are needed.

If compactness means that a set of sentences is satisfiable if and only if
every finite subset is, then that is a purely semantic assertion involving
no deductive system whatsoever. If it holds, then you can make up any
unsound and incomplete deductive system that you want. So it could not
possibly imply anything about an arbitrary deductive system. For example,
take ordinary predicate calculus, which is well known to have compactness.
Take the deductive calculus to have no axioms and no rules of inference.
This is obviously sound, but incomplete.