|
|
 | | From: | Leonid Portnoy | | Subject: | Can we have Second Order Logic expressibility in FOL? | | Date: | Sun, 23 Jan 2005 11:49:02 GMT |
|
|
 | If we can axiomatize set theory in FOL using ZFC, then it seems we can
quantify over sets, and thus over relations and functions since they
are sets. But isn't this the domain of second order logic - to be able
to quantify over predicates (i.e. relations)?
In particular, why can't we express things like graph reachability in
FOL by defining the transitive closure of a graph (by saying
Ap edge(x,y)->P(x,y) ^ ...
where p is a set representing transitive closure).
Or, why can't we represent mathematical induction:
Ap (P(0) ^ Am P(m)->P(m+1)) -> AnP(n)
where again p ranges over all functions [which are sets defined in FOL
via ZFC].
Thanks,
Leonid Portnoy
|
|
| | From: | George Cox | | Subject: | Re: Can we have Second Order Logic expressibility in FOL? | | Date: | Sun, 23 Jan 2005 14:41:27 +0000 (UTC) |
|
|
| Leonid Portnoy wrote:
>
> If we can axiomatize set theory in FOL using ZFC, then it seems we can
> quantify over sets, and thus over relations and functions since they
> are sets. But isn't this the domain of second order logic - to be able
> to quantify over predicates (i.e. relations)?
>
> In particular, why can't we express things like graph reachability in
> FOL by defining the transitive closure of a graph (by saying
>
> Ap edge(x,y)->P(x,y) ^ ...
>
> where p is a set representing transitive closure).
>
> Or, why can't we represent mathematical induction:
>
> Ap (P(0) ^ Am P(m)->P(m+1)) -> AnP(n)
>
> where again p ranges over all functions [which are sets defined in FOL
> via ZFC].
There is a difference between
"... for all P, x in P ..." (set theory's way)
and
For all formulae P: "... P(x) ..." (FOL's way).
In the first case "all P" means all sets P of which there are presumably
a lot, certainly uncountably many. In the second case "all formulae P"
just means countably many. This distinction is often discussed in
respect of second and first order statements of induction in Peano
arithmetic.
Note that "... for all P, x in P ..." is a single statement of set
theory but 'For all formulae P: "... P(x) ..."' is a scheme of
infinitely many formulae of FOL.
|
|
| | From: | Torkel Franzen | | Subject: | Re: Can we have Second Order Logic expressibility in FOL? | | Date: | 23 Jan 2005 13:10:06 +0100 |
|
|
| lp178@columbia.edu (Leonid Portnoy) writes:
> If we can axiomatize set theory in FOL using ZFC, then it seems we can
> quantify over sets, and thus over relations and functions since they
> are sets. But isn't this the domain of second order logic - to be able
> to quantify over predicates (i.e. relations)?
In first order logic, we can quantify over anything as long as it's
an individual. Here "individual" doesn't mean anything in particular,
and there is nothing to stop a domain of individuals from containing
sets of individuals.
> In particular, why can't we express things like graph reachability in
> FOL [...]
Because what is meant by a property of a structure being definable
in first order logic is that there is a set M (finite or infinite
depending on what notion we are talking about) of sentences such that
for any structure K, K satisfies the sentences in M if and only if K
has the property. Similarly for first order definability of relations
between individuals in a domain.
|
|
| | From: | Pierre Asselin | | Subject: | Re: Can we have Second Order Logic expressibility in FOL? | | Date: | Sun, 23 Jan 2005 20:59:33 +0000 (UTC) |
|
|
| Hmmm, posted to 2 groups, followups to the 2 groups...
Leonid, please edit the Followup-to line to continue. You have
our attention now.
In sci.logic Leonid Portnoy wrote:
> If we can axiomatize set theory in FOL using ZFC, then it seems we can
> quantify over sets, and thus over relations and functions since they
> are sets. But isn't this the domain of second order logic - to be able
> to quantify over predicates (i.e. relations)?
> [ snipped example from graph theory ]
> Or, why can't we represent mathematical induction:
> Ap (P(0) ^ Am P(m)->P(m+1)) -> AnP(n)
> where again p ranges over all functions [which are sets defined in FOL
> via ZFC].
Because that's just passing the buck. First let's rewrite your
induction principle in set notation,
AP (0\in P ^ Am (m\in P -> (m+1)\in P)) -> N \subset P
This is a single sentence in set theory, but to apply it to specific
cases where you prove that every natural number has some property,
you first have to prove the existence of the set P of of all things
that have the property. To do this, you have to rely on axioms
and axiom schemas formulated in first-order logic and this is where
the limitations come back.
A more subtle phenomenon occurs if you try to use the above as a
second-order-ish definition of the natural numbers ("N is the
smallest set containing zero and closed under successor"). The
quantifier on P looks right, but it is weaker than intended because
your set theory based on first-order logic does not "see" all the
sets. As a result, your theory (if consistent, blah blah blah)
has nonstandard models with hyperfinite natural numbers.
--
pa at panix dot com
|
|
| | From: | David C. Ullrich | | Subject: | Re: Can we have Second Order Logic expressibility in FOL? | | Date: | Sun, 23 Jan 2005 07:51:27 -0600 |
|
|
| On Sun, 23 Jan 2005 11:49:02 GMT, lp178@columbia.edu (Leonid Portnoy)
wrote:
>If we can axiomatize set theory in FOL using ZFC, then it seems we can
>quantify over sets, and thus over relations and functions since they
>are sets. But isn't this the domain of second order logic - to be able
>to quantify over predicates (i.e. relations)?
>
>In particular, why can't we express things like graph reachability in
>FOL
I _think_ it's correct to say that we can indeed express something
like that in first-order _set_ theory, but not in first-order
_graph_ theory (which is what is meant when people say that it
can't be done.)
>by defining the transitive closure of a graph (by saying
>
> Ap edge(x,y)->P(x,y) ^ ...
>
>where p is a set representing transitive closure).
>
>Or, why can't we represent mathematical induction:
>
> Ap (P(0) ^ Am P(m)->P(m+1)) -> AnP(n)
>
>where again p ranges over all functions [which are sets defined in FOL
>via ZFC].
>
>Thanks,
>Leonid Portnoy
************************
David C. Ullrich
|
|
|
