Основы полярной логики1 icon

Основы полярной логики1



НазваниеОсновы полярной логики1
страница1/3
Дата конвертации28.08.2012
Размер0.73 Mb.
ТипДокументы
  1   2   3

Основы полярной логики1


 В.И.Моисеев, 2011 г.


§ 1. Аксиомы и первичные определения полярной логики


Рассмотрим формальную аксиоматическую теорию ПЛ (полярная логика).

Язык этой теории строится следующим образом.


Алфавит:


  1. Пропозициональные константы 0,1, Кji, pi, Pi, где i=1,…,n, ji=1,…,mi,

  2. Символы логических связок: ,,.


Множество правильно построенных выражений (ППВ):


  1. Базис: константы есть атомарные ППВ,

(2) Индуктивное предположение: если х, у – ППВ, то х, ху, ху – ППВ.

  1. Замыкание: иных ППВ нет.


Примем в этой теории метавыражения вида


|-у х, где х и у – ППВ языка ПЛ.


Такое выражение будет означать, что выражение х обоснована на меру выражения у. Частным случаем таких выражений будет запись


|-1 х.


Это означает, что х обоснована на меру полной истинности, что соответствует классической теоремности в логике высказываний.


Примем в ПЛ следующие схемы аксиомы2:


Аксиомы булевой алгебры:


В1. |- 1 х  у  у  х

В2. |- 1 х  у  у  х

В3. |- 1 (х  у)  z  x  (у  z)

В4. |- 1 (х  у)  z  x  (у  z)

В5. |- 1 х  (х  у)  х

В6. |- 1 х  (х  у)  х

В7. |- 1 х  (у  z)  (ху)  (хz)

В8. |- 1 х  (у  z)  (ху)  (хz)

В9. |- 1 x х  1

В10. |- 1 xх  0


Кроме того, примем дополнительные схемы аксиом:


В11. |- 1 1

В12. |- 1 (ху)х

В13. |- 1 (ху)у

В14. |- 1 х(ху)

В15. |- 1 хх

B16. |- 1 (xy)z(x)  z(y), где z(x) – выражение z, подвыражением которой является х

В17. |- 1 х  у  (ху)

Здесь, как обычно,

(DE) ху означает (ху)(ух),

где

(DI) ху – это ху.

Для констант р1,…,рn, Р1,…,Рn и Кji (если последние есть) примем следующие аксиомы полярности:

(posi) |-pi pi,

(Posi) |-Рi Рi,

(PosKji) |-Kji Kji (если есть константы Кji),

(PP1i) |-1 (р­iPi),

(PP2ij) |-1 Рi  Рj  0, если i≠j,

(PP3) |-1 P1  …  Pn  1,

(PP4i) |-1 (pi0)  (Pipi),

(РР4Кji) |-1 (piКji)(КjiРi)(Кjipi)(PiKji) (если есть константы Кji).

В качестве одного из правил вывода будем использовать обобщенное правило отделения:

(GMP) Еcли |-1(х0) и |-1(ху), то |-у у.

Частным случаем этого правила будет обычный modus ponens:

(MP) Еcли |-1х и |-1(ху), то |-1 у.

Также примем правила:

(ЕC) Если |-1х и |-1у, то |-1ху,

(EЕ) |-а х е.т.е. |-1 ха,

(ЕD) Если |-а х и |-b у, то |-аb ху,

(ЕN) Если |-а х, то |-а х,


Под выводимостью |-у1х1,…,|-ynхn  |-ух в ПЛ будем понимать список выражений вида |-ba, где последнее выражение в этом списке есть |-ух, и каждое выражение есть либо одно из выражений |-у1х1,…,|-ynхn, либо аксиома ПЛ (в форме выражения |-ba), либо получена по одному из правил вывода из предшествующих выражений списка (предполагается, что все выражения а и b из |-ba есть ППВ из ПЛ). Выражения |-у1х1,…,|-ynхn будем в этом случае называть посылками, выражение |-ух заключением выводимости |-у1х1,…,|-ynхn  |-ух.

Под доказательством выражения |-ух будем иметь в виду выводимость |-ух из пустого множества посылок. Выражение |-ух будем называть теоремой ПЛ е.т.е. существует доказательство для |-ух.

Тот факт, что |-ух есть теорема ПЛ, будем обозначать в виде |ух.

Это значит, что может быть выражение |-ух, которое могло бы не являться |ух. Например, это некоторая гипотеза вида |-ух, относительно которой можно было бы посмотреть, что из нее можно вывести. Но в этом случае мы заранее можем не знать, является ли |-ух теоремой ПЛ или нет. Выражение |-ух лишь означает утверждение, что ППВ х обоснована на меру ППВ у (что равносильно утверждению |-1ху, согласно (ЕЕ)). Но верно это или нет, и насколько верно, этого мы не знаем без доказательства в ПЛ. Поэтому в выводах ПЛ фигурируют выражения |-ух, а не |ух. Выводы – это лишь трансформаторы одних выражений в другие. В доказательства они превращаются, когда действуют на теоремы, и сами дают в качестве своего результата теоремы.

Выражение |-ух будем называть позитивным выражением (Р-выражением) е.т.е. х и у есть ППВ и |1(y0).

Выражение |-ух является позитивной аксиомой (Р-аксиомой) в ПЛ е.т.е. |-ух есть Р-выражение, и в списке аксиом ПЛ есть аксиома |-у х.

Выражение |-ух является позитивной теоремой (Р-теоремой) в ПЛ е.т.е. |-ух есть Р-выражение, и для |-ух существует доказательство в ПЛ.

Правило вывода будем называть позитивным выводом (Р-выводом) е.т.е. это правило переводит Р-выражения в Р-выражения.

Выводимость |-у1х1,…,|-ynхn  |-ух будем называть регулярной Р-выводимостью и обозначать в виде |-у1х1,…, |-ynхnР |-ух е.т.е. все выражения в выводимости |-у1х1,…,|-ynхn  |-ух есть Р-выражения (отсюда следует, что в выводимости |-у1х1,…,|-ynхn  |-ух могут использоваться только Р- выводы).

^ Регулярным позитивным доказательством (регулярным Р-доказательством) назовем регулярную Р-выводимость из нулевого множества посылок.

Аналогичные определения могут быть введены для 1-выражений.

Выражение |-ух будем называть 1-выражением е.т.е. х есть ППВ и |1(y1).

Выражение |-ух является 1-аксиомой в ПЛ е.т.е. |-ух есть 1-выражение, и в списке аксиом ПЛ есть аксиома |-1 х.

Выражение |-ух является 1-теоремой в ПЛ е.т.е. |-ух есть 1-выражение, и для |-ух существует доказательство в ПЛ.

Правило вывода будем называть 1-выводом е.т.е. это правило переводит 1-выражения в 1-выражения.

Выводимость |-у1х1,…,|-ynхn  |-ух будем называть регулярной 1-выводимостью и обозначать в виде |-у1х1,…, |-ynхn1 |-ух е.т.е. все выражения в выводимости |-у1х1,…,|-ynхn  |-ух есть 1-выражения (отсюда следует, что в выводимости |-у1х1,…,|-ynхn  |-ух могут использоваться только 1- выводы).

^ Регулярным 1-доказательством назовем регулярную 1-выводимость из нулевого множества посылок.

Выводимость |-у1х1,…,|-ynхn  |-ух будем называть финальной у-выводимостью и обозначать |-у1х1,…,|-ynхnу |-ух.

Финальную у-выводимость |-у1х1,…,|-ynхn  |-ух будем называть финальной позитивной выводимостью (финальной Р-выводимостью) е.т.е. |-ух есть Р-выражение.

Финальную у-выводимость |-у1х1,…,|-ynхn  |-ух будем называть финальной 1-выводимостью е.т.е. |-ух есть 1-выражение.

Доказательство выражения |-ух будем называть финальным у-доказательством.

Доказательство Р-выражения |-ух будем называть финальным Р-доказательством.

Доказательство 1-выражения |-ух будем называть финальным 1-доказательством.

В качестве семантики теории ПЛ определим отображение | . | из множества ППВ языка ПЛ в множество элементов такой булевой решетки B с операциями умножения *, сложения + и дополнения C, что будут выполнены следующие соотношения:

(С1) Для каждой константы Pi, pi, Kji сопоставлены элементы |Pi|, |pi| и |Kji| соотв. из В,

(С2) |0| = 0 – ноль решетки В,

(С3) |1| = 1 – единица В,

(С4) |xу| = |х|+|у|,

(С5) |ху| = |х|*|у|,

(С6) |x| = C|x|,

(С7) Если |у х, то |x| = |y|.

Элементы решетки В можно понимать как полярные семантические значения, которые могут быть как истинностными значениями, так и более общими состояниями смысла, имеющего полярную структуру.


§ 2. Полярная логика и исчисление высказываний

Покажем, что полярная логика непротиворечива относительно исчисления высказываний (ИВ), если в ПЛ принять только аксиомы В1-В15, (pos1) и (Рos1), (PP1i) и (PP3), только 1-выводы (в 1-выводы можно перевести все выводы, кроме (EN)), отказаться от констант Kji и принять n=1. Причем, аксиома (pos1) принимается в этом случае в виде |-1 p1. Как вариант (PP3), имеем |111). Такую версию полярной логики я буду обозначать ПЛ1.

Кроме того, для ПЛ1 можем доказать следующую теорему.


Лемма Р1. |11Р1)

Док-во.

  1. |-1 p1 (pos1)

  2. |-1 p1  1 (ЕЕ), (1)

  3. |-1 Р1  1 (PP3)

  4. |-11Р1) Леммы 12, 12* (см. ниже)



Это значит, что константы р1, Р1 и 1 в ПЛ1 представляют собой одну константу 1. Покажем далее, что ПЛ1 непротиворечива относительно исчисления высказываний ИВ.


^ Теорема ПЛ1-непротиворечивости. ПЛ1 непротиворечива относительно ИВ.

Доказательство. Для доказательства этой теоремы нам нужно дать интерпретацию I ПЛ1 относительно ИВ, чтобы 1) все ППВ ПЛ1 перешли в ППВ ИВ, 2) все аксиомы ПЛ1 перешли в теоремы ИВ, 3) все выводы ПЛ1 перешли в выводимости ИВ.

  1. Используя индуктивное определение, мы можем дать следующее определение интерпретации I для ППВ ПЛ1:

(1) Базис: I(0) = AA, I(1) = I(p1) = I(P1) = AA, где А – некоторая пропозициональная переменная из языка ИВ.

(2)^ Индуктивное предположени: если х, у – ППВ ПЛ1 и определены I(x), I(y), то I(х) = I(x), I(ху) = I(x)I(y), I(ху) = I(x)I(y).


Заметим, что такая интерпретация сохраняет все связки выражений из ПЛ1, так что структура схем аксиом будет сохранена.

  1. Известно, что моделью ИВ является булева алгебра на двух элементах 0 и 1. Это значит, что все аксиомы булевой алгебры В1-В8 будут теоремами ИВ. Вообще надо заметить, что в ПЛ1 остаются аксиомы В1-В15, (pos1) и (Рos1), (PP1i) и (PP3). Все они будут тавтологиями при интерпретации I. Известно, что ИВ является полной системой, т.е. все тавтологии являются в ИВ теоремами. Таким образом, все аксиомы ПЛ1 при интерпретации I перейдут в теоремы ИВ.

  2. Обратимся теперь к правилам вывода в ПЛ1. Выражения вида |1x из метаязыка ПЛ1 будем интерпретировать как выражения |-I(x) в метаязыке ИВ3. 1-выводимость |-1х1,…,|-1хn  |-1х из ПЛ1 будем интерпретировать как выводимость I(х1),…,I(хn) |- I(х) в ИВ. Правила вывода (в форме 1-выводов) в ПЛ1 - это (GMP), (MP), (ЕC), (EE) и (ED). В ИВ получим: |-((х0)  х). Отсюда следует, что (GMP) совпадет в ПЛ1 с (MP), а (MP) есть вывод в ИВ. Правила вывода (ЕC), (EE), (ED) и (ЕS) есть выводимости в ИВ при данной интерпретации.

Теорема доказана.


В рамках Теоремы ПЛ1-непротиворечивости язык системы ПЛ1 интерпретируется как часть языка ИВ, построенная над формулами АА и АА как атомарными выражениями. Семантика ПЛ1 совпадает с семантикой ИВ. Такую логическую систему, которая включает в себя указанную часть языка ИВ, можно обозначить как систему ИВ(ПЛ1). Системы ПЛ1 и ИВ(ПЛ1) эквивалентны по языку. В то же время система ИВ(ПЛ1) так же полна, как и вся система ИВ. Отсюда можно сформулировать теорему полноты системы ПЛ1.


^ Теорема ПЛ1-полноты. ПЛ1 полна.

Доказательство. Пусть х – ППВ из ПЛ1. Тогда I(x) – ППВ из ИВ(ПЛ1). Если х – теорема ПЛ1, т.е. |1x, то, в силу Теоремы ПЛ1-непротиворечивости, имеем, что |-I(x), т.е. I(x) есть теорема ИВ(ПЛ1). Поскольку ИВ(ПЛ1) – часть ИВ, то I(x) есть теорема ИВ, и в силу полноты ИВ, I(x) – тавтология, т.е. семантика I(x) есть 1. Для семантических отношений в ПЛ1 имеем:

(С2) |0| = 0 = |AA| = |I(0)|,

(С3) |1| = 1 = |AA| = |I(1)| = |I(p1)| = |I(P1)|,

(С4) если |I(x)| = |x| и |I(y)| = |y|, то |xу| = |х|+|у| = |I(x)|+|I(y)| = |I(x)I(y)| = |I(xy)|,

(С5) если |I(x)| = |x| и |I(y)| = |y|, то |ху| = |х|*|у| = |I(x)|*|I(y)| = |I(x)I(y)| = |I(xy)|,

(С6) если |I(x)| = |x|, то |x| = C|x| = C|I(x)| = |I(x)| = |I((x))|,

Отсюда следует, что |I(x)| = |x|. Таким образом, в нашем случае для ППВ х имеем: |I(x)| = 1 = |x|, т.е. х истинна в семантике ПЛ1.


Теперь мы можем посмотреть на ситуацию в обратном направлении, проведя интерпретацию системы ИВ(ПЛ1) в ПЛ1. Для этого будем использовать интерпретацию I* следующего вида (по-прежнему имеем в виду, что язык ИВ(ПЛ1) строится над формулами AA и AA как атомарными выражениями):

(1) Базис: I*(AA) = 0, I*(AA) = p1, I*(ВВ) = P1, где В есть AA, I*(CC) = 1, где C есть ВВ.

(2)^ Индуктивное предположени: если Х, У – ППВ ИВ(ПЛ1) и определены I*(Х), I*(У), то I*(Х) = I*(Х), I*(ХУ) = I*(Х)I*(У), I*(ХУ) = I*(Х)I*(У).


Относительно интерпретации I* может быть доказана следующая теорема.


^ Теорема обратной непротиворечивости. Любая теорема ИВ(ПЛ1) является теоремой ПЛ1 при интерпретации I*.

Доказательство. Будем рассматривать версию ИВ, представленную в книге Э.Мендельсона4. Здесь принимаются три основных схемы аксиомы:

(A1) A(BC),

(A2) (A(BC))  ((AB)(AC)),

^ (A3) (BA)  ((BA)B).

В качестве единственного правила вывода используется (MP). Покажем, что в рамках интерпретации I* каждая аксиома ИВ(ПЛ1) является теоремой ПЛ1 и каждое правило вывода из ИВ(ПЛ1) является выводимостью в ПЛ1. Поскольку интерпретация I* сохраняет схему выражения, то правило вывода (МР) перейдет при интерпретации I* в правило вывода (МР) системы ПЛ1. Остается рассмотреть схемы аксиом.

Рассмотрим отдельно каждую схему аксиом (А1)-(А3).

Для схемы аксиом (А1) получим I*(A(BА)) = I*(A)(I*(B)I*(А)), т.е. ту же схему. Как уже было отмечено, схемы выражений будут вообще сохраняться при отображении I*, в том числе и для отображений (А2) и (А3).

Пусть I*(A) есть х, и I*(В) есть у. Тогда I*(A)(I*(B)I*(А)) есть х(ух). Выражение х(ух) может быть представлено как сокращение для х(ух). Ниже я приведу доказательство в ПЛ1 для этого выражения (указания на знак |-1 в выражении |-1x в доказательствах я буду опускать). Предварительно будут доказаны вспомогательные леммы 1-7, а окончательное доказательство теоремы х(ух) будет дано в лемме 8.

Лемма 1. х, ху |-1 у

Док-во.

  1. х посылка

  2. ху посылка

  3. (ху)(ух) (DE) (2)

  4. (ху)(ух)  (ху) (В12)

  5. ху (MP) (3), (4)

  6. у (MP) (1), (5)

Аналогично, используя (В13) вместо (В12), может быть доказана

Лемма 2. у, ху |-1 х


Лемма 3. ху |-1 ух

Доказательство.

  1. ху посылка

  2. ху  ух (В1)

  3. ух Лемма 1 (1), (2)

Аналогично, используя (В2) вместо (В1), может быть доказана

Лемма 4. ху |-1 ух


Лемма 5. (х  у)  z |-1 x  (у  z)

Док-во.

  1. (х  у)  z посылка

  2. (х  у)  z  x  (у  z) (В3)

  3. x  (у  z) Лемма 1 (1), (2)

Аналогично может быть доказана

Лемма 6. (х  у)  z |-1 x  (у  z)


Лемма 7. (xy), z(x) |-1 z(y)

Док-во.

  1. xy посылка

  2. z(x) посылка

  3. (xy)z(x) (ЕС) (1), (2)

  4. (xy)z(x)  z(y) (В16)

  5. z(y) (MP) (3), (4)



Лемма 7*. (xy), z(у) |-1 z(х)

Док-во.

  1. xy посылка

  2. z(у) посылка

  3. ху  ух (DE), (1)

  4. ух  ху Лемма 4, (3)

  5. ух (DE), (4)

  6. z(х) Лемма 7, (2), (5)



Лемма 8. |-1 х(ух).

(1) 1 В11

(2) x х  1 В9

(3) x х Лемма 2

(4) (x х)  (x х)  у (В14)

(5) (x х)  у (MP) (3), (4)

(6) (x х)  (х  х) (В1)

(7) (х  х)  y Лемма 7 (5), (6)

(8) х  (х  y) Лемма 5 (7)

(9) (х  y)  (y  x) (В1)

(10) х  (y  x) Лемма 7 (8), (9)


Теперь перейдем к доказательству того, что вторая аксиома (А2) при интерпретации I* переходит в теорему ПЛ1. Для этого достаточно показать, что теоремой ПЛ1 является выражение (х  у  z)  (x  y)  (x  z). Как и ранее, я приведу вспомогательные леммы 9-20, которые нам потребуются для окончательного доказательства. Последнее будет дано в лемме 21.

Лемма 9. |-1 x  x

Док-во.

  1. 1 В11

  2. x х  1 В9

  3. x х Лемма 2, (1), (2)



Лемма 10. х |-1 ху

Док-во.

  1. х посылка

  2. х(ху) В14

  3. ху (МР), (1), (2)



Лемма 11. (x  y)  (z  p) |-1 (x  (z  p))  y

Док-во.

  1. (x  y)  (z  p)

  2. x  (y  (z  p))

  3. y  (z  p)  (z  p)  y

  4. x  ((z  p)  y)

  5. (x  (z  p))  y

Это пример лемм, которые, опираясь на свойства коммутативности и ассоциативности, позволяют переходить к выражениям с любым порядком элементов и расстановкой скобок для ППВ с одной связкой. Далее я буду применять такие переходы, ссылаясь на общее название «Леммы переупорядочивания». Благодаря таким леммам мы вообще можем опускать скобки или расставлять их в любом порядке, используя выражения с многократным повторением конъюнкции или дизъюнкции.


Лемма 12. xy, yz |-1 xz

Док-во.

  1. xy посылка

  2. yz посылка

  3. xz Лемма 7*, (1), (2)



Лемма 12*. xy |-1 yx

Док-во.

  1. xy посылка

  2. (xy)  (yx) (DI), (1)

  3. (yx)  (xy) Лемма 4, (2)

  4. yx (DE), (1)



Лемма 13. х  (у  z) |-1 (х  у)  (х  z)

Док-во.

  1. х  (у  z) посылка

  2. х  (у  z)  (ху)  (хz) В7

  3. (ху)  (хz) Лемма 1, (1), (2)



Аналогично могут быть доказаны

Лемма 13*. (х  у)  (х  z) |-1 х  (у  z)

Лемма 13**. х  (у  z) |-1 (х  у)  (х  z)


Лемма 14. |-1 (у  z)  х  (у  х)  (z  х)

Док-во.

  1. х  (у  z)  (ху)  (хz) посылка

  2. х  (у  z)  (у  z)  х В1

  3. (х  у)  (у  х) В1

  4. (х  z)  (z  х) В1

  5. (у  х)  (z  х) Лемма 7, (1)-(4)



Лемма 15. (x  y  x)  1

Док-во.

  1. 1 В11

  2. 1  (х  у  х) В14, (1)

  3. (х  у  х)  1 Лемма 3, (2)

  4. (x  y  x)  1 (DI), (3)

  5. х  х Лемма 9

  6. (х  х)  (1  у) В14, (5)

  7. 1  (х  у  х) Леммы переупорядочивания

  8. 1  (х  у  х) (DI), (7)

  9. ((x  y  x)  1)  (1  (х  у  х)) (ЕС), (4), (8)

  10. (x  y  x)  1 (DЕ), (9)



Лемма 16. 1  z  z

Док-во.

  1. z  z Лемма 9

  2. z  z Лемма 3, (1)

  3. (z  z)  1 В14, (2)

  4. 1  (z  z) Лемма 3, (3)

  5. (1  z)  z Лемма 5, (4)

  6. (1  z)  (1  z) B17, (5)

  7. (1  z)  z Лемма 7, (5), (6)

  8. (1  z)  z (DI), (7)

  9. z  z Лемма 9

  10. z  z Лемма 3, (9)

  11. 1 B11

  12. 1  z В14, (10)

  13. z  1 Лемма 3, (11)

  14. (z  1)  (z  z) (EC), (10), (12)

  15. z  (1 z) Лемма 13*, (14)

  16. z  (1 z) (DI), (15)

  17. ((1  z)  z)  (z  (1 z)) (ЕС), (8), (16)

  18. 1  z  z (DЕ), (9)



Лемма 17. (x  x)  y  y

Док-во.

(1) 1  y  y Лемма 16

(2) x  x  1 В9

(3) (x  x)  y  y Лемма 7, (1), (2)


Лемма 18. xy |-1 yx

Док-во.

  1. xy посылка

  2. x  y (DI), (1)

  3. y  x Лемма 3, (2)

  4. yy В15

  5. y  x Лемма 7, (3), (4)

  6. yx (DI), (5)



Лемма 19. xy |-1 xy

Док-во.

  1. xy посылка

  2. (xy)  (yx) (DE), (1)

  3. xy В12, (2)

  4. yx В13, (2)

  5. yx Лемма 18, (3)

  6. xy Лемма 18, (4)

  7. (xy)(yx) (ЕС), (5), (6)

  8. xy (DE), (7)



Лемма 20. (x  y)  (x  y)

Док-во.

  1. х  у  (ху) В17

  2. (х  у)  (ху) Лемма 19, (1)

  3. x  х B15

  4. y  y B15

  5. (ху)  (ху) B15

  6. (х  у)  (ху) Лемма 7, (2), (3), (4)

  7. (x  y)  (x  y) Лемма 12*, (6)



Теперь мы можем доказать, что вторая аксиома (А2) при интерпретации I* переходит в теорему ПЛ1.


Лемма 21. |-1 (х  у  z)  (x  y)  (x  z)

  1. z  z Лемма 9

  2. (z  z)  (y  x) Лемма 10, (1)

  3. (z  y  x)  z Леммы переупорядочивания, (2)

  4. x  x Лемма 9

  5. (x  x)  y Лемма 10, (4)

  6. x  y  x Леммы переупорядочивания, (5)

  7. (x  y  x)  ((z  y  x)  z) (ЕС), (6), (3)

  8. ((x  y  x)  (z  y  x))  ((x  y  x)  z) Лемма 14, (7)

  9. (x  y  x)  1 Лемма 15

  10. ((x  y  x)  (z  y  x))  (1  z) Лемма 7, (8), (9)

  11. 1  z  z Лемма 16

  12. (x  y  x)  (z  y  x)  z Лемма 7, (10), (11)

  13. (x  y  x)  (z  y  x)  ((x  y)  (z  y))  x) B7, B1, Лемма 12*

  14. ((x  y)  (z  y))  x)  z Лемма 7, (12), (13)

  15. (y  y)  (z  y)  (z  y) Лемма 17

  16. ((x  y)  (y  y)  (z  y))  x)  z Лемма 7, (14), (15)

  17. ((x  y)  (y  y)  (z  y)  ((x  y  z)  y) B7, B1, Лемма 12*

  18. ((x  y  z)  y)  x)  z Лемма 7, (16), (17)

  19. (x  y  z)  (y  x)  z Леммы переупорядочивания, (18)

  20. (x  x)  (y  x)  (y  x) Лемма 17

  21. (x  y  z)  ((x  x)  (y  x))  z Лемма 7, (19), (20)

  22. ((x  x)  (y  x))  ((x  y)  x) B7, B1, Лемма 12*

  23. (x  y  z)  ((x  y)  x)  z Лемма 7, (21), (22)

  24. x  x В15, Лемма 12*

  25. y  y В15, Лемма 12*

  26. (x  y  z)  (x  y)  x  z Лемма 7, (23), (24), (25)

  27. (x  y  z)  (x  y  z) Лемма 20

  28. (x  y)  (x  y) Лемма 20

  29. (x  y  z)  (x  y)  (x  z) Лемма 7, (27), (28)



Наконец, покажем, что третья аксиома (А3) при интерпретации I* переходит в теорему ПЛ1. Для этого достаточно показать, что теоремой ПЛ1 является выражение (y  x)  (y  x)  y.


Лемма 22. |-1 (y  x)  (y  x)  y

Док-во.

  1. y  y Лемма 9

  2. y  y Лемма 9

  3. y  (x  x)  y Лемма 17, Лемма 4

  4. y  (x  x)  y Лемма 7, (2), (3)

  5. y  (x  x)  (y  x)  (y  x) В8

  6. ((y  x)  (y  x))  y Лемма 7*, (4), (5)

  7. (y  x)  (y  x) Лемма 20

  8. (y  x)  (y  x) Лемма 20

  9. ((y  x)  (y  x))  y Лемма 7*, (6), (7), (8)

  10. x  x В15

  11. ((y  x)  (y  x))  y Лемма 7*, (9), (10)

Теорема доказана.


Доказательством Теоремы обратной непротиворечивости мы резко упрощаем проблему выводимости в ПЛ1. Теперь достаточно удостовериться, что некоторая последовательность ППВ из ПЛ1 есть выводимость в ИВ, чтобы удостовериться, что эта же последовательность выражений есть выводимость в ПЛ1.

В ПЛ мы можем доказать следующую теорему.

^ Теорема вседоказуемости. Если х – ППВ, то |х х.

Доказательство. Если х – ППВ, то х построена индуктивно. Рассмотрим здесь базис и индуктивное предположение. Пусть х – константа. 1) х есть 0. Тогда мы можем получить |0 0 из |-1 1, согласно (Е4) и В11. 2) х есть ненулевая константа К. Если К отлична от pi, Pi и 1 и имеет вид Kji, то для этой константы имеем аксиому |Кji Кji (см. (PosKji)). Если К есть pi, Pi или 1, то получаем |К К, согласно (posi), (Рosi) или В11. Далее рассмотрим индуктивное предположение. Пусть |у у, и х есть у. Тогда имеем |у у, согласно (ЕN). Пусть |у у и |z z и х есть уz. Тогда получим |yz yz, согласно (ЕD). Таким образом, получаем, что для для любой ППВ х имеем |х х.


Построением системы ПЛ1 мы одновременно показали, что не вошедшие в нее аксиомы (PP2ij), (PP4i) и (РР4Кji) являются независимыми от аксиом, вошедших в ПЛ1 (аксиомы (PP2ij), (PP4i) и (РР4Кji) ложны при рассмотренной выше интерпретации ПЛ1 в ИВ). То же можно сказать о правиле вывода (EN), не вошедшем в ПЛ1, – принятие его как 1-вывода «Если |-1 х, то |-1 х» делает систему ПЛ1 противоречивой.

Следует также иметь в виду, что ППВ в полярной логике – это не обязательно формулы (имена суждений), но это могут быть и термы – имена понятий. В последнем случае семантика ПЛ не может быть истинностной, но выражает понятия как полярные структуры.


§ 3. Позитивная полярная логика

Рассмотрим далее такую версию ПЛ, как позитивная полярная логика ППЛ. В этой версии используются только регулярные Р-выводимости. В частности, это означает ограничение на использование правила вывода (EN) – оно может использоваться только как Р-вывод. В том числе в ППЛ не может быть доказана Теорема вседоказуемости, но лишь ее аналог:

^ Теорема Р-вседоказуемости. Если х – Р-выражение ПЛ, то |х х.

Доказательство. Если х – Р-выражение, то х построена индуктивно. Рассмотрим здесь базис и индуктивное предположение. Пусть х – Р-константа. 1) х есть ненулевая константа К. Если К отлична от pi, Pi и 1 и имеет вид Kji, то для этой константы имеем аксиому |Кji Кji (см. (PosKji)). Если К есть pi, Pi или 1, то получаем |К К, согласно (posi), (Рosi) или В11. Далее рассмотрим индуктивное предположение. Пусть |у у, и х есть у, причем х и у есть Р-выражения. Тогда имеем |у у, согласно (ЕN) как Р-выводу. Пусть |у у и |z z и y,z есть Р-выражения. Тогда, если х есть уz, то х есть также Р-выражение, и получим |yz yz, согласно (ЕD). Таким образом, получаем, что для для любого Р-выражения х имеем |х х.

Заметим также, что ПЛ1 является частью любой версии ПЛ, в том числе частью ППЛ. Поэтому все теоремы и выводимости ПЛ1 остаются таковыми в любой версии ПЛ, в том числе в ППЛ.

Будем говорить, что система ПЛ Р-непротиворечива е.т.е. в ней не может быть выведена теорема |0 х.


^ Теорема ППЛ-непротиворечивости. ППЛ Р-непротиворечива.

Доказательство. В ППЛ все аксиомы есть Р-аксиомы, и все правила вывода есть регулярные Р-выводы. В то же время выражение |0х не является Р-выражением и, следовательно, не может быть выведено в ППЛ.


Модель системы ППЛ есть булева решетка ВТ истинностных значений, для которой дополнительно верны аксиомы (PP1i), (PP2ij), (PP3), (PP4i) и (РР4Кji). Например, такой решеткой является булева решетка на образующих элементах 1,Т12,
  1   2   3




Похожие:

Основы полярной логики1 iconРаспоряжение Правительства РФ от 29 октября 2009 г. N 1578-р (с изменениями от 8 сентября 2010 г.)
Основы религиозных культур и светской этики, включающего основы православной культуры, основы исламской культуры, основы буддийской...
Основы полярной логики1 iconЧто будут изучать ваши дети? Учебный курс «Основы религиозных культур и светской этики»
Учебный курс «Основы религиозных культур и светской этики» состоит из 6 модулей: основы православной культуры, основы исламской культуры,...
Основы полярной логики1 iconТема Предполагаемое
Территориальные воды, морская миля, длина полярного дня и полярной ночи на разных широтах. Гп СССР
Основы полярной логики1 iconТеоретические основы инженерной геологии
Теоретические основы инженерной геологии. Механико-математические основы/Под ред акад. Е. М. Сергеева.— М.: Недра, 1986. 254 с.,...
Основы полярной логики1 iconТест по теме «Основы логики и логические основы компьютера»
Электронной логической схемы, которая реализует элементарную логическую функцию – это …
Основы полярной логики1 iconИнформация для родителей об особенностях курса «Основы религиозных культур и светской этики» в 2011 – 2012 учебном году Организационно-управленческие основы введения нового комплексного учебного курса «Основы религиозных культур и светской этики»
Организационно-управленческие основы введения нового комплексного учебного курса «Основы религиозных культур и светской этики»
Основы полярной логики1 iconДокументы
1. /21.ОСНОВЫ КОММУНИСТИЧЕСКОЙ ИДЕОЛОГИИ И СОВРЕМЕННОСТЬ (Word)/Введение.doc
2....

Основы полярной логики1 iconИгорь Андреевич Бобров, старший преподаватель Государственной Полярной Академии, Ольга Сергеевна Боброва, ассистент Санкт-Петербургского Университета Экономики
...
Основы полярной логики1 iconУрок №5 Тема урока: Замечательные кривые Цель урока: Познакомиться с полярной системой координат. Научиться стоить с помощью компьютера графики замечательных кривых
Несколько слов о замечательных кривых. Задачи, приводящие к различным замечательным кривым
Основы полярной логики1 iconТема: 14. 08. 06, Пн, 23: 55, Мск
Результаты нового исследования показывают, что в прошлом температура вод Северного Ледовитого океана составляла около 23 градусов...
Разместите кнопку на своём сайте:
Документы


База данных защищена авторским правом ©podelise.ru 2000-2014
При копировании материала обязательно указание активной ссылки открытой для индексации.
обратиться к администрации
Документы

Разработка сайта — Веб студия Адаманов