Questions on first vs second order logic

2 views
Skip to first unread message

Zhang

unread,
Oct 4, 2004, 3:38:45 PM10/4/04
to
On wikipedia I read

"... first-order logic is strong enough to formalize all of set theory
and thereby virtually all of mathematics. Its restriction to
quantification over individuals makes it difficult to use for the
purposes of topology, but it is the classical logical theory
underlying mathematics ..."

"... but one needs second-order logic to assert the least-upper-bound
property of the real numbers ..."

So I guess the LUB theorem, written in SOL on most college textbooks,
must be able to convert to FOL somehow (like Peano Arithmetic can have
both FOL and SOL formulations). What is the exact FOL expression of
LUB theorem then?

Of course this involves set theory. In first-order ZFC the sets and
elements of set are both treated as individual variables that
quantifiers can apply to. This means the domain of discourse includes
both sets and elements. So an FOL theory on real numbers needs to have
both number and number sets in its domain to express LUB theorem, I
think?

Can anyone provide some online references on how an FOL theory that
can "virtually formalize all mathematics" is build? Since normal
textbooks use a lot of SOL to express important theorems, I wonder how
they look like in FOL? And, is there interesting mathematics (e.g.
analysis or topology theorems that we are familiar with) that can only
be expressed in higher-order logic but not in FOL? How large is that
"virtually all mathematics"?

Thanks.

Tim Mellor

unread,
Oct 5, 2004, 7:45:54 AM10/5/04
to
zxg...@yahoo.com (Zhang) wrote in message news:<627349c8.04100...@posting.google.com>...

> On wikipedia I read
>
> "... first-order logic is strong enough to formalize all of set theory
> and thereby virtually all of mathematics. Its restriction to
> quantification over individuals makes it difficult to use for the
> purposes of topology, but it is the classical logical theory
> underlying mathematics ..."
>
> "... but one needs second-order logic to assert the least-upper-bound
> property of the real numbers ..."
>
> So I guess the LUB theorem, written in SOL on most college textbooks,
> must be able to convert to FOL somehow (like Peano Arithmetic can have
> both FOL and SOL formulations). What is the exact FOL expression of
> LUB theorem then?

Interesting question. Peano arithmatic contains the (second order)
axiom

For every property P, if P(0) and \forall n (P(n)->P(n+1)) then
\forall n P(n)

In first order logic, one trys to incorperate this via the schema that
includes for every formula \psi

(\psi(0) and \forall n (\psi(n)->\psi(n+1))) -> \forall n \psi(n)

In other words, we have replaced induction on all predicates, by
induction on all definable predicates.

Something similar occurs when one considers the first order theory RCF
of the reals. It is true that every _definable_ closed and bounded set
(in any model) has a least upper bound. One can call this "definable
completeness". This is not generally written as an axiom of RCF, but
it follows from the usual axioms. It is, for example, an easy
consequence of o-minimality.

See
http://planetmath.org/encyclopedia/OMinimality.html
for definition of o-minimal. For a real closed field, the definable
sets are the semi algebraic sets.

>
> Of course this involves set theory. In first-order ZFC the sets and
> elements of set are both treated as individual variables that
> quantifiers can apply to. This means the domain of discourse includes
> both sets and elements. So an FOL theory on real numbers needs to have
> both number and number sets in its domain to express LUB theorem, I
> think?

Let me see if I understand what you are proposing. Let L+ be a two
sorted language (field elements F and subsets S) whith the usual order
relation and field operations on F and order/inclusion relations on F
\times S.

The theory of (R,P(R)), would then prove
forall X \in S (if X is bounded above it has a least upper bound)

It would also show that any definable set was "equal" to some member
of S

A general model, would however, not have that S=P(F).
e.g. F:=R and S:=the definable subsets of R

H. Enderton

unread,
Oct 5, 2004, 1:34:37 PM10/5/04
to
Zhang <zxg...@yahoo.com> wrote:
>On wikipedia I read
>"... but one needs second-order logic to assert the least-upper-bound
>property of the real numbers ..."

Depends on the language. Yes, in a language where the variables
range over the set of real numbers and you have symbols for +
and x, the LUB property is second order.

But in the language of set theory (where the variables range over
the universe of all sets and you have a membership symbol), the
set of reals is defined (as in analysis courses) and the LUB
property is first order in the language of set theory.

--Herb Enderton


FiSH

unread,
Oct 6, 2004, 8:40:14 PM10/6/04
to
first order logic, say predicate logic is sound and complete.

second order logic is sound, but not complete. it can be considered as just
another system of sets in set theory.

fish

"Zhang" <zxg...@yahoo.com> wrote in message
news:627349c8.04100...@posting.google.com...

Reply all
Reply to author
Forward
0 new messages