4.Cимантика исчисление высказываний.Непротиворичивость ив.Таблицы истиности.Общезначимые и выполнимые формулы.Теорема о полноте.РазрешимостьИв.

Х- некоторое множество f_x:(A_i)=YX

f_x(φ¬Ψ)=f_x(φ)∩f(Ψ)’

f_x(φ Ψ)=f_x(φ)٧f_x(Ψ)

f_x(¬φ)=X | f_x(φ)

X

f_x(A_j)

f_x(A_i)

f_x(φ→Ψ)=f_x(¬φ)٧f_x(Ψ)

f_x – интерпритация ИВ в Х

Теорема: Для любой интерпритации f_x сиквенция φ₁, φ_n+ φ доказуема 

f_x(φ₁)∩f_x(φ₂)∩…∩f_x(φ_n)f_x(φ)

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

φ├φ

f_x(φ) f_x(φ)

1-12 правила

6) Г_i φ├φ_i; Г_iX├φ_i Г├φ٧X

Г├Ψ

Г=φ₁…φ_n

∩_i f_x(φ₁)∩ f_x(φ) f_x(φ)

∩_i f_x(φ₁)∩ f_x(φ) f_x(Ψ) => ∩_i f_x(φ₁)f_x(Ψ)

∩_i f_x(φ₁)f_x(φ) ٧ f_x(X)

следствие ├φ док-ма  f_x=X

φ٧¬φ док-ма f_x(φ) ٧ f(x(φ)=X

Cледствие ИВ непротиворичиво

Док-ва: X≠0, f_x , φ=A ^ ¬A сиквенция ├ φ не доказуема:

f_x(φ)= f_x(A)= f_x(A)∩ f_x(A)=0≠X

главная интерпритация :X={0}

f_x(A)=0 A B A^B A٧B A→B ¬A

={0}=1 0 0 0 0 1 1

0 1 0 1 1 1

1 0 0 1 0 0

1 1 1 1 1 0

f_x:{A₁,…,A_n}→{0,1}

φ(A₁,…,A_n)

f_x(φ)є{0,1}

(δ₁,…,δ_n)є{0,1}^h φ(δ₁,δ₂,…,δ_n)є{0,1}

װ

f_x(δ₁,…,δ_n) f_φ-истеная функция формулы φ

Формула φ называется тождественно истенной,если f_φΞ1

Формула φ называется тождественно истенной, если f_φΞ 0

Формула φ называется выполнимой ,если f_φ(δ₁,…,δ_n)=1

f_φ(δ₁,…,δ_n)=0 для некоторых δ₁,…,δ_n

теорема о полноте ИВ

Для любой ф-лы φ ИВ секвенция ├φ доказуема╞φ

├φ ٧¬φ f_φ ٧¬φ Ξ1

Следствие: ИВ разрешимо,т.е существует единый алгоритм проверки доказуема или нет,для каждой формулы опредиляется несколько классов.

φ₁,…, φ_n├φ доказуема├φ где φ=φ₁→( φ₂→…( φ_n→Ψ)…)

доказуема Ψ= φ₁^…^ φ_n→φ  f _Ψ Ξ1

Множество формул Г называется противоречием,если Г├ доказуема

5.Семантическое дерево. Алгоритм Квайна и алгоритм редукции проверки общезначимости формул.

Семантическое дерево: бинарное корневое дерево, в котором:

1. Каждое ребро помечено некоторой литерой А_i. 2)Литеры,выходящие из одной вершины, контрарны(A_i , ¬A_i ).

2. Ребра соответствующие переменной A_i  они находятся на одинаковых расстояниях от корня φ.

A₁ ¬ A₁

A₂ ¬ A₂ A₂ ¬ A₂

A₃ ¬ A₃

Алгоритм Квайна.

φ(A,B,C)=(((A^B)->C)^(A->B))->(A->C) , |= φ ?

f(A)=1 (((1^B)->C)^(1->B))->(1->C), ((B->C)^B)->C, f(B)=1 (1->C)^1)->C C->C –тожд. ист.

f(A)=0 (((0^B)->C)^(0->B))->(0->C), 1^1->1–тожд. ист.; f(B)=0 ((0->C)^0)->C ->C –тожд. ист.

Алгоритм Редукции.

Используется при небольшом количестве импликаций. ╞ ((A^B)->C) ->(A->(B->C)) ? Предположим противное, т.е. не ╞ ; f((A^B)->C)=1 , f(A->(B->C))=0; f(A)=1, f(B->C)=0, f(B)=1, f(C)=0.

f φ(A,B,C)=0 возможно только при условии, что (А,В,С)=(1,1,0); f ((A^B)->C)=1^1->0=0≠1 противоречие.