Proof that S (the successor function) is, in fact a Function.

In summary: Theorem, also known as the Axiom of Choice, is a fundamental theorem of mathematics that states that every set has a subset that is a union of the members of the set.Many thanks for your help.
  • #1
agapito
49
0
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
 
Technology news on Phys.org
  • #2
Peano Arithmetic is a theory with equality, and $x = y\to Sx = Sy$ is one of the axioms of equality.
 
  • #3
Evgeny.Makarov said:
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
 
  • #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 Wikipedia.
 
  • #5
Evgeny.Makarov said:
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 Wikipedia.

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.
 
  • #6
agapito said:
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.
 
  • #7
agapito said:
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.
 
  • #8
agapito said:
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
agapito said:
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

I posted this same question some time back and it was ably answered by Evgeny and Bachrack. My apologies for this oversight, I should have checked before posting. Agapito
 

FAQ: Proof that S (the successor function) is, in fact a Function.

What is the definition of a function?

A function is a mathematical rule or relationship that assigns a unique output value to each input value. In other words, for every input, there is one and only one corresponding output.

What is the successor function?

The successor function, denoted by S, is a mathematical function that outputs the next number when a natural number (positive whole number) is given as input. For example, S(3) would output 4, since 4 is the next natural number after 3.

How do we prove that S is a function?

To prove that S is a function, we need to show that for every input (natural number), there is one and only one output (the next natural number). This can be done by using mathematical induction, where we show that the successor function holds for the base case (input of 1) and then for the inductive step (input of n+1). This will prove that S is a well-defined function.

Why is it important to prove that S is a function?

Proving that S is a function is important because it is a fundamental building block in mathematical proofs and in the development of number systems. It ensures that the concept of "next number" is well-defined and can be applied consistently.

How does the proof that S is a function relate to other mathematical concepts?

The proof that S is a function relies on the principles of mathematical induction, which is a commonly used proof technique in various branches of mathematics. It also relates to the concept of one-to-one correspondence, as the successor function maps each natural number to a unique next number.

Back
Top