MALOG 2014, Axiomatika vyrokov
´
e´ logiky
´
Anton´ın Dvoˇrak
http://berta.osu.cz/dvorak2/malog/
Ostrava, 11. 4. 2014
Axiomatika vyrokov
´
e´ logiky
Redukce jazyka
´
Axiomy / schemata
axiomu
Odvozovac´ı pravidlo
Dukazy,
dukazy
z pˇredpokladu˚
˚
˚
ˇ o dedukci
Veta
ˇ o uplnosti
Veta
´
Redukce jazyka
Chceme-li usporn
eˇ volit axiomy, je v´yhodne´ redukovat poˇcet
´
´
spojek na spojky zakladn´
ı, v naˇsem pˇr´ıpadeˇ na negaci a
implikaci ¬, ⇒. Potom
A∨B
A&B
A⇔B
je zkratka za formuli
je zkratka za formuli
je zkratka za formuli
(¬A ⇒ B),
¬(A ⇒ ¬B),
(A ⇒ B) & (B ⇒ A).
´
Jsou moˇzne´ i jine´ kombinace zakladn´
ıch spojek.
Axiomy vyrokov
´
e´ logiky - Hilbertovsky´ kalkul
´
Jsou-li A, B, C formule, pak kaˇzda´ formule nasleduj´
ıch tvaru˚ je
axiom:
(A1) A ⇒ (B ⇒ A)
(A2) A ⇒ (B ⇒ C) ⇒ [(A ⇒ B) ⇒ (A ⇒ C)]
(A3) (¬B ⇒ ¬A) ⇒ (A ⇒ B)
Axiomy vyrokov
´
e´ logiky
Protoˇze pro kaˇzdou volbu formul´ı A, B, C vznikne jedna
´
instance v´yrazu (A1), (A2), (A3), tedy nov´y axiom, ˇr´ıkame,
zˇ e (A1), (A2), (A3) jsou schemata axiomu.
˚
Z jazyka v´yrokove´ logiky lze vytvoˇrit nekonecneˇ mnoho
formul´ı, kaˇzde´ schema generuje nekonecneˇ mnoho
axiomu.
˚
´ ı system
´ v´yrokove´ logiky ma´ tedy tˇri schemata
Formaln´
axiomu˚ a z nich odvozeno mnoho axiomu.
˚
ˇ ych spoˇcetna,
´ je
Je-li mnoˇzina v´yrokov´ych promenn´
spoˇcetna´ mnoˇzina vˇsech formul´ı a mnoˇzina vˇsech axiomu.
˚
Je-li napˇr. P = {p, q, r , s}, pak napˇr.
p ⇒ (q ⇒ p), (r ∨ s) ⇒ ((p&q) ⇒ (r ∨ s))
jsou axiomy.
Odvozovac´ı pravidlo
Z formul´ı A a A ⇒ B odvodˇ formuli B.
A, A ⇒ B
B
Toto odvozovac´ı pravidlo se naz´yva´ modus ponens.
Dukaz,
˚
dokazatelnost
ˇ ıkame,
´
Nechˇt A je formule. R´
zˇ e koneˇcna´ posloupnost formul´ı
A1 , A2 , . . . , An je dukazem
formule A,
˚
(a) je-li An formule A,
(b) Jestliˇze pro kaˇzde´ i, 1 ≤ i ≤ n, je formule Ai budˇ axiom,
nebo je odvozena z pˇredchoz´ıch formul´ı v dukazu
˚
Aj , 1 ≤ j < i pravidlem modus ponens.
´
Existuje-li dukaz
formule A, ˇr´ıkame,
zˇ e A je
˚
ˇ
dokazatelna´ ve v´yrokove´ logice, nebo, zˇ e A je vetou
v´yrokove´ logiky a p´ısˇ eme ` A.
Pˇr´ıklad
Dokaˇzme formuli
A ⇒ A.
(1)
Sestroj´ıme posloupnost formul´ı, ktera´ bude dukazem
formule
˚
(1).
1.
2.
3.
4.
5.
A ⇒ ((A ⇒ A) ⇒ A)
(A ⇒ ((A ⇒ A) ⇒ A)) ⇒ [(A ⇒ (A ⇒ A)) ⇒ (A ⇒ A)]
(A ⇒ (A ⇒ A)) ⇒ (A ⇒ A)
A ⇒ (A ⇒ A)
A⇒A
instance (A1)
instance (A2)
MP 1. a 2.
instance (A1)
MP 4. a 3.
Dukaz
˚
z pˇredpokladu˚
Nechˇt T je mnoˇzina formul´ı, A je formule.
ˇ ıkame,
´
R´
zˇ e posloupnost formul´ı
A1 , A2 , . . . , An
je dukaz
formule A z mnoˇziny pˇredpokladu˚ T , jestliˇze
˚
(a) An je formule A,
(b) pro kaˇzde´ i, 1 ≤ i ≤ n, je formule Ai axiom nebo prvek T ,
nebo je odvozena z pˇredchoz´ıch formul´ı v dukazu
˚
Aj , 1 ≤ j < i pravidlem modus ponens.
´
Existuje-li dukaz
formule A z pˇredpokladu˚ T , ˇr´ıkame,
˚
zˇ e A je dokazatelna´ z T , a p´ısˇ eme T ` A.
Korektnost MP
Pravidlo modus ponens je korektn´ı.
ˇ em
´ ohodnocen´ı v formule A a A ⇒ B pravdive,
´
Jsou-li pˇri nejak
tj. v¯ (A) = v¯ (A ⇒ B) = 1, potom je pravdiva´ i formule B, tj.
´ e,
ˇ jsou-li A a A ⇒ B tautologie, je B take´
v¯ (B) = 1. Specialn
tautologie.
Hilbertovske´ kalkuly
´
´ odvozovac´ıch pravidel,
V´yhody: Jednoduch´y zapis,
malo
´ schemat axiomu˚ (ale axiomu˚ jako takov´ych hodne!)
ˇ
malo
´ ı vlastnost´ı cele´ logiky.
Dobre´ pro ukazovan´
Jednoduchou modifikac´ı se dostaneme do jine´ logiky.
´ ı konkretn´
´ ı
Nev´yhody: Velmi nev´yhodne´ pro dokazovan´
´
´ nedav
´ a´
formule A — formule, kterou chceme dokazat,
nam
´ y navod,
´
zˇ adn´
jak postupovat.
Alternativy: Pˇrirozena´ dedukce, sekventov´y poˇcet,
analyticka´ tabla.
ˇ o dedukci
Veta
Nechˇt T je mnoˇzina formul´ı a nechˇt A, B jsou formule, potom:
´ eˇ kdyˇz T ∪ {A} ` B.
T ` A ⇒ B prav
M´ısto T ∪ {A} na prave´ straneˇ p´ısˇ eme T , A. Prava´ strana
ekvivalence odpov´ıda´ tomu, jak se obvykle implikace
dokazuj´ı.
ˇ o dedukci je vetou
ˇ
Veta
o existenci dukazu.
Existuje-li
˚
dukaz
tvrzen´ı na leve´ straneˇ ekvivalence, pak take´ existuje
˚
ˇ a naopak.
dukaz
tvrzen´ı na prave´ strane,
˚
ˇ o dedukci
Dukaz
˚
vety
(a) Nechˇt T ` A ⇒ B a nechˇt A1 , A2 , . . . , An , A ⇒ B je dukaz
˚
A ⇒ B z pˇredpokladu˚ T . Potom A1 , A2 , . . . , An , A, A ⇒ B, B
je dukaz
B z pˇredpokladu˚ T , A.
˚
(b) Nechˇt T ∪ {A} ` B a nechˇt A := A0 , A1 , A2 , . . . , An je dukaz
˚
B z pˇredpokladu˚ T , A. Omezenou indukc´ı pro 0 ≤ j < n
´ zeme T ` A ⇒ Aj . T´ım pro j = n bude dukaz
dokaˇ
hotov.
˚
ˇ o dedukci
Dukaz
˚
vety
Rozliˇs´ıme cˇ tyˇri pˇr´ıpady:
(b1) j = 0, potom ` A ⇒ A0 plyne z ` A ⇒ A.
(b2) Aj je axiom v´yrokove´ logiky, potom Aj ⇒ (A ⇒ Aj ) je
instanc´ı schematu (A1) a A ⇒ Aj odvod´ıme pomoc´ı
pravidla modus ponens.
ˇ
(b3) Aj je pˇredpoklad z T . Postupujeme stejne.
(b4) Aj je odvozena z formul´ı Ai , Ak , i, k < j. Bez ujmy
na
´
´
obecnosti muˇ
zˇ e Ai je tvaru Ak ⇒ Aj .
˚ zeme pˇredpokladat,
ˇ o dedukci
Dukaz
˚
vety
Podle indukˇcn´ıho pˇredpokladu:
T ` A ⇒ Ak
T ` A ⇒ (Ak ⇒ Aj )
| {z }
(2)
Ai
Ze schematu (A2) plyne
T ` (A ⇒ (Ak ⇒ Aj )) ⇒ [(A ⇒ Ak ) ⇒ (A ⇒ Aj )].
| {z }
Ai
Odkud dvoj´ım pouˇzit´ım pravidla modus ponens a pˇredpokladu
´ ame
´
(2) dostav
T ` A ⇒ Aj .
ˇ dokaz
´ ana.
´
Pro j = n je veta
ˇ o dedukci – pˇr´ıklad pouˇzit´ı
Veta
` (A ⇒ (B ⇒ C)) ⇒ (B ⇒ (A ⇒ C))
(3)
ˇ o dedukci (VD):
Podle vety
A ⇒ (B ⇒ C) ` B ⇒ (A ⇒ C)
A ⇒ (B ⇒ C), B ` A ⇒ C
A ⇒ (B ⇒ C), B, A ` C
Podle MP:
A, A ⇒ (B ⇒ C)
B⇒C
B, B ⇒ C
.
C
ˇ (3) dokaz
´ ana
´
T´ım je veta
- na poˇrad´ı antecedentu˚ v implikaci
´ z´ı.
nezaleˇ
ˇ ı pˇr´ıklad
Dals´
` ¬A ⇒ (A ⇒ B)
Dukaz:
˚
1.
2.
3.
4.
5.
` ¬A ⇒ (¬B ⇒ ¬A)
¬A ` ¬B ⇒ ¬A
` (¬B ⇒ ¬A) ⇒ (A ⇒ B)
¬A ` (A ⇒ B)
` ¬A ⇒ (A ⇒ B)
schema (A1)
VD
schema (A3)
2., 3., MP
VD
(4)
Duleˇ
˚ zite´ dokazatelne´ formule
ˇ
Veta
`A ⇒ A
`[A ⇒ (B ⇒ C)] ⇒ [B ⇒ (A ⇒ C)]
`A ⇒ ¬¬A, ` ¬¬¬A ⇒ ¬A, ` ¬¬A ⇒ A
(5)
`(A ⇒ B) ⇔ (¬B ⇒ ¬A)
(6)
`(A ⇒ B) ⇔ (¬¬A ⇒ ¬¬B)
(7)
`(¬A ⇒ A) ⇒ A
(8)
`(B ⇒ A) ⇒ [(¬B ⇒ A) ⇒ A]
(9)
`A ⇒ (¬B ⇒ ¬(A ⇒ B))
(10)
´ ı formuli
O neutraln´
Tvrzen´ı
Nechtˇ T je mnoˇzina formul´ı a A, B jsou formule.
Jestliˇze T , A ` B a T , ¬A ` B potom T ` B.
Proof.
Plyne z VD a aplikujeme MP na (8).
O dukazu
˚
z atomickych
´
komponent
Znaˇcen´ı: Nechˇt v je pravdivostn´
ı ohodnocen´ı (valuace) a B je
B,
pokud
v¯ (B) = 1;
lib. formule. Potom B v
¬B, jinak.
Tvrzen´ı
Nechtˇ v je valuace a P1 , . . . , Pn jsou vˇsechny atomicke´
komponenty formule A. Potom
P1v , . . . , Pnv ` Av .
Proof.
Indukc´ı podle sloˇzitosti A.
(a) A ∈ P tedy je jednou z Pi a Piv ` Piv .
(b) A je tvaru ¬B: 1) v¯ (B) = 0 2) v¯ (B) = 1
(11)
Proof.
(c) A je tvaru B ⇒ C:
1) v¯ (B) = 1 a v¯ (C) = 1.Potom v¯ (B ⇒ C) = 1. Z (A1) a VD
dostaneme C ` B ⇒ C. C je C v a je dokazatelne´ z
´ ano.
´
pˇredpokladu˚ (11). Protoˇze Av je B ⇒ C, je tvrzen´ı dokaz
2) v¯ (B) = 1 a v¯ (C) = 0. Potom v¯ (B ⇒ C) = 0.
Z (10) ` B ⇒ (¬C ⇒ ¬(B ⇒ C)) pak |{z}
B v , |{z}
C v ` ¬(B ⇒ C).
B
3) v¯ (B) = 0. Podle (4) a VD
¬B ` B ⇒ C.
Nyn´ı ¬B je B v a B ⇒ C je Av .
¬C
ˇ o uplnosti
Slaba´ forma vety
´
(Emil Post, 1920)
ˇ
Veta
Nechtˇ A je formule. Potom plat´ı:
´ eˇ kdyˇz |= A.
` A prav
Proof.
ˇ rit, zˇ e vˇsechny axiomy jsou tautologie a MP je korektn´ı.
”→” Oveˇ
”←” Nechtˇ |= A a P1 , . . . , Pn jsou vˇsechny jej´ı atomicke´
komponenty. Zvol´ıme lib. valuaci w a v´ıme, zˇ e P1w , . . . , Pnw ` A.
Nechtˇ v je totoˇzna´ s w aˇz na to, zˇ e Pn pˇriˇrazuje opaˇcnou
v ,P ` A
P v , . . . , Pn−1
n
v
v
hodnotu, potom v1
v , ¬P ` A tedy P1 , . . . , Pn−1 ` A.
P1 , . . . , Pn−1
n
´
Postup opakujeme n-1 krat.
ˇ o uplnosti
Silna´ forma vety
´
ˇ
Veta
Pro libovolnou mnoˇzinu formul´ı T a formuli A:
T `A
´ eˇ kdyˇz
prav
T |= A.
Proof.
”→” Z korektnosti MP.
”←” T |= A potom existuje koneˇcna´
´ eˇ kdyˇz
T0 = {A1 , A2 , . . . , An } ⊆ T : T0 |= A (kompaktnost) prav
´ eˇ kdyˇz ` B (slaba´ veta
ˇ o uplnosti)
|= A1 ⇒ (. . . (An ⇒ A)) prav
´
|
{z
}
B
´ eˇ kdyˇz T ` A
prav
(VD).
Download

MALOG 2014, Axiomatika výrokové logiky