1. Not finding help here? Sign up for a free 30min tutor trial with Chegg Tutors
    Dismiss Notice
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.
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook

Have something to add?