Second-Order Logic: Understanding the Basics

[Semo727]

I have read, that properties of sets such as that every subset has supremum or that set is well ordered cannot be expressed in the language of first-order logic. Well, when I tried to write these things, I seemed to write them in first order language, which really bothers me. So please, tell me, where is the point, where I use something such as quantifying over predicates:
A is well ordered set iff:
(\forall s)((s\,\text{is subset of}\,A)\rightarrow(\exists y)(y\,\text{is least element of}\,s))
and (s is subset of A) can be written as well formed first-order formula with free variables s and A: (\forall x)(x\in s\rightarrow x\in A)
and (y is least element of s) can be written as well formed first-order formula with free variables s and y: ((\forall x)(x\in s\rightarrow y\leq x))\,\&\,(y\in s).
I think, that written formulla for definition of well ordered set is well formed first-order formula with one free variable A.

 

[Hurkyl]

I have read, that properties of sets such as that every subset has supremum

This statement I hear usually made about the arithmetic. One cannot express, the theorem

Every bounded, nonempty subset of the real numbers has a supremum​

in the first-order language of arithmetic. (Because, in this language, a 'set of real numbers' is a first-order predicate)

But if you want to state this theorem in the language of set theory, you can make it a first-order statement, because sets are actual objects in the theory. (And in some sense, set theory itself acts like a higher-order logic)

 

[Semo727]

I really heard this in context of ZF set theory... but maybe it was just some mistake in that text. Now I will maybe think about that this way until I learn more about logic and set theory :)

 

[evagelos]

This statement I hear usually made about the arithmetic. One cannot express, the theorem

Every bounded, nonempty subset of the real numbers has a supremum​

in the first-order language of arithmetic. (Because, in this language, a 'set of real numbers' is a first-order predicate)

But if you want to state this theorem in the language of set theory, you can make it a first-order statement, because sets are actual objects in the theory. (And in some sense, set theory itself acts like a higher-order logic)

1st order real analysis is obtained from the 2nd order version by replacing the completeness axiom with the completeness scheme:


\exists x\forall y( F(y)----->y\leq x)---->\exists x[\forall y( F(y)---->y\leq x) & \forall z(\forall y( F(y)---->y\leq z)---->x\leq z)] ,

one instance for each formula F of the respective 1st order language of analysis,provided that F contains neither x nor z free.


And in 2nd order together with 1st order the completeness axiom can be expressed in the following way:

\forall S{ S\neqΦ, S\subseteq R and S is bounded from above----->\exists x[\forall y( yεS---->y\leq x) & \forall z(\forall y( yεS---->y\leq z)---->x\leq z)]


Where S is a set

 

[Hurkyl]

Of course, none of that affects the fact that the completeness axiom cannot be stated in first-order arithmetic. (Nor is that first-order schema equivalent to the second-order axiom)

And, for the record, real analysis includes a fragment of set theory -- either explicitly by adding sets into the language and axioms, or implicitly via higher-order logic. What you wrote is an axiomization for the first-order theory of real closed fields.

 

[evagelos]

Of course, none of that affects the fact that the completeness axiom cannot be stated in first-order arithmetic. (Nor is that first-order schema equivalent to the second-order axiom)

And, for the record, real analysis includes a fragment of set theory -- either explicitly by adding sets into the language and axioms, or implicitly via higher-order logic. What you wrote is an axiomization for the first-order theory of real closed fields.

What is 1st order arithmetic??Can you do a formal proof in 1st order arithmetic??

so that you can show that you really know what 1st order theories are in general.

Then can you give us a formal proof involving a supremum problem and show us that the two formulas i wrote are not equivalent by using your own formulas.

For example can you give us a formal proof of the following :

Let S be a non empty set of real Nos bounded from above.Let A={as: sεS,a>0}.Then prove
Sup(A)= aSup(S) .Use any formalized formulas you like.

Of course if you wish to do so

 

[evagelos]

What you wrote is an axiomization for the first-order theory of real closed fields.

Please state the definition of a real closed field,because the formulas i wrote are not for the axiomatization of real closed fields as a whole ,but simply the completeness axiom

 

[Hurkyl]

Please state the definition of a real closed field

References are easy enough to find. Waste google's time, not mine.

 

[evagelos]

References are easy enough to find. Waste google's time, not mine.

I don't think you find anywhere in google the formal proof of the problem i presented to you.

I my self have search very thoroughly the internet,because i am very interested in formal proofs in real analysis.

Should you find a site please inform me.