Уважаемый коллега!

Вы слишком строги по отношению к использованному мною обороту:
"существуют истинные, но недоказуемые формулы языка".

Гёдель (как известно) доказал так называемую синтаксическую
версию теоремы : существует такая формула, которую нельзя ни
доказать, ни опровергнуть. Понятие истинной формулы в этой
системе отсутствует (в связи с неопределенностью, что такое
"истина") и заменено образом доказуемости.

Семантический подход (я им и спекулировал) допускает, что
бывает такая истинная формула, которую нельзя доказать.
Это (как я могу предположить) нисколько не противоречит
1-му (верхнему) варианту. В принципе, речь идет о некоем
свойстве (качестве) формулы языка, "реальность" которого
объявляется ЗА возможностями системы различать его тем
набором формальных средств, которым она располагает.

Жаль, что тема данной ветки не позволяет злоупотреблять
вниманием тех, кому извращения Гёделя не так "важны", как
мне и Вам.