Истинность формулы ЛП в алгебраической системе.

 

Дадим индуктивное определение истинности формулы φ(x₁,…,x_n) сигнатуры Σ на элементах a₁,…,a_n А в алгебраической системе = .

Запись ╞φ(a₁,…,a_n) будет означать, что формула φистинна на элементах a₁,…,a_n А в системе .

1) ╞t₁(a₁,…,a_n)=t₂(a₁,…,a_n), где t₁,t₂ T(Σ), значения термов t₁,t₂ в системе Ã на элементах a₁,…,a_n А совпадают;

2) ╞P(t₁(a₁,…,a_n),….,t_k(a₁,…,a_n)), где P^(k) Σ,t₁,…,t_k T(Σ),↔(t₁(a₁,…,a_n),…, t_k(a₁,…,a_n)) P;

3) ╞ψ(a₁,…,a_n)∧χ(a₁,…,a_n) ╞ψ(a₁,…,a_n) и ╞χ(a₁,…,a_n);

4) ╞ψ(a₁,…,a_n)∨χ(a₁,…,a_n) ╞ψ(a₁,…,a_n) или ╞χ(a₁,…,a_n);

5) ╞ ψ(a₁,…,a_n) → χ(a₁,…,a_n) если ╞ ψ(a₁,…,a_n), то ╞ χ(a₁,…,a_n);

6) ╞ψ(a₁,…,a_n) неверно, что ╞ψ(a₁,…,a_n);

7) ╞ xψ(x,a₁,…,a_n) ╞ψ(a,a₁,…,a_n) длялюбого а A;

8) ╞ xψ(x,a₁,…,a_n) ╞ψ(a,a₁,…,a_n) для некоторого а А.

Если не выполняется ╞φ(a₁,…,a_n), то будем говорить, что формула φ(a₁,…,a_n)ложна в системе .

Пример 1.

Записать формулу φ(x), истинную в тогда и только тогда, когда х четно.

Решение.

φ(x)= y(x=y+y).

Пример 2.

Записать формулу φ'(x,y,z), истинную в тогда и только тогда, когда z‑ наименьшее общее кратное чисел х и y.

Решение.

φ'(x,y,z)=ψ(x,y,z)∧χ(x,y,z), где формула ψ «говорит» о том, что z делится на x и на y, а формула χ "говорит"о том, что z делит все общие кратные х и у, т. е. является наименьшим из всех общих кратных:

ψ= u,∨(z=u∙x∧z=∨х∙y),

χ= w( u,∨(w=u∙x∧w=∨х∙y)→ w₁(w=w₁∙z)). Итак,

φ'(х,у,z)= u,∨(z=u∙x∧z=х∙y)∧ w( u,∨(w=ux∧w=хy)→ w₁(w=w₁z)).

 

Логическое следствие в ЛП

 

Через обозначим кортеж переменных ; через ‑ .

Определение. Пусть φ₁(),…,φ_n(), ψ() – формулы сигнатуры ∑. Формула ψ называется логическим следствием формул φ₁,…,φ_n (обозначается φ₁,…,φ_n╞ ψ), если для любой алгебраической системы сигнатуры ∑

╞ (φ₁() … φ_n()→ψ()).

Пример 1.

Доказать, что φ₁()→φ₂(),φ₂()→φ₃()╞φ₁()→φ₃() (1)

где φ₁(),φ₂(),φ₃() – формулы сигнатуры ∑.

Пусть =‹А, ∑› ‑ произвольная система сигнатуры ∑. Необходимо указать, что ╞ ((φ₁()→φ₂()) ((φ₂()→φ₃())→(φ₁()→φ₃())).

Пусть и ╞ ((φ₁()→φ₂()) ((φ₂()→φ₃()).

Покажем, что ╞(φ₁()→φ₃() (2)

Предположим, что ╞φ₁(). Так как ╞(φ₁()→φ₂(), то ╞φ₂().

Так как ╞φ₂()→φ₃(), то ╞φ₃().

Таким образом (2), а, следовательно, и (1), доказано.

Исчисление предикатов

Зафиксируем некоторую произвольную сигнатуру Σ и определим исчисление предикатов сигнатуры Σ (ИП^Σ).

Формулами ИП^Σ будут формулы сигнатуры Σ.

Примем следующие соглашения. Пусть x₁,…,x_n ‑ переменные, t₁,…,t_n ‑ термы сигнатуры Σ и φ ‑ формула сигнатуры Σ. Запись будет обозначать результат подстановки термов t₁,…,t_n вместо всех свободных вхождений в φ переменных x₁,…,x_n соответственно, причем, если в тексте встречается запись , то предполагается, что для всех i={1,...,n} ни одно свободное вхождение в φ переменной x_i не входит в подформулу φвида y или y , где у - переменная, входящая в t_i.

Аксиомами ИП^Σ являются аксиомы вида 1-10 ИВ, а также аксиомы

11) xφ→(φ)_t^x;

12) (φ)_t^x→ xφ;

13) x=x;

14) x=y→((φ)_x^z→(φ)_y^z).

Формулы 1-14 называются схемами аксиом ИП^Σ.

Правила вывода ИП^Σ:

1. φ, φ → ψ,

ψ

2. ψ →φ,

ψ→ xφ

3. φ → ψ,

xφ → ψ

где в правилах 2 и 3 переменная x не входит свободно в ψ.

Доказательством в ИП^Σ формулы φ называется такая последовательность φ₀,…,φ_n формул ИП^Σ, что φ_n φ и для каждого i≤n формула φ_i удовлетворяет одному из следующих условий:

1) φ_i ‑аксиома ИП^Σ;

2) φ_i получается из некоторых φ₁,…, φ_i-1, по одному из правил вывода 1-3.

Если существует доказательство в ИП^Σ формулы φ, то φ называется доказуемой в ИП^Σ или теоремой ИП^Σ (обозначаем ├φ).

Выводом в ИП^Σформулы φ из множества формул φ₁,…, φ_m называется такая последовательность ψ₁,…,ψ_k формул ИП^Σ, что φ_n φ и для каждого i≤n формула φ_i удовлетворяет одному из следующих условий:

1) φ_i ‑аксиома ИП^Σ;

2) φ_i принадлежит Г;

3) φ_i получается из некоторых ψ₁,…, ψ_i-1 j<i, по одному из правил вывода 1-3, причем при применении правил 2 и 3 переменная х не должна входить ни в одну формулу из Г свободно.

Если существует вывод в ИП^Σ формулы φ из множества формул φ₁,…, φ_n, то φ называется выводимой в ИП^Σ из Г (обозначаем Г├φ). При этом Г называется множеством гипотез. Очевидно, что доказуемость формулы эквивалентна ее выводимости из пустого множества гипотез. Так же, как в исчислении высказываний, определяется понятие квазивывода. Если Г = {ψ₁,…,ψ_n}, то вместо Г├φ пишем ψ₁,…,ψ_n├φ.

Формула ψ сигнатуры Σ называется тавтологией, если она получается из формулы φ исчисления высказываний, доказуемой в исчислении высказываний, путем замены всех ее пропозициональных переменных x₁,…,x_n на формулы ψ₁,…,ψ_n сигнатуры Σ соответственно. Формулу φ при этом называют основой тавтологии.

Утверждение 1. Любая тавтология φ сигнатуры Σ доказуема в ИП^Σ.

Следствие 1. Если φ и ψ ‑ пропозиционально эквивалентные формулы сигнатуры Σ, то φ и ψ‑ эквивалентные формулы сигнатуры Σ.

 

В исчислении предикатов ИП^Σ справедлива теорема о дедукции.

Теорема 1. (о дедукции).Пусть Г – множество формул ИП^Σ, φ, ψ – формулы ИП^Σ. Тогда Г,φ├ψ, Г├φ→ψ.

Эквивалентные формулыИП

Определение эквивалентных формул, утверждения 3,4 при замене формул φ, ψ, χ ИВ на формулы ИП^Σ имеют место.

Утверждение 1. В ИП^Σ выполнимы все эквивалентности ИВ из теоремы 5.

Доказательство. Выполнимость в ИП^Σ всех эквивалентностей исчисления высказываний следует из следствия 3.

Утверждение 2. В ИП^Σ выполнимы следующие эквивалентности, в которых предполагается, что переменная ж не входит свободно в формулу ψ, а переменная у не входит в формулу φ:

1) xφ≡ xφ,1^\) xφ≡ xφ,

2) x(φ∧ψ)≡ xφ∧ψ, 2^\) x(φ∨ψ)≡ xφ∨ψ

3) x(φ∧ψ)≡ xφ∧ψ, 3^\) x(φ∨ψ)≡ xφ∨ψ,

4) xφ≡ . 4^\) xφ≡

Пример. 1. Докажем эквивалентность а). Построим квазивывод формулы xφ→ xφ из Ø:

1. φ→ xφ ‑ аксиома 12;

2. xφ→φ ‑ к п.1 применили утверждение 3:

3. xφ→ xφ ‑ к п.2 применили правило вывода 2.
Построим квазивывод формулы xφ→ xφ из Ø:

1. xφ→φ ‑ аксиома 11;

2. φ→ xφ ‑ к п.1 применили утверждение 3;

3. xφ→ xφ ‑ к п. 2 применили правило вывода 3;

4. xφ→ xφ ‑ к п.З применили утверждение 3.

Пример. 2. Докажем эквивалентность г). Построим квазивывод формулы x(φ∧ψ)→ xφ∧ψ из Ø:

1. x(φ∧ψ)→φ∧ψ ‑ аксиома 11;

2. φ∧ψ→φ ‑ утверждение 1;

3. x(φ∧ψ)→φ ‑ к пп.1,2 применили утверждение 1;

4. x(φ∧ψ)→ xφ ‑ к п.4 применили правило вывода 2;

5. φ∧ψ→ψ ‑ утверждение 1;

6. x(φ∧ψ)→ψ ‑ к пп.1,5 применили утверждение 1;

7. ( x(φ∧ψ)→ xφ)→(( x(φ∧ψ)→ψ)→( x(φ∧ψ)→ xφ∧ψ)) ‑ аксиома 5;

8. x(φ∧ψ)→ xφ∧ψ ‑ к пп.4.6.7 применили правило вывода 1.

Построим квазивывод формулы xφ∧ψ → x (φ∧ψ) из Ø:

1. xφ∧ψ→ xφ ‑ аксиома 3;

2. xφ→φ‑ аксиома 11;

3. xφ∧ψ→φ ‑ к пп.1,2 применили утверждение 1;

4. xφ∧ψ→ψ‑ аксиома 4;

5. ( xφ∧ψ→φ)→(( xφ∧ψ→ψ)→( xφ∧ψ→φ∧ψ)) ‑ аксиома 5;

6. xφ∧ψ→φ∧ψ ‑ к пп.3,4,5 применили правило вывода 1;

7. xφ∧ψ→ x(φ∧ψ)‑ к п.6 применили правило вывода 2.

Теорема 1. (теорема о замене). Если формула φ сигнатуры Σ получается из формулы ψ сигнатуры Σ заменой некоторого вхождения подформулы ψ' на формулу φ' сигнатуры Σ и φ'≡ψ', то φ≡ψ.