# How to write a first order formula with unspecific parameter

Excuse me for the awkward wording. I'm new to logic. What I really mean is this:

Consider the number theory that spawns from the structure $N=\{\mathbb{N},+,\cdot\}$ (equipped with the usual interpretation) using first order logic. I understand that the formal sentences generated this way are capable of expressing all elementary number theory statements in the sense that the statement "$x$ divides $y$" can be expressed as $\exists z(x\cdot z=y)$, so that $N\models \exists z(x\cdot z=y)$ iff $x$ divides $y$.

But there's a kind of statement that I don't know how to express in the system, like "$x$ can be written as the sum of cubes". It is easy to write "$x$ can be written as the sum of $n$ cubes" given specific $n$ into something like $\exists z_1z_2...z_n(x=z_1\cdot z_1\cdot z_1+z_2\cdot z_2\cdot z_2+...+z_n\cdot z_n\cdot z_n=x)$. But in the first statement it seems one can't follow suit because the "$n$" there is not specific. How can we quantify the unspecific parameter? What are tricks for expressing it?

Edit: By the way, "...that the formal sentences generated this way are capable of expressing all elementary number theory statements..." Is this true?

-

yes you are right. thank you for pointing that out – Eric Mar 21 '12 at 3:15

## 1 Answer

The trick is to encode the sequences of natural numbers by a natural number. For example the sequence $x_1, ..., x_n$ can be encoded by the number $p_1^{x_1 + 1} \cdot ... \cdot p_n^{x_n + 1}$, where $p_i$ is the $i$-th prime number. Then you express properties of such an encoding. That is you construct formulas to express some of the following relations and functions

• $seq(x)$ - $x$ encodes a sequence
• $lh(x)$ - the length of the sequence encoded by $x$
• $(x)_i$ - $i$-th element of the sequence encoded by $x$.

Then the statement ''$x$ can be written as the sum of cubes'' can be expressed by something like this $$\exists y (seq(y) \land x = sum(y) \land \forall (i < lh(y)) cube((y)_i))$$ where x = sum(y) is the following formula $$\exists z (seq(z) \land lh(z) = lh(y) \land (z)_0 = (y)_0 \land x = (z)_{lh(z) -1} \land \forall (0 < i < lh(z)) (z)_i = (z)_{i-1} + (y)_i)$$ which expresses the relation $x$ is the sum of elements of the sequence encoded by $y$.

-

But what is $x=sum(y)$? – Eric Mar 20 '12 at 1:17
Edited the answer to explain that. – Levon Haykazyan Mar 20 '12 at 20:54
$cube((x)_i)$ should be $cube((y)_i)$, right? – Eric Mar 21 '12 at 1:25
yes, that's right, thanks. Edited to fix that. – Levon Haykazyan Mar 21 '12 at 14:23
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 30, "mathjax_display_tex": 2, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9388197660446167, "perplexity_flag": "head"}