Re: Second-order and Higher-order Logic

Paul Holbach schrieb:
by Herbert B. Enderton:

http://plato.stanford.edu/entries/logic-higher-order

It should probably be said, that the general semantics
is pretty useless for existential quantified predicates
and/or functions. Isn't it?

Because the article says:

"The main feature of the general semantics is a result of
the “nothing but” type: Second-order logic with the general
semantics is nothing but first-order logic (many-sorted)
together with the comprehension axioms. Thus a sentence
is valid in the general semantics iff it is logically
implied (in first-order logic) by the set of comprehension
axioms."

Which somehow implies that in the general semantics
we can define the validity of all types of second order
sentences, but which is not the case in my opinion.

Clearly FOL has a forall semantics when it comes to
predicates and/or functions. In a sentence of the
form:

forall P forall f .... P(x) ... f(x) ...

I can leave out the P and f quantifier, and I am already
done with FOL, and if the P or f occurs once in
the above sentence I can directly use its definition.

If the P and f occur in multiple sentences I have to copy
the definitions and do some renaming, because the forall
quantifications should be independent.

But what if I have a sentence of the following
form?:

... exists P ... P(x) ...

My first intuition is that there is no translation
to FOL, also in the general semantics, when we have
somewhere a definition for P.

Because as soon as we interpret the above sentences
in a first order model M, the P is fixed, but the
sentence asks for a existential quantification of
P, even when all other predicates and functions are
already fixed.

Or is there some trick involved, by unfolding
the definition in case of an existential occurences?
So if it were that we have a definition:

forall y forall x (P(x) <-> A(x,y))

Now the predicate P becomes dependent not only on
the variable y but also on all predicates P1,..,Pn
occuring in A. So if I unfold I am only trading
the predicat P for the predicates P1,..,Pn:

... exists P1,..,Pn,y ... A(x,y) ...

I again arrive at a sentences that is not expressible
in first order logic. Or is the assumption that
the definitions somewhere end in pure variable
definitions, i.e. n=0?

Comments welcome.


Best Regards
.

Quantcast