Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 116
Текст из файла (страница 116)
Эти формулы при помощи схемы (5,) дают формулу )(6йй)» а из нее по схеме (5,) мы получим формулу $-» )Я. Из формулы 6-» )(Яйе) при помощи обращения схемы (5!) получается формула ~(Ей(Лй6)); с другой стороны, из выводимой формулы (!р' й Я) й 6-» 14! й (Я й 6) прн помощи производной схемы контрапозиции получается формула .)(6й(ййе)) -)(()))йй)йе).
Из этих двух полученных нами формул при помощи схемы заключения (В,) получается формула 1((6 йй) йе), а из нее при помощи схем (5,) и (8,) мы получаем формулу $- (я-» )6). ПРИЛОЖЕНИЕ Заметим, что в только что приведенных выводах схема формул (3,) не используется. Отсюда следует, что теорема о посылках применима как к формализму схем (3,) — (3,), так и к формализму схем (31) — (31) Итак, доказательство выводимости всех тождественно истинных 1-К-Н-формул при помощи схем (3,) — (3,) закончено. Что же касается вопроса о независимости схем (3,) — (31), то легче всего можно убедиться в независимости схемы заключения (3,): она вытекает из того, что с помощью остальных схем не может быть выведена никакая формула вида 6616.
Независимость схем (3,), (3,), (3,), (3,) и (31) получается с помощью тех оценок, посредством которых мы в гл. Ш т. 1 установили независимость формул П 1), 2), 1 3) и Ч 1), 3) в системе, состоящей из формул 1 — Ч (с использованием подстановок и схемы заключения)1). При этом из упомянутых оценок здесь нужно взять только определения значений для импликации, конъюнкции и отрицания.
Доказательство независимости с помощью такого рода оценки для любой данной схемы (31) проводится следующим образом. Сначала для каждой отличной от (31) схемы из списка (3,) — (3,), являющейся схемой формул, мы показываем> что каждая построенная по этой схеме 1-К-Н-формула на осно. ванин рассматриваемой оценки при произвольных значениях переменных принимает только вполне определенные, выделенные значения; затем для каждой нз остальных, отличных от(31) схем мы показываем, что от формул, принимающих только выделенные значения, эта схема снова ведет к формуле, также обладающей этим свойством. Тогда отсюда получается, что каждая 1-К-(Ч-формула, выводимая по отличным от (3;) схемам, при любых значениях формульных переменных принимает выделенное значение.
С другой стороны, указывается тождественно истинная 1-К-М-формула, которая при некоторых значениях формульных переменных на основании рассматриваемой оценки принимает невыделенное значение. Эта формула, как было показано, выводима с помощью схем (3,) — (3,), но она не может быть выведена без использования схемы (3;).
В этих доказательствах, проводимых с помощью упомянутых пяти оценок, в качестве выделенного значения используется значение а. Независимость схемы (3,) мы получаем с помощью оценки с четырьмя значениями а, 3, у и 6, определяемой следующим .образом: А-РА=и, й-РА=а при любом значении А; 11 Си. 1, 1, с. 107 н 110 — 111, тождественные 1-к-н-Формулы если А М В и А чь 11, то А — В = В; Аи А=А, А61а=А, А81(1=й при любом значении А; А й В = В й А при любых значениях А и В; уйб=й; ~а=Р, ~Р=а, ~у=б, ~б=у. При этой оценке 1-К-М-ф рмулы, выводимые при помощи схем (31), (31) (31) — (31) всегда принимают значение и; в то же самое время тождественно истинная формула А — Р (В -+ А 61 В) при А =у и В=6 принимает знзчение р.
Независимость схемы (3,) удается доказать при помощи оценки, отличающейся от только что указанной лишь равенствами у616=6, 1т=й, 16=а. При этом наряду с а в качестве выделенного значения рассматривается еще и у. В самом деле, оказывается, что при помощи схем (3,) — (3,) и (3,) выводятся только такие 1-К-Х-формулы, которые при укаэанной оценке всегда принимают одно из значений а или у; с другой стороны, тождественно истинная формула, (А — В) -1.
( 1В -Р ) А) при А =у и В=6 принимает значение (). Замечание. Примененный для установления независимости схем (3,) — (3,) метод перехода от исходных схем формул к соответствующим им конкретным формулам с добавлением правила подстановки и сохранением в качестве схемы вывода одной только схемы заключения в случае схем (3,) — (3,) не всегда ведет к цели, так как в этом случае формула 1(А 61 В) -~-(А-» 1В), соответствую1цая схеме (3„), не независима от формул, ствующих схемам (3,) — (3,), (3,), (3,) и (3,) В"речем, обсуждение схем в терминах оценок всегда проще„ "ем обсуждение соответствующих формул.
В за включение кратко упомянем некоторые другие факты имеюп ие 1 е отношение к рассмотренным здесь вопросам. Что касается выводов 1-К-Х-формул при помощи схем (3 ) — (3 ), то имеет место У щ е утверждение. Произвольная формула тогда и только 1 7 то~да выводима с помощью схем (3,) — (3 ), примененных 1 7 венной м -формулам, когда она либо является позитивно тождестформулой„либо когда она содержит отрицание и переходит в позитивно тождественную формулу, если мы, выбрав некоторую ПРИЛОЖЕНИЕ !!и тождсстнснные ! к н ФОРмулы 4 3! ие входящую в нее формульную переменную З, заменим каждое входящее в нее выражение )Я импликацией Я-«3!). Эта теорема получается из некоторых результатов Иоганссона, относящихся к минимальному исчислению ').
Алгоритм, позволяющий по любой 1-К-формуле распознавать, является ли она позитивно тождественной, получен Генценом') на основе его «теоремы о подформулах». Еще один алгоритм для решения этой задачи построен М. В а й с бе р г о м '). Упомянутые исследования Генцена и Вайсберга дают также алгоритм для распознавания выводимости формул в гейтинговском исчислении высказываний ').
Исчисление Гейтинга с дедуктивной точки зрения равносильно формализму, который получится, если к совокупности формул, образованных с помощью импликации, конъюнкции, отрицания и дизъюнкции, применить схемы (Бх) — (Вт) и, кроме того, схему вывода ~Я Я-«6 .для отрицания, а также следующие схемы для дизъюнкции: Если здесь опустить схему вывода 1Я то получится формализм так называемого м и н и м а л ь н О г о исчисления. Из результатов Генцена и Вайсберга следует, что всякая 1-К-формула, выводимая в гейтннговском исчислении высказываний, является позитивно тождественной н что выводимые в гей- г) Эта формулировка примыкает к формулировке несколько более слабой теоремы, докааанной Вайсбергом в его работе; % а ! з Ь е г й М.
1!п!егзосьппйеп йЬег беп Аоззайеп!га!Ьй!. — %!аботовс! Ма1егп., 1938, 46. ° ) з оь апззоп 1, !уег М!п!гпа!Ьа!Ьй!, е!п гебпг!ег1ег !п1ои!оп!з!!зсьег Роппапапнз.— Согпроыпо. Ма1Ь., !936, 4, № !. — Некоторое уточнение интуиционистской логики высказываний в духе минимального исчисления было полу. чено А. Колмогоровым в его (написанной на русском языке) работе: Колыот орр ов А. Н. О принципе 1егнюп поп да!от.— Метем. сб., !925, 32. ') В его работе: Оеп1хеп О. !!п1егзнсйнпйеп йЬег баз!ой!асье Бсш!ейеп. — Ма1Ь, 2., 1934, 39.
См. сноску 1 на с. 520. Я См. только что цитированную работу еНп1егзосьопйеп йЬег реп Апззайепйв1йй!». з) См. Неу! ! пй А. О!е !оппа!еп цейс!п бег !п1п!1!Оп!з!!зспеп 1ойж. — ' 3!1вппйзьег. Ргеой, Айаб. %!зз., рйуз.чпа1Ь. К1., 1930, Н. тингонском исчислении формулы, не содержащие отрицания, выводимы без использования отрицания при помощи схем ($х) — (3з) и трех указанных выше схем для дизыонкции.
Если рассматривать выводы с помощью подстановок и схемы заключения, то формулы 1 1) — 3), П 1) — 3), 1П 1) — 3), Ч 1) — 2) нз приведенной в гл. П1 т. 1 системы формул 1 — У!) образуют систему аксиом для минимального исчисления, При этом формулы 1 1) — 3) могут быть заменены формулами 1", а формула 11 3) более простой формулой (А — В) -«(А-ь. А йг В); кроме того, шесть формул 1 1) — 3), П 1) — 3) могут быть заменены приведенными в 9 2 равнозначными им двумя системами, состоящими из четырех и соответственно из пяти формул ').
Кроме того, вместо двух формул Ч 1) — 2) (А-ь.В) — «ПВ-«) А) и А-«"! 1А можно взять одну формулу (А-«В) — «((А-ь ~В)-«1А) или одну формулу (А-ь ! В) «(В-«) А). Если формулы Ч !) — 2) заменить двумя формулами (А-«1А) — ) А ! А-«(А — В), то получится система аксиом для гейтинговского исчисления высказываний. В каждой из перечисленных систем аксиом любая из формул независима от всех остальных.
') См. т. 1, с. 96 — 97. з) См. с. 529, 53!. 18 д. Гельверт, П. Бернаае ПРИЛОЖЕНИЕ 1Ч ФОРМАЛИЗМЫ ДЛЯ ДЕДУКТИВНОГО. ПОСТРОЕНИЯ АНАЛИЗА й 1. Описание одного формализма Мы изложим здесь один формализм, пригодный для дедуктивного построения анализа. Этот формализм будет приведен нами — ' с точностью до несущественных деталей — в том виде, как он излагался в лекциях Гильберта по теории доказательств. Сходный формализм описан в диссертации Аккермана').
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
