7 Responses to “Peano Axioms and First Order Predicate Logic”

1. admin says:

   February 27 at 4:03 pm

   I found one book called
   "Set theory and logic" and there
   was some discussions on axioms etc.
   but unfortunately I do not remember
   the name of this book.
   

   Pasi

   Peter Edwards (nos…@nospam.nospam) wrote:

   : I am attempting to do some proofs of simple statements using the Peano
   : Axioms expressed in first order predicate logic (FOPL), but I have been
   : having a few difficulties. I would be grateful if anyone could provide me
   : with or at least give me a few pointers towards proving (in FOPL) the
   : statement ’2 is not equal to 1′ using the Peano Axioms.

   : Thanks

   : Pete
2. admin says:

   February 27 at 4:03 pm

   Rustanius Pasi (sip…@cs.tut.fi) wrote:

   : I found one book called
   : "Set theory and logic" and there
   : was some discussions on axioms etc.
   : but unfortunately I do not remember
   : the name of this book.
   

   : Pasi

   Hmmm… the _author(s)_ of this book I mean.

   Sorry,
           Pasi
3. admin says:

   February 27 at 4:03 pm

   Write x’ for the successor of x.  2 is defined as 0” and 1 is defined as 0′.
   

   Assume 2 = 1,
   then 0” = 0′ by defintions.
   Hence 0′ = 0 from the PAAx x’ = y’ -> x = y,
   But 0′ != 0 from the PAAx x’ != 0.
   So we have a contradiction and our assumption is shown to false.
   I.e. 2 != 1.

   Do you want me to translate that into FOPL?

   - Hide quoted text — Show quoted text -

   Peter Edwards wrote:
   > I am attempting to do some proofs of simple statements using the Peano
   > Axioms expressed in first order predicate logic (FOPL), but I have been
   > having a few difficulties. I would be grateful if anyone could provide me
   > with or at least give me a few pointers towards proving (in FOPL) the
   > statement ’2 is not equal to 1′ using the Peano Axioms.
   

   > Thanks

   > Pete
4. admin says:

   February 27 at 4:03 pm

   On Thu, 11 Nov 1999, Peter Edwards wrote:
   > I am attempting to do some proofs of simple statements using the Peano
   > Axioms expressed in first order predicate logic (FOPL), but I have been
   > having a few difficulties. I would be grateful if anyone could provide me
   > with or at least give me a few pointers towards proving (in FOPL) the
   > statement ’2 is not equal to 1′ using the Peano Axioms.

   Hint: Find a property possessed by 1 which is not possessed by 2, or vice
   versa.
5. admin says:

   February 27 at 4:03 pm

   Peter Percival <peter.perci…@cwcom.net> wrote in message

   news:382C6D18.B6179816@cwcom.net…
   

   > Write x’ for the successor of x.  2 is defined as 0” and 1 is defined as
   0′.

   > Assume 2 = 1,
   > then 0” = 0′ by defintions.
   > Hence 0′ = 0 from the PAAx x’ = y’ -> x = y,
   > But 0′ != 0 from the PAAx x’ != 0.
   > So we have a contradiction and our assumption is shown to false.
   > I.e. 2 != 1.

   > Do you want me to translate that into FOPL?

   It would be useful if you could.

   Thanks

   Pete
6. admin says:

   February 27 at 4:03 pm

   - Hide quoted text — Show quoted text -

   Peter Edwards wrote:
   > Peter Percival <peter.perci…@cwcom.net> wrote in message
   > news:382C6D18.B6179816@cwcom.net…
   > > Write x’ for the successor of x.  2 is defined as 0” and 1 is defined as
   > 0′.
   

   > > Assume 2 = 1,
   > > then 0” = 0′ by defintions.
   > > Hence 0′ = 0 from the PAAx x’ = y’ -> x = y,
   > > But 0′ != 0 from the PAAx x’ != 0.
   > > So we have a contradiction and our assumption is shown to false.
   > > I.e. 2 != 1.

   > > Do you want me to translate that into FOPL?

   > It would be useful if you could.

   (1)  AxAy(x’=y’->x=y)       axiom of PA
   (2)  0”=0′->0′=0           from (1) by universal instantiation
   (3)  Ax~(x’=0)              axiom of PA
   (4)  ~(0′=0)                from (3) by universal instantiation
   (5)  ~(0”=0′)              from (2) and (4) by modus tolendo tollens
   (6)  ~(2=1)                 from (5) by the definitions of 1 and 2
7. admin says:

   February 27 at 4:03 pm

   - Hide quoted text — Show quoted text -

   Peter Percival wrote:
   

   > Peter Edwards wrote:

   >> Peter Percival <peter.perci…@cwcom.net> wrote in message
   >> news:382C6D18.B6179816@cwcom.net…
   >> > Write x’ for the successor of x.  2 is defined as 0” and 1 is
   >> defined as
   >> 0′.

   >> > Assume 2 = 1,
   >> > then 0” = 0′ by defintions.
   >> > Hence 0′ = 0 from the PAAx x’ = y’ -> x = y,
   >> > But 0′ != 0 from the PAAx x’ != 0.
   >> > So we have a contradiction and our assumption is shown to false.
   >> > I.e. 2 != 1.

   >> > Do you want me to translate that into FOPL?

   >> It would be useful if you could.

   > (1)  AxAy(x’=y’->x=y)       axiom of PA
   > (2)  0”=0′->0′=0           from (1) by universal instantiation
   > (3)  Ax~(x’=0)              axiom of PA
   > (4)  ~(0′=0)                from (3) by universal instantiation
   > (5)  ~(0”=0′)              from (2) and (4) by modus tolendo tollens
   > (6)  ~(2=1)                 from (5) by the definitions of 1 and 2

   PS, in the end I thought that MTT was better than RAA.