в "естественной" модели соответствуют истинные высказывания
Интересно, как это определяется? Если я правильно понимаю Гёделя, модель, в которой истинны те и только те высказывания, которые выводимы, тоже достаточно "естественна". Хотя при этом окажется истинным высказывание, утверждающее противоречивость арифметики, ну да и пусть...
Суть создания ИИ я вижу в том, чтобы машина могла доказывать или опровергать утверждения из самых разных областей математики. Современные компьютеры на базе машины Тьюринга это не умеют.
Машина-то Тьюринга Вам чем не угодила? Она, в общем-то как раз и определяет то, что в принципе "доказуемо или опровержимо". Так что если Вы хотите чего-то такого, что в принципе недостижимо для машины Тьюринга, то значит собираетесь залезть в область принципиально недоказуемого и неопровержимого.