Студопедия

Главная страница Случайная страница

КАТЕГОРИИ:

АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника






Метатеорема о дедукции.






Впервые данная теорема была сформулирована в 1930 году Эрбраном. Поэтому иногда ее называют теоремой Эрбрана. Но как общий методологический принцип, характеризующий аксиоматические дедуктивные системы, она появилась у А.Тарского.

Метатеорема о дедукции формулируется так:

Если А1,... Аn-1, Аn |- В, то А1,... Аn-1 |- Аn É В.

То есть если из формул А1,... Аn-1 и Аn выводимо В, то из формул А1,... Аn-1 выводима импликация Аn É В.

Другими словами: «Если дано доказательство формулы В из А1,... Аn-1, Аn, то можно построить на его основе доказательство импликации Аn É В из А1,... Аn-1».

Выводимость формулы на основе теоремы о дедукции характеризуется тремя особенностями, выражаемыми в следующих правилах:

а) из произвольных формул А1,... Аn выводима каждая из этих формул:

А1,... Аn |- Аi где 1 Ô і Ô n;

б) из произвольных формул А1,... Аn выводима каждая формула, выводимая в S2:

А1,... Аn |- R (R – выводимая формула в S2);

в) если из произвольных формул А1,... Аn выводимы посылки правила МР, то из них также выводимо заключение правила MP.

Данные особенности выводимости (дедукции) становятся очевидными на основе следующих семантических соображений:

1). Особенность а) выражает свойство рефлексивности следования «посылка следует из самой себя»: А |= А, так как |= А É А.

2). Особенность б) выражает свойство истинных (выводимых) формул «каждая истиная формула рассматривается в качестве консеквента логически истинной импликации с произвольным антецедентом».

3). Особенность в) фиксируется следующим образом: «если из А1,... Аn |- В¢ и из

А1,... Аn |- В¢ É В¢ ¢, то |= В¢ É В¢ ¢, а это возможно, когда |= В¢ ¢».

Перейдем к доказательству метатеоремы о дедукции:

Пусть вывод формулы В из посылок А1,... Аn-1, Аn представляет из себя последовательность формул B1, B2, … Bm, где Bm = В. Преобразуем каждую формулу Bi (і = 1, 2, …m) в формулу Аn É Вi. Тогда плучим последовательность формул Аn É В1, Аn É В2 , … Аn É Вm. В ней последней формулой является нужное нам заключение, но, к сожалению, эта последовательность в общем случае не может считаться доказательством формулы B.

Чтобы превратить ее в нужное нам доказательство, потребуется между некоторыми формулами данной последовательности вставить дополнительные формулы такие, чтобы рассматриваемая последовательность превратилась в вывод Аn É В из гипотез А1,... Аn-1. Для каждого і = 1, 2, …m выбор тех формул, которые следует поместить перед формулой Аn É Вi, зависит от основания, по которому Вi вошло в последовательность B1, B2, … Bm. Здесь возможны четыре случая, которые мы сейчас рассмотрим.

І. Вi может быть одним из допущений А1,... Аn-1, например, Вi = А1. В этом случае формула Аn É Вi имеет вид Аn É А1. Тогда перед данной формулой вставляем следующую последовательность формул:

1) А1 допущение

2) А É (В É А). - А 1

3) А1 É (Аn É A1) - по п/п в 1: А/А1, В/Аn

4) Аn É А1 - по МР к 1,, 3.

П. Вi является последним допущением, то есть Вi = Аn. Тогда перед формулой Аn É Аn вставляем следующую последовательность формул:

1) А É А - теоремa в S2

2) Аn É Аn - по п/п в 1: А/Аn.

Ш. Вi является аксиомой. Тогда перед Аn É Вi вставляем следующую последовательность формул:

1) Вi - аксиома

2) А É (В É А). - А 1

3) Вi É (Аn É Вi) - по п/п в 2: А/ Вi, В/Аn

4) Аn É Вi - по МР к 1,, 3.

IV. Вi получается из двух предыдущих формул Вj Вk(j, k < i) последовательности

B1, B2, … Bm применением правила MP. В этом случае формула Вk имеет вид Вj É Вi, и интересующая нас часть последовательности B1, B2, … Bm имеет следующий вид:

p) Аn É Вj

……………

q) Аn É (Вj É Вi)

…………….

r) Аn É Вi.

Чтобы данная последовательность давала вывод Аn É Вi, преобразуем ее следующим образом:

p) Аn É Вj

………………

q) Аn É (Вj É Вi)

q + 1) (А É (В É С) É ((А É В) É (А É С)) -- A2

q + 2) (Аn É (Вj É Bi) É ((Аn É Вj) É (Аn É Bi)) - по п/п в q + 1): A/An, B/Bj, C/Bi

q + 3) (Аn É Вj) É (Аn É Bi) - по MP к q), q + 2)

q + 4) (Аn É Bi) - по MP к p), q + 3).

 

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

 

3. Металогические принципы в S2.

Свойства разрешимости, непротиворечивости, полноты и независимости (аксиом) называют металогическими принципами. Анализируют данные принципы путем доказательства соответствующих метатеорем.


Поделиться с друзьями:

mylektsii.su - Мои Лекции - 2015-2024 год. (0.008 сек.)Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав Пожаловаться на материал