Перейти к содержимому
Topos Uranos
Русский

Семантическое следование и эквивалентность

Краткое содержание

Этот урок переходит от истинностного значения формулы к отношениям между формулами. Он определяет семантическое следование из множества посылок, конечного или бесконечного, и уточняет прочтения знака следования, включая прочтение его отрицания, которое говорит, что нечто не общезначимо, а не что оно противоречиво. Он использует значения связок, записанные как многочлены, что превращает проверку закона в вычисление, и доказывает структурные свойства следования (рефлексивность, монотонность, сечение и транзитивность), семантическую теорему о дедукции и сведение следования к невыполнимости, на которое будет опираться метод резолюций. Затем он определяет семантическую эквивалентность, доказывает, что она является отношением эквивалентности, совпадающим со взаимным следованием и с общезначимостью эквиваленции, и доказывает индукцией по сложности две теоремы, которые позволяют с ней работать: замену одного вхождения подформулы на другую, эквивалентную ей, и равномерную подстановку формул вместо переменных. С их помощью он составляет каталог законов с их правильными названиями и упрощает формулы цепями эквивалентностей, без таблиц истинности.

Цели обучения

  1. Решать, является ли формула семантическим следствием множества формул, конечного или бесконечного, предъявляя опровергающую оценку или доказывая, что её нет.
  2. Доказывать и применять свойства следования, семантическую теорему о дедукции и сведение следования к невыполнимости.
  3. Устанавливать семантические эквивалентности таблицами истинности, вычислением со значениями и цепями эквивалентностей, правильно называя каждый закон.
  4. Доказывать индукцией по сложности теорему о семантической замене и теорему о равномерной подстановке и различать, когда применяется каждая из них.

Что используется из предыдущего урока

Урок о семантике логики высказываний придал формулам значение, и этот урок считает его известным. Оценка есть функция v ⁣:V→{0,1}v\colon V \to \{0, 1\}, которая сопоставляет каждой переменной истинностное значение, 11 (истина) или 00 (ложь). По теореме об определении по рекурсии на формулах из урока об индукции каждая оценка единственным образом продолжается на все формулы с помощью пункта для стрелки Пирса, единственного, который нужен, поскольку в языке только одна связка:

v((φ↓ψ))=1  ⇔  v(φ)=0,    v(ψ)=0v((\varphi \downarrow \psi)) = 1 \;\Leftrightarrow\; v(\varphi) = 0, \;\; v(\psi) = 0

В силу единственности продолжения v(φ)v(\varphi) пишется и для значения продолжения; буква vv без индекса всегда обозначает оценку (а v′v', ww, uu обозначают другие), тогда как переменные всегда несут свой индекс. Как в уроке о формализации, pp, qq, rr, ss и tt обозначают переменные от v1v_1 до v5v_5, а V(φ)V(\varphi) есть множество переменных формулы φ\varphi. Говорят, что vv выполняет φ\varphi, и пишут v⊨φv \models \varphi, когда v(φ)=1v(\varphi) = 1, и что она её опровергает, v⊭φv \not\models \varphi, когда v(φ)=0v(\varphi) = 0. Формула общезначима (или является тавтологией), и пишут ⊨φ\models \varphi, если её выполняет всякая оценка; выполнима, если её выполняет некоторая оценка; невыполнима (или является противоречием), если её не выполняет ни одна; нейтральна, если она выполнима, не будучи общезначимой. Оценка выполняет множество Γ\Gamma формул, v⊨Γv \models \Gamma, когда выполняет каждую из них, и Γ\Gamma выполнимо, если его выполняет некоторая оценка, и невыполнимо в противном случае. Наконец, ⊤:=(v1→v1)\top := (v_1 \rightarrow v_1) и ⊥:=¬⊤\bot := \neg\top, так что v(⊤)=1v(\top) = 1 и v(⊥)=0v(\bot) = 0 при всякой оценке.

Из того урока используются ещё два результата. Первый есть лемма о совпадении: если две оценки совпадают на переменных формулы φ\varphi, они совпадают на φ\varphi; в силу неё значение формулы с nn переменными зависит лишь от 2n2^{n} комбинаций, и её таблица истинности конечна. Второй есть теорема о значениях производных связок, которая вычисляет по официальным сокращениям значение каждой связки как многочлен от значений компонент. Если a=v(φ)a = v(\varphi) и b=v(ψ)b = v(\psi):

v(¬φ)=1−a,v((φ∨ψ))=a+b−ab,v((φ∧ψ))=abv(\neg\varphi) = 1 - a, \qquad v((\varphi \vee \psi)) = a + b - ab, \qquad v((\varphi \wedge \psi)) = ab
v((φ→ψ))=1−a(1−b),v((φ↔ψ))=ab+(1−a)(1−b),v((φ⊻ψ))=a+b−2abv((\varphi \rightarrow \psi)) = 1 - a(1 - b), \qquad v((\varphi \leftrightarrow \psi)) = ab + (1 - a)(1 - b), \qquad v((\varphi \veebar \psi)) = a + b - 2ab

Доказательства этого урока почти все состоят в сравнении истинностных значений, и эти многочлены позволяют делать его вычислением, а не перебором случаев. Их единственное дополнительное правило состоит в том, что 00 и 11 суть единственные числа, совпадающие со своим квадратом: если xx равно 00 или 11, то x2=xx^{2} = x и x(1−x)=0x(1 - x) = 0. Полезно, кроме того, иметь под рукой три другие записи тех же значений, которые получаются раскрытием произведений:

v((φ↓ψ))=(1−a)(1−b),v((φ∨ψ))=1−(1−a)(1−b),v((φ↔ψ))=1−a−b+2abv((\varphi \downarrow \psi)) = (1 - a)(1 - b), \qquad v((\varphi \vee \psi)) = 1 - (1 - a)(1 - b), \qquad v((\varphi \leftrightarrow \psi)) = 1 - a - b + 2ab

Первая есть пункт для стрелки Пирса (произведение 1−a1 - a и 1−b1 - b равно 11 ровно тогда, когда a=b=0a = b = 0); вторая говорит, что дизъюнкция равна 00, только если обе компоненты равны 00; третья, что эквиваленция равна 11, если a=ba = b (поскольку 1−2a+2a2=11 - 2a + 2a^{2} = 1), и 00, если a≠ba \neq b (поскольку тогда a+b=1a + b = 1 и ab=0ab = 0).