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

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

При применении правила V_bк формуле Λ(α∕β, γι,..., γ_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 каждая переменная из М ограничивает относительно некоторую переменную из М.

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

Для всякой переменной α, пусть [α] - это множество всех переменных из М, каждую из которых α ограничивает относительно в 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.1 нашего исследования.

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

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

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

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

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

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

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

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

1, r)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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