SUO: Re: Peirce's MS 514
Pat,
I agree that there is room for quibbling, especially in notes
that are written quickly without any serious review (which
in fact comes from the responses). I generally agree with
your quibbles, and I'll toss in a couple of my own.
MW>>Well I can see some difference, and that entailment should be
>> >stronger,
>
PH>They should be precisely the same strength, in an ideal world.
Actually, there may be good reasons for allowing incomplete
proof procedures, even in the best worlds we can ever have
(i.e., short of being omniscient).
>The common example of the need for care over the choice of namespace
>is that of Skolem functions, which are 'new' function symbols are
>introduced to replace existential quantifiers, so that one can replace
>(forall (?x) (exists (?y) (R ?x ?y))
>with
>(forall (?x)(R ?x (fun ?x)))
>These are almost the same in meaning, if you think about it, but the
>first does not entail the second because the second one uses a symbol
>which isnt in the namespace of the first one.
Yes, but you could (in a second-order notation) add another
quantifier that ranges over functions:
(forall (?x) (exists (?fun) (R ?x (?fun ?x))))
>John, you might have pointed out that it was also K. Goedel who
>proved the first-order completeness theorem.
Yes, sorry, Goedel (1930) proved the completeness of FOL for
his PhD dissertation, and the next year he proved the
incompleteness of higher order logic.
But then perhaps I should have mentioned that Leon Henkin (1950)
proved the completeness of higher-order logic if you allow
nonstandard models. But that is another story.
John