Results 1 to 4 of 4

Thread: First order logic (maybe linked to Peano axioms)

  1. #1
    Newbie
    Joined
    Dec 2016
    From
    ROmania
    Posts
    2

    First order logic (maybe linked to Peano axioms)

    Hello,

    I was trying to define natural numbers using first order logic in order to use them in an automated theorem prover. The problem is, I am apparently unable to solve the following problem:

    Is it possible to specify, using FOL, that, for example, the only numbers lower or equal than 3 are: 0,s(0) (one), s(s(0)) (two), s(s(s(0))) (three) ?

    Let's assume that the axiom system is made up of the axioms mentioned here (the very first system, the shorter one) (https://en.wikipedia.org/wiki/Peano_..._of_arithmetic), with multiplication removed (not needed at the moment), plus a "lower than or equal" predicate defined something like this \forall x,y \ \rm{leq}(x,y) \Leftrightarrow \rm{natural}(x)\land \rm{natural}(y) \land (\exists a \ \rm{natural}(a) \land (y = x + a))
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor

    Joined
    Apr 2005
    Posts
    18,604
    Thanks
    2604

    Re: First order logic (maybe linked to Peano axioms)

    Can we assume that you are defining "3" to be "s(s(s(0)))"? How are you defining "less than" here?
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Dec 2016
    From
    ROmania
    Posts
    2

    Re: First order logic (maybe linked to Peano axioms)

    Thank you for your answer. I have defined 3 as s(2) and 2 as s(1) and 1 as s(0), but I think I can only do so(assign numbers) for a finite number of terms with the software I am using. The less than or equal definition is at the bottom of the original post. If you are asking for a syrictly less than, I would have said like x\neq y \land leq(x,y). Do you think the definition is wrong for this purpose? Maybe I should have used the successor somehow ? Thank you
    Last edited by PhantomR; Dec 13th 2016 at 12:39 AM.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    Senior Member
    Joined
    Feb 2010
    Posts
    470
    Thanks
    6

    Re: First order logic (maybe linked to Peano axioms)

    Use induction.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. On a discusssion of the Peano axioms
    Posted in the Discrete Math Forum
    Replies: 10
    Last Post: Sep 10th 2013, 08:28 AM
  2. How to write this in first order peano arithmetic
    Posted in the Discrete Math Forum
    Replies: 6
    Last Post: Jul 3rd 2011, 03:23 PM
  3. Replies: 1
    Last Post: Feb 13th 2011, 12:03 PM
  4. Replies: 0
    Last Post: May 26th 2008, 10:16 PM
  5. Express in First Order Peano Arithmetic (FOPA)
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: May 9th 2008, 09:35 PM

/mathhelpforum @mathhelpforum