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

Дадим индуктивное определение истинности формулы φ(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-1j<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. (теорема о замене). Если формула φсигнатуры Σ получается из формулы ψсигнатуры Σ заменой некоторого вхождения подформулы ψ'на формулу φ' сигнатуры Σ и φ'≡ψ', то φ≡ψ.