Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 58

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 58)

В первом иэ этих случаев мы поместим формулу Я, иа которой 6 получается в результате подстановки, над формулой 6, изобразив это следующим образом: Во втором случае посылки (е и ш-»- 6 рассматриваемой схемы эаключения с реаультирующей формулой 6 мы поместим слева и справа над формулой 6, иэобраэив это в виде Теперь мы рассмотрим формулу Я (соответственно каждую иэ Формул 5 и Я-». 6) с точки зрения упомянутой выше альтернативы. Если эта формула является тождественной формулой или »г» 1гл.

ч2 НАЧАЛА АРИФМКТИКИ ОВЩВЛОГИЧЕСКАЯ ЧАСТЬ ДОКАЗАТНЛЬСТВА $21 276 аксиомой, то мы на ней и остановимся; если же эта формула получается подстановкой иа формулы, полученной ранее, или если она является результирующей формулой какой-нибудь схемы заключения, то мы поступим с ней так в'е, как с заключительной формулой 6. Случай совпадения с одной из предыдущих формул мы рассматриваем совершенно так же, как случай подстановки. С добавившимися на данном шаге формулами мы поступаем тем же самым способом. Этот обратный просмотр мы будем продолжать до тех пор, пока он по всем ветвям не дойдет до исходных формул, т. е.

до тождественных формул или до аксиом. Эта ситуация рано пли поздно будет достигнута, так как при каждом шаге просмотра мы переходим от данной формулы доказательства к какой- либо предшествующей (соответственно к двум предшествующим формулам), и потому количество таких в|агав ограничено рааиерами самого доказательства. Коли при выполнении этой операции некоторые формулы доказательства останутся яеиспольаованными, то мы исключим их из дальнейшего рассмотрения.

Чтобы пояснить описанный метод на примере, мы должны будем рассмотреть вывод какой-нибудь действительно доказуемой в нашей системе аксиом формулы. Мы возьмем вывод формулы 1(0" <О'). Прежде чем приводить этот вывод, заметим, что здесь, равно как и в других случаях, мы будем допускать произвольный порядок посылок при применении схемы заключения, т.

е. будем допускать оба возможных случая чередования ы,,с~ Я-«~б Я Благодаря этому мы сэкономим ненужные повторения, а при разложении докааательства на нити это различие все равно не будет играть никакой роли, так как мы условились всегда писать формулу Я слева, а формулу Я-«Й справа перед результирующей формулой ааключения. Применение схемы заключения мы всякий раз будем отмечать горизонтальной чертой между посылками и результирующей формулой, а получение формулы ив предыдущей в результате подстановки или повторения мы будем указывать соединительной стрелкой, ведущей от предыдущей формулы к последующей. Мы устроим сквозную нумерацию формул следующего ниже докааательства, чтобы в дальнейшем при разложении доказательства на нити каждую его формулу можно было упоминать при помощи ее номера 1) а < Ь & Ь < с -«а < с 2) (А & В -+.

С) — «(А -«(-1 С -«1 В)) ~~3) (а<а'& а'<а-«а<а)-«(а<а'-«( 1(а<а)-«~ (а <а))) ,4) а < а' & а' < а — «а < а 5) а<а' — «(1(ас а)-«~(а'<а)) 6) а<а' 7) 1 (а < а) — « -1 (а' < а) 8) 1(а < а) ~ — 9) -1 (а' а) . 10) -1 (О" < 0') Разложение этого доказательства на нити изображается следующей фкгурои: 1) 2) 1 4) 3) 10) С помощью атой фигуры мы проиллюстрируем смысл выражения разложение доказательства на нити.

Под нитью докааательства мы будем понимать последовательность формул, идущих в фигуре разложения друг за другом в обратном направлении, причем эта последовательность начинается заключительной формулой доказательства, а оканчивается исходной формулой, на которой эта нить и обрывается. При каждом применении схемы заключения две нити доказательства расходятся и две такие пити, однажды отделившись друг от друга, в дальнейшем никогда не сольются.

Поэтому в данном доказательстве имеется в точности столько нитей, сколько в фигуре разложения имеется различных концевых вершин. В концевых вершинах находятся исходные формулы доказательства. В приведенной фигуре таких вершин четыре. В них 279 НАЧАЛА АРИФМЕТИКИ [ггг, чг ОЭЩЬЛОГИЧЕСКАЯ ЧАСТЬ ДОКАЗАТЕЛЬСТВА [ гп находятся формулы 1), 2), 6) и 8). Формула 2) — тождественная формула исчисления высказываний, а 8), 1) и 6) — это наши аксиомы ((г), (~з) и ((а). Укааанным четырем концевым вершинам соответствуют следующие четыре нити доказательства: 10), 9), 7), 5), 4), 1); 10), 9), 7), 5), 3), 2); 10), 9), 7), 6); 10), 9), 8), В то время как разложение заданного докааательства на нити ведет к однозначно определяемой фигуре рааложения, одной и той же фигуре разложения отвечает, вообще говоря, несколько различных доказательств, которые, правда, отличаются друг от друга лишь несущественными деталями, а именно таким образом, что одно из них всегда может быть получено нз другого в результате перестановок и повторения (соответственно опускания повторно встречающихся) формул.

Так, например, доказательство, состоящее иэ последовательности формул 2), 3), 1), 4), 3), 4), 5), 6), 5), 7), 8), 7), 9), 10), дает то же самое разложение па нити, что и заданное нам дока- зательство, состоящее иэ последовательности 1), 2), 3), 4), 5), 6), 7), 8), 9), 10) Фигуру разложения какого-либо доказательства мы для краткости будем называть р а а л о ж е н н ы м д о к а з а т е л ьс т в о и. Такая фигура характеризуется следующими свойствами.

Она состоит из нитей доказательства, т.е. иэ последовательностей формул, начинающихся (мы ведем счет снизу вверх) одной и той же формулой. Каждые две несовпадающие нити доказательства расщепляются у формулы, которая является результирующей формулой некоторого заключения, посылками которого являются следующие по порядку формулы обеих нитей, и у всех нитей, которые проходят через такое место фигуры, где стоит результирующая формула некоторого заключения, за этой формулой следует одна из двух посылок заключения. Формула, в которой никакие две нити доказательства не расщепляются, находится со следующей за ней формулой (в любой нити, которая их содержит) в таком отношении, что либо она совпадает с этой формулой, либо получается из нее в результате подстановки.

Всякая нить оканчивается формулой, которая является либо тождественной формулой, либо аксиомой. 2. Возвратный перенос подстановок; исключение свободных переменных; нумер н е ические формулы; определение истинности и ложности' истинность всякой формулы, выводимой без использомы помяк 'ли вания связанных анных переменных. Разложение на нити мы у у бып о- в качестве первои иа т .

" иа тех двух операций, которые мы смогли ы про- извести над выводом формулы ОФО, если бы он оказался в нашем распоряжении. Вторая операция, примыкающая к а к данной представляет собой исключение свободных сем все леременнмх. то . Ч бы подготовить эту операцию, мы перенесем вс ельстве ггодстановки, ко д которые проиаводятся в данном доказат ь моб а- е исходные формулы.

Это может быть проделано следующим о ра- зом. 51ы идем по . 51 каягдой нити, начиная с ааключптельной фор- мулы, до тех пор, пока не дойдем до двух рядом стоящих в атой ф и л Я и З, первая из которых получается из второй эт по становку в реаульт т льтате подстановки. Тогда мы производим ту д т и в самон Чгормуле, та ф е З так что вместо З у нас получится пов оре- ние формулы Я.

Если З представляет собой исходную формулу, то в резуль- тате этои процедуры р ы рассматриваемая подстановка оказывается н й в исходную формулу. В противном случае З ли о ы ей о мулыб, получается подстановкой из некоторой предыдущей формулы либо является повторением предыдущей формулы, либо является результирующей формулой некоторого заключения В первом случае на место гь мы снова помещаем формулу Я, так что в гз должны быть проиаведены сразу обе подстановки, ведуШиеот[г, к пот х З З к 98 В случае повторения выполняется только одна подстановка.

ся в результате применения схемы ааключеЕсли ю получает ния, то мы про ы и оизводим подстановку, ведущую от 3 к Я, в формулах Ж и 6-~ З; при этом формула гб претерпевает иаме иаменения в том и только в том случае, когда ока содержит ту переменную, вместо которой производится подстановка при переходе от З к Я. В любом случае на и есте первоначальной схемы заключения с результирующеи фо ф рмулой З будет стоять схема заключения г] нАчАлА АРКФметики !ГЛ, Ч! ОБЩЕЛОГИЧЕСКАЯ ЧАСТЬ ДОКАЗАТЕЛЬСТВА Указанный процесс мы будем продолжать до тех пор, пока по каждой нити не дойдем до исходной формулы. Когда этот процесс аакончится, на месте каждой подстановки будет стоять повторение, на месте каждой схемы заключения снова будет стоять некоторая схема заключения, а в исходных формулах будут произведены те или иные подстановки.

Если мы применим эту процедуру к нашему предыдущему примеру, то вместо формулы 9) мы должны будем написать повторение формулы 10): ] (О" < 0'). Эта формула получается из 9) в результате подстановки 0' вместо а. Теперь мы должны произвести ту же самую подстановку и в трех идущих в обратном направлении схемах заключения; иными словами, мы должны будем в формулах 8), 7), 6), 5), 4), 3) всюду вместо а подставить 0'. Наконец, мы должны будем вместо формулы 2) написать формулу, получающуюся в результате этой подстановки из формулы 3), а вместо формулы 1) — формулу, получающуюся в результате этой подстановки из формулы 4). В результате всех этих подстановок вместо первоначального доказательства мы получим следующий ряд формул: 0' с 0" 8с 0" < 0' -+ 0' < 0', (о'<О" Ао" <о' — )-о'со')-~-(о'с о" (-](о'со')-+.-] (О"с О'))), (О' < 0' д 0" < О' -э- 0' < 0 ) — э- (О' < 0' -«-(~ (О' < 0 ) -+.

-] (О" < 0'))), 0' < 0" % 0" < 0' -!- 0' < 0' о'со" .(-,(о <о) -](о" <о)) 0' <О" Ф -](О <О) -,(О-<О) -1(О СО) -] (О".< О ) ~(О'<О) Этот пример носит несколько специальный характер, так как в рассматриваемом случае процедура возвратного переноса подстановок соотносит каждой формуле нашего первоначального докааательства соответствующую ей модифицированную формулу совершенно одкоаначным образом. В общем случае этого достичь не удается, потому что при разложении доказательства на нити одна и та же формула доказательства может встречаться в фигуре разложения в нескольких местах.

Характеристики

Список файлов книги