Повна версія

Головна arrow Природознавство arrow ІНТЕЛЕКТУАЛЬНІ СИСТЕМИ

  • Увеличить шрифт
  • Уменьшить шрифт


<<   ЗМІСТ   >>

ПОВНОТА ЧИСЛЕННЯ ВИСЛОВІВ

Існує багато різних дедуктивних систем для опису загальнозначущих формул логіки висловлювань, що відрізняються великою кількістю використовуваних логічних зв'язок і вибором аксіом; наведемо тут одну з найпростіших таких систем в якій розглядаються лише дві логічні связкі-- «, -

Решта логічні зв'язки легко можуть бути виражені через них і трактуватися як свого роду "скорочені позначення" для відповідних формул з - »і - ?. Аксіоми даної дедуктивної системи задаються за допомогою так званих

схем аксіом.

А1) Якщо /, д- формули, то формула

є аксіома.

А2) Якщо /, д, h - формули, то формула є аксіома.

АЗ) Якщо f, д - формули, то формула

є аксіома.

Насправді кожна зі схем аксіом Al, А2, АЗ визначає безліч аксіом, що відрізняються вибором формул f, g, h.

Правило виводу в цій дедуктивної системі одне - якщо вже отримані загальнозначущі формули / і (/ - * у), то з них виводиться загальнозначуща формула g (відповідно до класифікації запропонованої ще Аристотелем, це правило називається modus ponens).

Щоб проілюструвати техніку, яка застосовується при вивченні дедуктивних систем, наведемо схематичні начерки доказів деяких важливих властивостей тільки, що певною дедуктивної системи.

Висновком формули / зі списку формул Г = <7i, ..., g n будемо називати довільну послідовність формул / ь / г, ..., / т = /, таку, що кожне / ДГ = 1 ,, тп) є або аксіома, або елемент списку Г, або отримано за правилом modus ponens з деяких fj, Д, при j, k € {l, ..., t - 1}. Якщо існує висновок / з Г, то позначаємо цю обставину за допомогою Г Ь / (зокрема, список Г може бути порожній; ті формули, які виводяться з пустого Г, як легко можна бачити, утворюють клас всіх виведених формул нашої дедуктивної системи). Наступна лема є приклад виведеної формули.

Лемма 7. Якщо / - формула, то (- (/ -? /).

Доведення. Наступна послідовність формул, що представляє собою висновок з пустого Г, доводить твердження.

Перший її елемент - аксіома, яка виникає за схемою аксіом А2; другий і четвертий - аксіоми по А1; третій і п'ятий - отримані застосуванням правила виведення. ?

Має місце наступне важливе твердження, відоме як теорема дедукції (Ербран).

Теорема 18. Якщо Г - список формул і /, д - формули, то з Г, / Т- д випливає Г Ь (/ -> д).

Доведення. Дане твердження доводиться індукцією по довжині п виведення <7ь ... , д п = 9 формули д з Г, /.

Базис індукції. Якщо п = 1, то g або аксіома, або елемент списку Г, /. У першому випадку висновок (/ - * д) з Г має вигляд - *? (/ -> д)), д , (/ - * д). У другому випадку можливі два подслучая - якщо д € Г, то знову беремо вказаний вище висновок; якщо ж д = /, то використовуємо наведений вище висновок (/ -? /) з пустого списку.

Індуктивний перехід. Якщо п> 1 і g - аксіома, або елемент списку Г, /, то чинимо так само як вище. Нарешті якщо g отримано за правилом modes ponens з формул 9ti9j> (hj < п ) "то згідно з припущенням індукції маємо Г Ь (/ -> pj), Г h (/ - + gj). Зауважимо, що одна з формул gi, gj , наприклад gj, повинна мати вигляд (# -> д). Для отримання висновку (/ -? Д) з Г тепер досить розглянути послідовність утворену розташованими поспіль висновками (/ - * <7j), (/ -> д ^) з Г, і приєднати до неї в кінці формули ((/ { -? д)) -> (((/ - + g t ) -> (/ -? $))),

((/ 9г) - "(/ - * 9 )), (/ -> р). Перша з цих формул є

аксіома отримана за схемою аксіом А2; дві останні отримані застосуванням правила виведення. ?

Для доказу того, що кожна загальнозначуща формула алгебри логіки виводиться в розглянутій нами дедуктивної системі, нам знадобляться такі допоміжні затвердження.

Лемма 8 (доказ від протилежного). Якщо Г - список формул і f, д - формули, то з Г, - "/ Ь д, ~ <д випливає гь /.

Доведення. Так як Г, - "/ Ь д, -" д, то по теоремі дедук- ції ГI- (-> / - » д), (-> / -> -> д).

Висновок / з Г наступний:

Тут спочатку використовується аксіома АЗ, а потім - двічі правило modus ponens. ?

Лемма 9 (зняття подвійного заперечення). Якщо f - формула, то Т- (-1-1 / -? /).

Доведення. Наступне твердження очевидно:

Використовуючи лему 8, отримуємо-год-год / Ь /. Звідси по теоремі дедукції маємо I- (- "-> / -? /). ?

Лемма 10. Якщо / - формула, то h (/ -?-Год-год /).

Доведення. За лемі 9 маємо /, -> - * - * / I- /, - "/. Використовуючи лему 8, отримуємо / I - »-» /. Звідси по теоремі дедукції маємо Ь (/ ->-год-год /). ?

Докази наступних трьох тверджень рекомендуються в якості самостійних вправ.

Лемма 11. Якщо / - формула, то Ь (-> / - * (/ -> у)).

Лемма 12. Якщо f - формула, то h (/ -? (-Год? - »* год (/ - * <7))). Лемма 13. 2? Кщо / - формула, то

Для довільної формули д і деякої інтерпретації / мови логіки висловлювань позначимо за допомогою ( g) j формулу, яка співпадає з д, якщо значення д в інтерпретації / є І, і збігається з (-47) в іншому випадку.

Лемма 14. Нехай { - формула логіки висловлювань; Xit ..., х п - всі змінні входять до f, і I - деяка інтерпретація мови логіки висловлювань. Тоді виконується (Xl) l, ..., (x n ) l ь (Л /.

Доведення. Це твердження будемо доводити індукцією по числу т логічних зв'язок в /.

Базис індукції. Якщо т = 0, то / збігається з ii, і твердження зводиться до очевидного факту (xi) / h (xi) /.

Індуктивний перехід. Нехай т > 0. Розглянемо наступні два випадки.

  • 1) / має вигляд (- » h ). Цей випадок розбивається на наступні подслучаі.
  • а) Якщо ( h) j = Д, то (/) / = За припущенням індукції маємо (xi) /, ..., (х п ) / Ь h. За лемі 10 маємо h -? Застосовуючи modus ponens, отримуємо (- »-» / i).
  • б) Якщо ж (h) / = (- »/ i), то (/) / = / = (-'Л), і твердження зводиться до припущення індукції.
  • 2) / має вигляд (/ ii -? / 12). Цей випадок розбивається на наступні подслучаі.
  • а) Якщо (hi) / = (- «/ ii), то (/) / = / = (hi -> Л 2 ). За припущенням індукції маємо (xi) /, ..., (x n ) / Ь (-> / 1). За лемі 11 маємо (-'hi -? (/ Ц -? / 12)) - Застосовуючи modus ponens, отримуємо (hi -? / 12) -
  • б) Якщо (Л 2 ) / = ~ 'h 2} то (/) / = / = (hi -> Д 2 ) .По аксіомі А1 маємо / i 2 -? (hi -> h 2 ). За припущенням індукції (xi) /, ..., (a: n ) / Ь h 2 . Застосовуючи modus, ponens отримуємо (hi -? H 2 ).
  • в) У випадку (hi) / = hi і (h 2 ) / = -> / i 2 маємо (/) / = -i / =
  • -? Д 2 ) - По припущенням індукції

За лемі 12 маємо (h -? (- * / 12 - * - * / * 2))) - Двічі застосовуючи modus ponens, отримуємо -> (hi -> h 2).

?

Теорема 19 (про повноту числення висловів). Формула логіки висловлювань є общезначима тоді і тільки тоді, коли вона виведена в розглянутій дедуктивної системі зі схемами аксіом Л 1 , А 2 , АЗ і правилом виведення modus ponens.

Доведення. Достатність. Якщо / і (/ -н? Д) - • загальнозначущі формули, то зрозуміло, що і формула д - загальнозначуща. Отже, правило modus ponens з загальнозначущих формул виводить загальнозначущі. Оскільки, як легко бачити, схеми аксіом задають загальнозначущі формули, то всі виведені формули - загальнозначимі.

Необхідність. Будемо позначати за допомогою / а , де про G {І, Л}, формулу / в разі а = І, і формулу (- «/) в разі а = Л. Нехай / довільна загальнозначуща формула алгебри логіки, і х , ... , х п - всі вхідні в неї змінні. Покажемо індукцією по до , що для будь-якого цілого невід'ємного до, до <п, і будь-якого набору (<7i, ..., а до) логічних констант І, Л виконується х ° 1 , ..., x? fc Н /.

Базис індукції, до = п, тобто задана інтерпретація / = ({ji, ..., <7 "). Так як (х *) / = xf *, то по лемі 14 маємо

4 1 . h (/) / = / •

Індуктивний перехід. Якщо дане твердження вже доведено для деякого до у до> 0, то розглянемо довільний набір (<7i, ..., afc_i) констант І, Л. За припущенням індукції, маємо 1 , ..., x ak k Si , х * Т- / і х * 1 , ...,, - * х * Ь /. за

теоремі дедукції знаходимо звідси х * [ 1 , ..., х ** ^ 1 I- (х * - »/) і Xjх ^ 1 Ь (- * х * -? /). За лемі 13 маємо (х * -> /) - "((-1Х * -» /) - "/). Двічі скориставшись правилом modus ponens, отримуємо xj 1 , ..., х? * ^ ! Ь /. Крок індукції, таким чином, доведено.

При до = 0 остаточно отримаємо h /. ?

 
<<   ЗМІСТ   >>