<<
>>

2.2.Семантическая непротиворечивость системы BMV

Определение 2.2.1.Переменная α называется активной (пассивной) в BMV- выводе, если α абсолютно ограничена в этом выводе и (не) существует абсолютно ограниченная в этом выводе переменная β, которую относительно ограничивает переменная α.

При применении правила Vbк формуле Λ(α∕β, γι,..., γn) выводится формула VαΛ(α), переменная β становится абсолютно ограниченной и β относительно ограничивает все переменные из γι,..., γn.

При применении правила Зи к формуле 3αΛ(α) выводится формула Λ(α∕β, γι,..., γn), переменная β становится абсолютно ограниченной и β относительно ограничивает все переменные из γι,..., γn.

Построим следующий завершенный вывод 3xVyA(x, y) |- 3xVzA(x, z).

В этом выводе переменная x пассивна и переменная у активна, поскольку абсолютно ограниченная переменная y относительно ограничивает другую абсолютно ограниченную переменную x на шаге 4.

Лемма 2.2.2.В произвольном BMV-выводе D с непустым множеством М всех абсолютно ограниченных переменных в D найдется переменная α: α ∈М и α не

2 ограничивает относительно в D ни одну переменную из М.

Доказательство: от противного.

Допустим, что в D каждая переменная из М ограничивает относительно некоторую переменную из М.

2Техникой доказательства этой леммы мы обязаны В.М. Попову.

Для всякой переменной α, пусть [α] - это множество всех переменных из М, каждую из которых α ограничивает относительно в D, и пусть для всякого непустого множества X переменных (X)minесть переменная из X, которая нестрого предшествует в алфавитном порядке переменных любой переменной из X.

Поскольку произвольный BMV-вывод конечен (определение 2.1.3), найдется такое натуральное число n: М есть n-элементное множество. Пусть для определенности ∏o есть натуральное число и М есть no-элементное множество.

Доказано.

Лемма 2.2.2 доказана для произвольного BMV-вывода. Поскольку всякий завершенный BMV-вывод есть BMV-вывод, лемма 2.2.2 верна для произвольного завершенного BMV-вывода с непустым множеством абсолютных переменных.

По определению вывода в системе BMV, вывод - это непустая конечная последовательность формул, каждая из которых является либо посылкой, либо получена из предыдущих формул по одному из правил вывода системы BMV.

3Подробный логический анализ данного отношения проводится в параграфе 3.1 нашего исследования.

Таким образом, важным параметром любого завершенного вывода является число применений в нем правил вывода. Будем обозначать это число посредством q. Из определения вывода следует, что q ≥ 0.

Специфическим свойством вывода в данном исчислении является наличие в выводе (возможно, пустого) множества абсолютно ограниченных переменных. Будем называть рангом вывода число абсолютно ограниченных переменных данного вывода и обозначать ранг вывода посредством г. Из определения вывода следует, что r ≥ 0.

Пусть Г - произвольное непустое множество формул языка логики предикатов, тогда из Г логически следует формула В (обозначается записью «Г |= В»), если и только если не существует модели и приписывания значений предметным переменным, при которых каждая формула из Г принимает значение «истина», а формула В - значение «ложь».

Лемма 2.2.3.В произвольном завершенном выводе, число применений правил вывода в котором есть q и ранг которого есть r, последняя формула этого вывода семантически следует из множества всех неисключенных в этом выводе посылок.

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

Данная лемма будет доказана методом двойной математической индукции по числу применений правил вывода и по рангу произвольного завершенного вывода.

В обосновании данного метода мы следуем [Смирнов, с. 122-123].

Запишем сокращенно данную лемму в виде VqVrΠ(q, г).

Для доказательства этой леммы достаточно доказать три утверждения:

1, r)

Поэтому доказательство леммы сводится к доказательству утверждений (А), (Б) и (С).

(А) Л(0, 0): лемма верна для всех завершенных выводов, ранг и число применений правил вывода в которых равны 0.

Пусть последовательность формул С1, C2,., Сі (t ≥ 1) есть завершенный вывод, ранг и число применений правил вывода в котором равны 0. Для доказательства Л(0, 0) достаточно показать, что формула Gtсемантически следует из множества всех неисключенных посылок в выводе С1, C2,., Q.

По определению семантического следования, получаем, что {С1, C2,., Сі) |= С Но множество {С1, C2,., С1) есть множество всех неисключенных посылок в выводе С1, C2,., Сі. Поэтому Сі семантически следует из множества всех неисключенных посылок в выводе С1, C2,., С1.

Таким образом, имеет место Л(0, 0).

(Б) лемма верна для всех завершенных выводов, ранг которых равен 0 и число применений правил вывода в которых равно n+1, в предположении, что лемма верна для всех завершенных выводов любого ранга, число применений правил вывода в которых меньше или равно n.

Ранг вывода равен 0, значит, в выводе не применялись правила Vb,3и.

верна для всех завершенных выводов, ранг которых меньше или равен r и число применений правил вывода в которых равно n.

Т.е. докажем VrΛ(n, r+1) в предположении, что Vr1(r1 ≤ r ⊃Л(п, rι)).

Пусть имеется завершенный вывод Д с п+1 количеством абсолютно ограниченных переменных и {α1, α2, ..., αn+1} - множество (n ≥ 1) абсолютно ограниченных переменных в этом выводе.

По лемме 2.2.2, среди {α1, α2, ..., αn+1} найдется пассивная переменная αi, 1 ≤ i ≤ п+1. Если в Д несколько пассивных переменных, то мы выбираем первую (сверху вниз) из них.

Тогда (С) разбивается на 2 случая:

С1. Пассивная переменная αiабсолютно ограничена по правилу Vb.

С2. Пассивная переменная αiабсолютно ограничена по правилу Зи.

Тогда вывод Д может принять один из двух видов:

Построим следующий вывод Д*, который будет отличаться от предыдущего только наличием посылки 0 вида К ⊃М, где К - формула, находящаяся на шаге h в выводе Д, и М - формула, находящаяся на шаге k в выводе Д.

Тогда вывод Д* может принять один из двух видов:

<< | >>
Источник: ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004. 2004

Еще по теме 2.2.Семантическая непротиворечивость системы BMV:

  1. Цели, основные понятия и композиция исследования
  2. Введение
  3. 3.3. Онтологические предпосылки самопознания.
  4. Физиология
  5. Пребывание — исхождение — возвращение (μονή ~~ πρόοδος* — Επιστροφή).
  6. Воля господина в трактовке Гегеля
  7. Виды возвращения.
  8. ЗАКЛЮЧЕНИЕ
  9. Учение о красоте и триада благо-мудрость-красота.
  10. Терминологические и методологические проблемы
  11. Психоанализ
  12. ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004, 2004
  13. 2.2. Исторические свидетельства о трактате «О природе космоса и души»
  14. 3.4.1. Учение о душе и видах душ.
  15. Гармоника в контексте мыслительного феномена прото­упорядочивания
  16. Научные исследования в перспективе вопроса о сущности воли
  17. Ответы к экзамену по логике,