Nxx писал(а):
в формальном языке примитивно-рикурсивных функций невозможно.
Нет такого формального языка.
Вы пытаетесь забить гол в ворота противника, но все время выбиваете мяч в аут. Правила, между прочим, издаются с тридцатых годов.
Например, реально вы могли дать такое возражение: по определению выразимого отношения все еще нельзя доказать, что в принятой аксиоматике формальной арифметики есть формула, с помощью которой выражалось бы отношение
![$\Gamma$ $\Gamma$](https://dxdy-04.korotkov.co.uk/f/b/2/a/b2af456716f3117a91da7afe7075804182.png)
. Тут мне нечем было бы крыть, а пришлось бы наложить заплатку, мол, для доказательства я использовал такое расширение формальной арифметики, в которой формула, выражающая
![$\Gamma$ $\Gamma$](https://dxdy-04.korotkov.co.uk/f/b/2/a/b2af456716f3117a91da7afe7075804182.png)
, разрешима. Вообще, утверждая, что формула
![$P$ $P$](https://dxdy-02.korotkov.co.uk/f/d/f/5/df5a289587a2f0247a5b97c1e8ac58ca82.png)
некоторой формальной теории
![$K$ $K$](https://dxdy-02.korotkov.co.uk/f/d/6/3/d6328eaebbcd5c358f426dbea4bdbf7082.png)
выражает отношение
![$R$ $R$](https://dxdy-02.korotkov.co.uk/f/1/e/4/1e438235ef9ec72fc51ac5025516017c82.png)
, мы тем самым предполагаем ее разрешимость в
![$K$ $K$](https://dxdy-02.korotkov.co.uk/f/d/6/3/d6328eaebbcd5c358f426dbea4bdbf7082.png)
. А что если она неразрешима в
![$K$ $K$](https://dxdy-02.korotkov.co.uk/f/d/6/3/d6328eaebbcd5c358f426dbea4bdbf7082.png)
? Нет проблем - добавим к аксиомам теории
![$K$ $K$](https://dxdy-02.korotkov.co.uk/f/d/6/3/d6328eaebbcd5c358f426dbea4bdbf7082.png)
новую аксиому
![$P$ $P$](https://dxdy-02.korotkov.co.uk/f/d/f/5/df5a289587a2f0247a5b97c1e8ac58ca82.png)
или
![$\neg P$ $\neg P$](https://dxdy-04.korotkov.co.uk/f/3/d/7/3d7f0dfe7ce626d36dcd9f3682e3649882.png)
и все станет на свои места в новой теории
![$K'$ $K'$](https://dxdy-02.korotkov.co.uk/f/1/1/a/11ad6c363764241ae47a3bfe1660862382.png)
.