2 views

Skip to first unread message

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.

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?

> 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

Oct 5, 2004, 1:34:37 PM10/5/04

to

>"... but one needs second-order logic to assert the least-upper-bound

>property of the real numbers ..."

>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

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

Search

Clear search

Close search

Google apps

Main menu