Может быть, проблема в том, что теоремой Гёделя можно называть как "настоящую" теорему арифметики
![$\exists \varphi: \varphi \leftrightarrow \neg \Box_{PA} \varphi$ $\exists \varphi: \varphi \leftrightarrow \neg \Box_{PA} \varphi$](https://dxdy-02.korotkov.co.uk/f/9/a/5/9a5883df6d98797b5137ef56182a9c8182.png)
(а 2й
![$Cons_{PA} \rightarrow \neg \Box_{PA} \ulcorner Cons_{PA}\urcorner$ $Cons_{PA} \rightarrow \neg \Box_{PA} \ulcorner Cons_{PA}\urcorner$](https://dxdy-02.korotkov.co.uk/f/5/8/f/58f060b176a49ec472ab273fae6b669782.png)
), так и неформальную "если арифметика непротиворечива, то она неполна"?
Формально у нас есть три варианта:
1)
![$PA$ $PA$](https://dxdy-02.korotkov.co.uk/f/d/d/2/dd29b5d12dbf57473c73ccd13f55799582.png)
непротиворечива, и у нее есть модель, соответствующая нашей "интуиции" про стандартную модель: оговорка не нужна
2)
![$PA$ $PA$](https://dxdy-02.korotkov.co.uk/f/d/d/2/dd29b5d12dbf57473c73ccd13f55799582.png)
противоречива: оговорка нужна
3)
![$PA$ $PA$](https://dxdy-02.korotkov.co.uk/f/d/d/2/dd29b5d12dbf57473c73ccd13f55799582.png)
непротиворечива, но у нее есть только "нестандартные" модели: всё очень плохо (непонятно, что вообще "значат" все наши формальные результаты про выводимость)
Тот, кто говорит "арифметика неполна" "прав" (на неформальном уровне) в 1м случае, тот, кто говорит "если непротиворечива, то неполна" - в 1 и 2.
Интересный вопрос, что мы будем делать, если окажется, что
![$PA \vdash \neg Cons_{PA}$ $PA \vdash \neg Cons_{PA}$](https://dxdy-03.korotkov.co.uk/f/6/e/1/6e1491294f2f4bdd179e2ed4d755c64282.png)
...