Вывод формул из гипотез

Обобщим понятие выводимости ф-л из аксиом.Опр. Гипотезами назовем произвольное мн-тво ф-ул (ИВ).Обозн. Г.

Опр. Выводом ф-лы А из мн-ва гипотез Г наз-ся конечная послед-ть ф-ул F₁, F₂, …,F_k, заканчивающаяся ф-лой А (F_k=A) и каждая ф-ла в этой послед-ти явл-тся или аксиомой, или гипотезой, или получена из двух предыдущих по правилу (MP).Обозн. Г А (из Г выводима А) или F₁, F₂, …,F_k А (ф-ла выводима из гипотез F₁,F₂, …,F_k.)

П-р: построить вывод ф-лы С из гипотез: А, А®В, В®С.

1) А гип.1;

2) А®В гип.2;

3) В®С гип.3;

4) В (МР) к 1), 2)

5) С (МР) к 3), 4).

Выводимость из аксиом м. рассматривать как частный случай выводимости из гипотез, где множество гипотез пусто.

Св-ва вывода ф-л из гипотез.

1°. Г, А А (св-во самовыводимости).

Док-во: Вывод состоит из единственной формулы А.

2°. Если Г А, то Г, В А, где В – люб.ф-ла (расширение списка гипотез).Док-во: Мн-во гипотез м.расширять, при этом выводимость ф-лы не нарушается. Данный вывод яв-ся в то же время и искомым. Новое док-во ф-лы А совпадает со старым, на ф-лу В не ссылаются.3°. Г, В А и Г В, то Г А (выводимые гипотезы м. исключать из списка гипотез, при этом выводимость дан.ф-лы не нарушается).Док-во: Нужно в дан.вывод ф-лы А подставлять вместо В ее вывод из Г, получим тем самым вывод ф-лы А из Г.4°. Если из Г А и А В, то Г В (св-во транзитивности вывода).Док-во: В выводе А В каждое вхождение ф-лы А след-т заменить ее выводом из Г ( ГА), в рез-те получится искомый вывод.5°. Если из Г, А, А В, то Г, А В (св-во сокращения).До-во: Повторяющиеся гипотезы из списка м. исключать. Дан.вывод б.и искомым.

6°. Если из Г, А, В С, то Г, В, А С (св-во коммутативности). Гипотезы в списке м.менять местами.

6. Исчисление выс-й (ИВ) – пример простейшей формализованной мат.теории. Здесь дается точное опр-е ф-лы, формулируются явно аксиомы и правила вывода, дается точное опр-е доказуемой ф-лы (т.е. теоремы).(ИВ) входит составной частью в более сложные формализованные теории (формальную арифметику, формальную геометрию и т.д.).

Формальные теории строятся по единому плану: Построение исчисления выс-й. Зададим алфавит из след. групп символов:x, y, …, z,..., А, В, … – пропозициональные переем-е;®,Ø – лог.связки;(,) – технические сим-лы.Дадим опр-е ф-лы исчисления выс-й (или правильно построенной формулы – п.п.ф.):каждая пропозициональная пер-я явл-ся п.п.ф. (простейшей, атомной).Если А – п.п.ф. (ИВ), то (ØА) – п.п. ф-ла (ИВ).Если А и В – п.п. ф-лы исчисления выс-й, то (А®В) – тоже п.п. ф-ла (ИВ).Никаких других п.п. ф-л (ИВ), кроме получающихся согласно п.п.1–3, нет.Нек.из п.п.ф. особенно важны. Им отводится роль основного материала, из кот.строится все ИСЧИСЛЕНИЕ. Мы выделяем эти ф-лы и называем их аксиомами. Выбор некот.ф-л в кач-ве аксиом произволен и определяется только тем, какое исчисление желательно получить. Нас интересует только вопрос: как из некоторых п.п.ф. при помощи некоторой процедуры получить другие п.п.ф. и какие п.п.ф. так можно получить. Аксиомами назовем ф-лы вида:

(А1):А®(В®А);(А2):А®(В®С)®((А®В)®(А®С)) – з-н самодистрибутивности импликации;(А3):() (A B)– з-н контрапозиции.Дан.ф-лы пред-т из себя схемы аксиом: в них вместо любой буквы м.б.записана люб.п.п.ф. (одна и та же во всех вхождениях буквы). Н-р, A1:(x y) (( (z x)) (x y))– сделаны з-ны А=(x®y),В= (z®x).Все остальные ф-лы б.док-ть, ссылаясь на перечисленные.Для построения (ИВ) надо указать также правила вывода, т.е. правила, по кот.из одних п.п.ф. можно строить другие п.п.ф.Для нашего (ИВ) мы возьмем одно правило вывода, которое называется modus ponens (правило отделения или гипотетический силлогизм).

(MP): – условная запись правила.Из ф-л А и А®В считается выводимой ф-ла В. А наз-ся малой посылкой, А®В – большой посылкой, В – заключением.Выводом ф-лы А (формальным док-вом) наз-ся конечная послед-ть ф-л, заканчивающаяся ф-лой А и каждая ф-ла в этой послед-ти явл-ся аксиомой или получена из двух предыдущих по правилу (MP).Если для ф-лы А такой вывод построен, то она наз-ся доказуемой или выводимой в (ИВ) (или теоремой (ИВ)), в этом случае б. записывать: A-выводима ф-ла А.

ИСЧИСЛЕНИЕ содержит выводимые ф-лы (в дан.аксиоматике с пом-ю дан.правил вывода).Пр-ры выводимых ф-л. В (ИВ) выводимы ф-лы:

1. А®A

x→ (y®z)®((x®y)®(x®z)) (A2). 1). A→((B→A)→A)→((A→ (B→A))→(A→A)). 2). A→((B→A)→A) (A1). 3). (A→(B→A))→(A→A) из 1),2) по (МР). 4). A→(B→A) (A1). 5). A→A из 3),4)по (МР).

Вывод содержит 5 формул.

2. ®(А®B)

Запишем аксиому А2: x®(y®z)®((x®y)®(x®z)). Сделаем переобозначение перем-х:

x→ (y®z)®((x®y)®(x®z)). (A2). 1) →(( → ) (A→B)) (( →( → ))→( →(A→B))) (A2). 2). ( → )→(A→B) (A3). 3). (2)→( →(2)) ()→(A→B)→( → ))) (A1). 4). →(2) →(( → )→(A→B)) из 2)3) по (МР).5) →( → )→( →(A→B))) из1),4)по (МР).

6). →( → ) (A1).

7). ( →(A→B)) из 5),6) по (МР).

Вывод содержит 7 ф-л.

3. ®( ®A)

Запишем аксиому А2: x®(y®z)®((x®y)®(x®z)). Сделаем переобозн-е пер-х:

x®(y®z)®((x®y)®(x®z)) (A2). 1) →(( 2). ()→( →A) (A3). 3). (2)→( →(2)) ( ( →A)→( →(( → )→( →A)))(A1). 4). ( →(2)) ( →(( →( →A))) из 2),3) по (МР). 5). ( →( 6). → 7). ( →A) из

5),6) по (МР).Вывод содержит 13 ф-л.

A

x®(y®z)®((x®y)®(x®z)) (A2). 1). →( →A)→(( → )→ ( →A)) (A2). 2). →( →A) 3-й пример – 13 формул. 3). (( → )→( →A)) из 1),2)по (МР). 4). ( → ) 1-й прмер – 5 формул. 5). ( →A) из 3),4) по (МР).

5. А®

( → )→(x→y) (A3). 1).( → )→(A→ ). 2). ( → ) 4-й пример – 21 формула. 3). (A→ ) из1),2) по (МР).

Вывод содержит 23 ф-лы.