Teopeма Гёделя | страница 44
Перейдем теперь к более подробному изложению доказательства теоремы Гёделя.
1. Мы уже определили выше формулу «~ Dem(x, z)», представляющую в формальном арифметическом исчислении метаматематическое высказывание: «последовательность формул, имеющая гёделевский номер x, не является доказательством формулы, имеющей гёделевский номер z». Теперь мы доставив перед формулой приставку «∀x», являющуюся формальным аналогом языкового оборота «для всех x» (или «для любого x»), и получим в результате новую формулу «∀ x ~ Dem (x, z)», представляющую в формальной арифметике метаматематическое высказывание: «для любого x последовательность формул, имеющая гёделевский номер x, не является доказательством формулы, имеющей гёделевский номер z». Таким образом, эта новая формула является как раз той формулой формального арифметического исчисления, которая представляет в нем метаматематическое высказывание «формула, имеющая гёделевский номер z, недоказуема», или, что то же: «для формулы с гёделевским номером z нельзя построить доказательство».
Гёдель далее показал, что некоторый частный случай этой формулы является формально недоказуемым. Чтобы получить формулу, мы будем исходить из следующей формулы:
∀ x ~ Dem(x, sub(y, 13, y)) (1)
Эта формула, принадлежащая формальному арифметическому исчислению, представляет некоторое метаматематическое высказывание. Какое же именно? Читатель должен помнить, что выражение «sub(y, 13, y)» обозначает некоторое число, которое есть гёделевский номер формулы, получаемой из формулы, имеющей гёделевский номер у, подстановкой вместо переменной, имеющей гёделевский номер 13, (т. е. переменной y) цифры, обозначающей число у. Отсюда видно, что формула (1) представляет метаматематическое высказывание: «формула, имеющая в качестве гёделевского номера число sub(y, 13, y), недоказуема».
Но так как формула (1) принадлежит арифметическому исчислению, она имеет некоторый гёделевский номер, который можно фактически вычислить. Пусть этим номером является число
 
                        
                     
                        
                     
                        
                    