FST and SND operations in language of elementary arithmetic.

Question

I'm trying to figure out this problem, without any luck now. Maybe you can help me. Suppose we have a first order logic with functions and predicates. We pick a signature, that consists of operation symbols: S^1, +^2, *^2 and a predicate symbol =^2(symbol and number or arguments).

We pick the natural implementation for this symbols, and we only work on natural numbers, including zero.

Now we can do things like this:

nonZero(n) := exists x. S(x) = n
isZero(n) := !nonZero(n)
isOne(n) := exists x. S(x) = n \/ isZero(x)
lessOrEqual(a,b) := exists y. a + y = b
divides(a,b) := exists y. a * y = b

And so on. Also I have the Gödel's β function available, S(x,c) which can map any finite sequence to constance c.

This thing might be called Peano arithmetic, but I'm not sure about this.

Suppose we have this function:

pair(x,y) := (x + y) * (x + y) + x

which works kinda the same as an operation symbol.

I need to create two other functions, fst and snd so that fst(pair(x,y)) = x and snd(pair(x,y)) = y

I thought that I can do it like this:

isFst(x, c) : exists b. (b * b <= c) & (Sb * Sb > c) & (b * b + x = c)
isSnd(y, c) : exists b. (b * b <= c) & (Sb * Sb > c) & exists x. isFst(x, c) & (x + y = b)

But it does not hold the equations above.

Can you help me? Maybe I'm missing something.

EDIT:

Firstly, I'm not good at this. Second, I don't know exactly, what my prof wants. From my perspective we have a function

pair(x,y) = (x+y)*(x+y)+x

which takes two numbers, and returns one. It works like a a+b function, which takes two numbers and returns a single one.

On the other hand, isFst is a predicate. It takes two numbers and returns TRUE or FALSE.

But I think, that I was given a task to make a function fst that takes one number and returns one number.

When I said that equation does not hold, I meant that isFst takes two arguments, but fst takes only one.

Then I thought that I can do it like this:

isFst(x,pair(x,y)) which is actually the same as fst(pair(x,y)) = x, so the predicate will be fst(c) = x := exists b. pair(x, b) = c

I saw this in a book, that I attach the screenshot to:

So my main question is if the predicate can become a function?

And yes, can you show "the function fst from ℕ to ℕ is definable in the language of PA" this?

Answer 1

Imagine you were tasked with recapitulating something close to the relatively simple proof of the halting problem inside Peano arithmetic. In the case of the halting problem, the proof is pretty simple because it's based on a relatively powerful architecture called a Turing machine. You are now tasked with recapitulating that proof inside Peano arithmetic using only addition and multiplication, a very weak architecture indeed.

You are now stuck with having to implement most of a programming language based only on the operations addition and multiplication. This includes substantial data structures as well as a parser at least. Where to begin? One idea would be to copy an existing programming language. Fortunately, several such languages exist, notably Lisp. In Lisp, all the data structures are built on one fundamental data structure: a pair. In Lisp, such a pair is called a cons cell; in Scheme, this thing is called a pair. To use such a pair, we need to define accessors to get to the first element of the pair as well as the second element of the pair.

So here we find ourselves on your question. We have to define a pair based on addition and multiplication. And so we can see in your page from your attached textbook that the authors are doing just that. But they're doing it in a somewhat dodgy way. They're creating a quadratic function based on addition and multiplication. This is fine until one wants to extract $x$ and $y$ back from $c$. At this point this requires square roots, but these are not closed over the natural numbers. So they define the function implicitly using logic. Luckily this works fine for a mathematical proof, even though this can't work in any efficient way if at all in creating an actual programming language.

So to get to your questions: first, the $\text{fst}(c)$ function is defined implicitly on the page you enclosed from the textbook as I described in the previous paragraph. Second, the definition is based only on the standard logical operators as well as addition and multiplication so the function is indeed defined in terms of Peano arithmetic.

Answer 2

To your first question, yes, there is no problem transforming a predicate into a function using the "if and only if" operator.

In the other hand, first of all fst is not a function from $\mathbb N$ to $\mathbb N$. This is to de fact that are natural numbers that cannot be form with the operator pair, for example 3. A side from this, the construction of it shows that it is definable in the language of PA, due to the fact that we have only used definitions that at their base come from first-order logic and the functions S,+,* that come from the PA itself.