FOM: RE: Re: SOL confusion

[Harvey Friedman]

Reply to Insall 2:57PM 9/10/00:

>To this end, I would call a
>deductive calculus ``worthy'' if for any formula p, and any finite set S of
>formulas, such that p is a consequence of S, p is deducible from S.  I also
>blundered with the place where soundness should be introduced.  Thus I
>should state the desired result as follows:
>
>For any logic system with a sound and worthy deductive calculus, the
>compactness principle is equivalent to completeness.

Your notion of worthy is often called completeness. And then completeness
for sets of sentences would be called strong completeness.

So in a sound and complete finitary deductive calculus, semantic
compactness is equivalent to strong completeness.

>Would you please tell me:
>1.  Would you consider this an appropriate revision?

Yes, but the hypothesis of completeness is far too strong in the context of
SOL. The set of SOL validities is nowhere near even recursively enumerable.

>2.  Would you say it applies to (``standard'') DSOL?  (By ``standard'' DSOL,
>I mean DSOL with a deduction system designed in essentially the same way as
>``standard'' FOL, with the rule modus ponens, etc.)

SOL is well known not to be semantically compact, and also any complete
deductive system for SOL must be grossly unreasonable.

>3.  I expect it is equivalent to AC or at least to BPI.  Do you agree?

What is "it"? The correct theorem above requires no form of AxC. However,
compactness for arbitrary sets of sentences of FOL does require some form
of AxC.

>4.  What is the use of studying deductive systems that are not ``worthy''?

We have been talking about versions deductive SOL endlessley on the FOM,
none of which are "worthy".

>One might object, saying that it is unclear how to determine when a
>deductive system is ``worthy''.  But in fact, is that not the common design
>when someone seriously considers devising a deductive calculus?

No.