Facebook Page
Twitter
RSS
+ Reply to Thread
Results 1 to 7 of 7
  1. MHB Apprentice

    Status
    Offline
    Join Date
    Apr 2018
    Posts
    38
    Thanks
    16 times
    Thanked
    1 time
    #1
    In axioms containg S one invariably finds:

    Sx = Sy -----> x = y

    The converse, which characterizes S as a function:

    x = y ------> Sx = Sy

    Is never shown. Neither is it shown as an Axiom of FOL or formal Theory of Arithmetic. From the basic axioms and rules of FOL, how does one go about deriving the latter expression formally? Any help or references appreciated. am

  2. # ADS
    Circuit advertisement
    Join Date
    Always
    Posts
    Many
     

  3. MHB Master
    MHB Site Helper
    MHB Math Scholar

    Status
    Offline
    Join Date
    Jan 2012
    Posts
    2,467
    Thanks
    531 times
    Thanked
    4,393 times
    Thank/Post
    1.781
    Awards
    MHB University Math Award (2018)  

MHB Humor Award (2017)  

MHB Discrete Mathematics Award (2017)  

MHB Chat Room Award (2016)  

MHB Humor Award (2016)
    #2
    Peano Arithmetic is a theory with equality, and $x = y\to Sx = Sy$ is one of the axioms of equality.

  4. MHB Apprentice

    Status
    Offline
    Join Date
    Apr 2018
    Posts
    38
    Thanks
    16 times
    Thanked
    1 time
    #3 Thread Author
    Quote Originally Posted by Evgeny.Makarov View Post
    Peano Arithmetic is a theory with equality, and $x = y\to Sx = Sy$ is one of the axioms of equality.
    Thanks for responding. All descriptions of Peano Arithmetic I have seen indicate only the converse:

    Sx = Sy ----> x=y

    Can you please give me a reference containing

    x=y ----> Sx=Sy

    As a Peano axiom?

    Many thanks again, am

  5. MHB Master
    MHB Site Helper
    MHB Math Scholar

    Status
    Offline
    Join Date
    Jan 2012
    Posts
    2,467
    Thanks
    531 times
    Thanked
    4,393 times
    Thank/Post
    1.781
    Awards
    MHB University Math Award (2018)  

MHB Humor Award (2017)  

MHB Discrete Mathematics Award (2017)  

MHB Chat Room Award (2016)  

MHB Humor Award (2016)
    #4
    In the book

    Peter Smith. An Introduction to Gödel's Theorems. Cambridge University Press: 2013

    the description of BA on p. 62 includes Leibniz’s Law. The axiom you are talking about is its special case. Robinson's Arithmetic and Peano Arithmetic are extensions of BA and so inherit this law.

    Putting it another way, all theories of arithmetic considered in that book are theories with equality. This means that they include axioms that define properties of =. For the list of axioms see .

  6. MHB Apprentice

    Status
    Offline
    Join Date
    Apr 2018
    Posts
    38
    Thanks
    16 times
    Thanked
    1 time
    #5 Thread Author
    Quote Originally Posted by Evgeny.Makarov View Post
    In the book

    Peter Smith. An Introduction to Gödel's Theorems. Cambridge University Press: 2013

    the description of BA on p. 62 includes Leibniz’s Law. The axiom you are talking about is its special case. Robinson's Arithmetic and Peano Arithmetic are extensions of BA and so inherit this law.

    Putting it another way, all theories of arithmetic considered in that book are theories with equality. This means that they include axioms that define properties of =. For the list of axioms see .
    Many thanks Evgeny. My interest in this is having a feel for what would be needed by a machine to perform these proofs. Obviously in that case no amount of metalanguage verbiage would help. A machine would have no way of "knowing" whether a certain symbol represents a function or something else to be able to apply the axioms. As an example, could a Turing Machine be programmed to do it?

    Thanks again for your valuable help.

  7. Indicium Physicus
    MHB Math Scholar
    MHB Ambassador

    Status
    Offline
    Join Date
    Jan 2012
    Location
    Rochester, MN
    Posts
    4,054
    Thanks
    11,785 times
    Thanked
    10,029 times
    Thank/Post
    2.474
    Trophies
    1 Highscore
    Awards
    MHB Chat Room Award (2017)  

MHB Math Notes Award (2016)  

MHB Math Notes Award (2015)
    #6
    Quote Originally Posted by agapito View Post
    In axioms containg S one invariably finds:

    Sx = Sy -----> x = y

    The converse, which characterizes S as a function:

    x = y ------> Sx = Sy

    Is never shown. Neither is it shown as an Axiom of FOL or formal Theory of Arithmetic. From the basic axioms and rules of FOL, how does one go about deriving the latter expression formally? Any help or references appreciated. am
    In Landau's Foundations of Analysis, on page 2, he simply incorporates it into his version of the Peano axiom 2, which he phrases as, "For each $x$ there exists exactly one natural number, called the successor of $x$, which will be denoted by $x'.$" The implication $x=y\implies x'=y'$ is a direct consequence of uniqueness.

  8. MHB Master
    MHB Site Helper
    MHB Math Scholar

    Status
    Offline
    Join Date
    Jan 2012
    Posts
    2,467
    Thanks
    531 times
    Thanked
    4,393 times
    Thank/Post
    1.781
    Awards
    MHB University Math Award (2018)  

MHB Humor Award (2017)  

MHB Discrete Mathematics Award (2017)  

MHB Chat Room Award (2016)  

MHB Humor Award (2016)
    #7
    Quote Originally Posted by agapito View Post
    A machine would have no way of "knowing" whether a certain symbol represents a function or something else to be able to apply the axioms. As an example, could a Turing Machine be programmed to do it?
    Of course. There are programs called interactive theorem provers, or proof assistants, where you can construct proofs in Peano Arithmetic.

Similar Threads

  1. Replies: 6
    Last Post: August 14th, 2015, 00:07
  2. [SOLVED] Proof of a Function
    By eleventhxhour in forum Pre-Algebra and Algebra
    Replies: 15
    Last Post: March 30th, 2014, 16:03
  3. [SOLVED] Hermitian Function Proof
    By Sudharaka in forum Linear and Abstract Algebra
    Replies: 5
    Last Post: November 4th, 2013, 09:05
  4. Totient function proof
    By Poirot in forum Number Theory
    Replies: 3
    Last Post: April 8th, 2013, 08:51
  5. Proof about the continuity of a function of norm
    By ianchenmu in forum Analysis
    Replies: 1
    Last Post: February 4th, 2013, 05:02

Tags for this Thread

Posting Permissions

  • You may not post new threads
  • You may not post replies
  • You may not post attachments
  • You may not edit your posts
  •  
Math Help Boards