"... 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
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"?
Interesting question. Peano arithmatic contains the (second order)
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.
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
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
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
A general model, would however, not have that S=P(F).
e.g. F:=R and S:=the definable subsets of R
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.
second order logic is sound, but not complete. it can be considered as just
another system of sets in set theory.
"Zhang" <zxg...@yahoo.com> wrote in message