Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Second-order logic

  1. Oct 11, 2008 #1
    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:
    [tex](\forall s)((s\,\text{is subset of}\,A)\rightarrow(\exists y)(y\,\text{is least element of}\,s))[/tex]
    and (s is subset of A) can be writen as well formed first-order formula with free variables s and A: [tex](\forall x)(x\in s\rightarrow x\in A)[/tex]
    and (y is least element of s) can be writen as well formed first-order formula with free variables s and y: [tex]((\forall x)(x\in s\rightarrow y\leq x))\,\&\,(y\in s)[/tex].
    I think, that written formulla for definition of well ordered set is well formed first-order formula with one free variable A.
  2. jcsd
  3. Oct 11, 2008 #2


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    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)
  4. Oct 11, 2008 #3
    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 :)
  5. Oct 11, 2008 #4

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

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

    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:

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

    Where S is a set
  6. Oct 11, 2008 #5


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    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.
    Last edited: Oct 11, 2008
  7. Oct 12, 2008 #6
    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
  8. Oct 12, 2008 #7
    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
  9. Oct 12, 2008 #8


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    References are easy enough to find. Waste google's time, not mine.
  10. Oct 12, 2008 #9
    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.
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook