Terminology: arithmetic vs. expressible vs. represented

A function $$f:\mathbb{N}^k\rightarrow\mathbb{N}$$ is arithmetic iff its graph is arithmetic, i.e., there is a formula $$\psi(\vec{x},y)$$ in the language of Peano arithmetic such that for all $$\vec{a}$$ in $$\mathbb{N}^k$$, $$f(\vec{a})=b$$ iff $$\mathbb{N}\models\psi(\vec{a},b)$$.

For $$f$$ to be represented in PA, we have the (much) stronger condition that for all $$\vec{a}$$ in $$\mathbb{N}^k$$, $$f(\vec{a})=b$$ iff $$\text{PA}\vdash\psi(\vec{a},b)$$.

I'm wondering about an intermediate condition: $$f$$ is arithmetic, and in addition, PA proves that the associated formula defines a function. That is, $$\text{PA}\vdash\forall\vec{x}\,\exists!y\,\psi(\vec{x},y)$$.

Would it be reasonable to call this condition expressible in PA? Or would that conflict with generally accepted terminology?

I'm also assuming that definable in PA is a synonym for arithmetic. But I'm interested in hearing from anyone who doesn't agree with this.

• IMO, the terminology is not very "stable". R.Smullyan (into his G's Incompl Th) uses expressible for the first one (true in...) and representable for the second one (provable in...). – Mauro ALLEGRANZA May 10 at 14:59
• Your condition for "represented" doesn't make sense : what's the connection between $a$ and $x$, $b$ and $y$ ? – Max May 10 at 15:39
• @Max I assume what was meant was $\text{PA}\vdash \psi(\overline{a},b)$. – Alex Kruckman May 10 at 15:52
• @AlexKruckman yes I thought so but at first I had a misconception in my head about what $\mathbb{N}\models \psi(a,b)$ implied about provability in PA, I was thinking in too low complexity of formulas – Max May 10 at 16:00

Your condition is called definable. This is standard usage in model theory: Given a theory $$T$$, a definable function is a formula $$\varphi(\overline{x},y)$$ such that $$T\vdash \forall \overline{x}\, \exists^! y\, \varphi(\overline{x},y)$$, up to provable equivalence in $$T$$. Then for any model $$M\models T$$, $$\{(\overline{a},b)\in M^{n+1}\mid M\models \varphi(\overline{a},b)\}$$ is the graph of a function $$M^n\to M$$ (which we abuse terminology by also calling a definable function).
It would be a big mistake to make "definable in PA" a synonym for "arithmetic". The point is that the definition of arithmetic has nothing to do with the theory PA, it's just about the standard model $$\mathbb{N}$$. On the other hand, the definition of definable has nothing to do with the standard model $$\mathbb{N}$$, it's just about the theory PA. These are totally different concepts.
• OK, thanks. And I guess we would use "definably represented" for the conjunction of those two conditions. (A priori, I can't see why one would imply the other, in general (i.e., for $\psi$ high enough in the hierarchy). – Michael Weiss May 10 at 18:39
{"ft_lang_label":"__label__en","ft_lang_prob":0.87683815,"math_prob":0.99913687,"size":913,"snap":"2019-26-2019-30","text_gpt3_token_len":271,"char_repetition_ratio":0.13971397,"word_repetition_ratio":0.06837607,"special_character_ratio":0.28039432,"punctuation_ratio":0.13989638,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9999379,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-06-21T00:03:30Z\",\"WARC-Record-ID\":\"<urn:uuid:922f2fd5-a8b5-4eae-a84b-c7aba06df680>\",\"Content-Length\":\"146521\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:cd4d7826-157a-4919-a427-53084fe52384>\",\"WARC-Concurrent-To\":\"<urn:uuid:b4203a5d-07b1-417e-8011-3c7875d0376a>\",\"WARC-IP-Address\":\"151.101.129.69\",\"WARC-Target-URI\":\"https://math.stackexchange.com/questions/3221021/terminology-arithmetic-vs-expressible-vs-represented\",\"WARC-Payload-Digest\":\"sha1:7SJ7KUKICXYVCPGN52PFU55YGIT6J5CH\",\"WARC-Block-Digest\":\"sha1:X7IKK4EAJMJJBJQ7KJJM7OAELSUVJVWJ\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-26/CC-MAIN-2019-26_segments_1560627999291.1_warc_CC-MAIN-20190620230326-20190621012326-00512.warc.gz\"}"}