VL
je-li fle A pravdivá při ohodnocení v, pak v |= A (v je model A).,
tautologie: pravdivá vždy: |= A. tautologický důsledek: T |= A.
axiomy VL:
A1: ( A → ( B → A )) (triviální)
A2: ( A → ( B → C )) → ((A → B ) → (A → C )) (roznásobení)
A3: (¬ B → ¬ A) → (A→ B) (obrácení implikace)
odv. pravidlo - modus ponens: A, A → B |- B.
fmle je dokazatelná (je větou VL): |- A. důkaz z předpokladů: T |- A.
věta o dedukci: T |- A → B <~> T, A |- B.
pomocné věty VL:
v1: |- A → A. (z A1) (triviální)
v2: |- ¬ A → ( A → B ) (z A2) (nepravda implikuje cokoliv)
v3: |- ¬¬ A → A (z V2) (zákon vyloučeného třetího)
v4: |- A → ¬¬ A (z V3) (v3 naopak)
v5: |- (A → B) → (¬ B → ¬ A) (z v3,MP) (A3 naopak)
v6: |- ( A → (¬ B → ¬( A → B ))) (z MP) (neplatnost implikace)
v7: |- (¬ A → A) → A (z v6) (nesmysl -> platí negace)
T je sporná, pokud T |- cokoliv, jinak je bezesporná. max. bezesporná T : ∀ S, S &sup
T : S = T.
Lindenbaumova věta : ∀ bezespornou množinu lze rozšířit do max. bezesporné.
Věta o bezespornosti a splnitelnosti: T je bezesporná <~> je splnitelná.
Věta o úplnosti: T |- A <~> T |= A ( |- A <~> |= A ), tj. VL je bezesporná, jsou v ní
dokazatelné právě tautologie.
Věta o kompaktnosti : T splnitelná <~> ∀ konečná T0 ⊂ T je splnitelná.
A ∧ B |- A, A ∧ B |- B, A, B |- A ∧ B,
A ↔ B |- A → B.
A ↔ ( A ∧ A ) (idempotence)
(A ∧ B) ↔ (B ∧ A) (komutatitvita)
(A ∧ B) ∧ C ↔ A ∧ (B ∧ C) (asociativita)
(A1 → ... (An → B) ... ) → ((A1 ∧ ... An) → B)
Věta o ekvivalenci: nechť A' vznikne z A nahrazením někt. výskytů A1, ... An fmlemi
A'1, ... A'n. Potom |- A1 ↔ A'1 ... |- An ↔ A'n ~> |- A' ↔ A.
DeMorgan: ¬ (A ∧ B) ↔ (¬ A ∨ ¬ B), ¬ (A ∨ B) ↔ (¬ A ∧ ¬ B).
A → (A∨ B) (monotonost)
A ↔ (A∨ A) (idempotence)
(A∨ B ) ↔ (B∨ A) (komutativita)
((A ∨ B) ∨ C) ↔ (A ∨ (B∨ C)) (asociativita)
Důkaz rozborem případů : T, (A∨ B) |- C <~> T, A |- C a T, B |- C.
(A ∨ (B ∧ C)) ↔ ((A∨ B) ∧ (A ∨ C))
(A ∧ (B∨ C)) ↔ ((A∧ B) ∨ (A ∧ C))
Věta o norm. tvarech: ∀ fmli lze sestrojit ekvivalentní v CNF/ DNF.
PL
jazyk, termy, fmle; vázaná x volná proměnná, otevřená/uzavřená fmle.
interpretace jazyka : M*, obs. M, fM: M*n --> M*, pM ⊂ Mn., ohodnocení proměnných
e: X --> M (X - proměnné), interpretace termu: t[e] = e(x), t[e]= fM(t1[e], ... tn[e])
A je splněna v M* při e: M* |= A[e], pozměněné ohodnocení : e(x/m)(y) = m( y ≡ x), e(y)
jinak. A pravdivá v M* - M* |= A - je splněna při každém ohodnocení. validní/logicky pravdivá
- |= A (při každé interpretaci jazyka).
t je substituovatelný do A za x, když pro každé y, vyskytující se v t, žádná podfmle (∀ y)B,
(∃ y)B fmle A neobs. (z hlediska A) volný výskyt x. Ax[t].
tx1,...xn[t1, ... tn][e] = t[e(x1/m1, ... xn/mn)] (ti[e] = mi)
M |= Ax1,...xn [t1, ... tn][e] <~> M |= A[e(x1/m1, ... xn/mn)].
další axiomy PL:
SS: (∀ x)A → Ax[t]
SP: (∀ x)(A→ B) → (A→ (∀ x)B) (x není volná v A)
pravidlo generalizace: A |- (∀ x)A (pro lib. x)
pravidlo zavedení ∀: A → B, x není volná v A |- A → (∀ x)B
pravidlo substituce: |- Ax[t] → (∃ x)A
pravidlo zavedení ∃: A → B, x není volná v B |- (∃ x)A → B.
Věta o instancích: A' instance A ~> ( |- A ~> |- A' ). (jen implikace!)
(instance: Ax1, ... xn[t1 ... tn] - dosazuji vše zároveň).
Věta o uzávěru: A' uzávěr A ~> (|- A <~> |- A' ). (uzávěr: pro všechny x1, ... xn s volným
výskytem: (∀ x1) ... (∀ xn) A ).
lemma o distribuci kvantifikátorů: |- A → B ~> ( |- (∀ x)A → (∀ x)B,
|- (∃ x)A → (∃ x)B ).
Věta o ekvivalenci: stejná jako VL.
Věta o variantách : A' varianta A ~> ( |- A' ↔ A ) (varianta: vznikne z A post. nahrazením
podfmlí (Q x)B fmleni (Q y)B[y], y není volná v B ).
Věta o dedukci: A je uzavřená!!: T |- A → B <~> T, A |- B
Věta o konstantách: L' vznikne rozš. L o nové symboly c1, ... cn, potom T |- Ax1,...xn[c1,...cn]
<~> T |- A.
Věta o redukci: T |- A <~> existuje přir. číslo n a formule B1, ... Bn, z nichž každá je uzávěrem
nějaké formule z T, t.ž. |- ( B1 → ( B2 → ... ( Bn → A ) ... ).
důsledek (VD a věty o uzávěru): Je-li A' uzávěr A, potom T |- A <~> T ∪ {¬ A'} sporná.
prenexní tvar: A ≡ (Q1 x1) ... (Qn xn) B (prefix, otevřené jádro). ∀ formuli A lze
sestrojit ekvivalentní A' v prenexním tvaru.
prenexní operace:
podformuli lze nahradit nějakou její variantou
|- ¬ (Q x)B ↔ (Q x)¬ B
|- (B → (Q x)C) ↔ (Q x)(B → C) (x není volná v B)
|- ((Q x)B → C) ↔ (Q x)(B → C) (x není volná v C)
|- ((Q x)B ∧∨ C) ↔ (Q x)(B ∧∨ C) (x není volná v C)
axiomy rovnosti:
R1: x = x (identity)
R2: x1 = y1 → ( x2 = y2 → ( .... → ( f(x1, ... xn) = f(y1, ... yn)) ...))
R3: x1 = y1 → ( x2 = y2 → ( .... → ( p(x1, ... xn) = p(y1, ... yn)) ...))
Zákl. věta o rovnosti: T |- t1 = s1, ... T |- tn = sn. s vznikne z t záměnou někt. ti za si
~> T |- t = s; A' vznikne z A záměnou někt. ti za si, ne bezprostředně za kvantifikátorem ~>
T |- A' = A.
|- t1 = s1 → ... → tn = sn → t[t1,...tn] = t[s1,...sn]
|- t1 = s1 → ... → tn = sn → (A[t1,... tn] ↔ A[s1, ... sn])
|- Ax[t] ↔ (∀ x)(x = t → A)
|- Ax[t] ↔ (∃ x)(x = t ∧ A )
mn. T v jazyce 1. řádu - teorie, její fmle - spec. axiomy; M* interpretace L, T teorie s L: M* model
T: M |= T, jestliže ∀ spec. axiom je v M* pravdivý. A je sémantickým důsledkem T, jestliže
A je pravdivá v každém modelu T ( T |= A ).
lemma : axiomy pred. logiky jsou validní formule.
Věta o korektnosti: T |- A ~> T |= A ( |- A ~> |= A ).
Věta o úplnosti : T |- A <~> T |= A. T bezesporná <~> má model.
kanonická struktura M*: M = { t | t je term bez proměnných }, tM(t1, ... tn) = f(t1,..tn) ∈ M,
(t1,...tn) ∈ pM <~> T |- p(t1, ... tn).
lemma : M* je kanonická struktura pro L, A atomická fmle bez proměnných ~> M* |= A <~> T |- A.
úplná teorie: je bezesporná a ∀ uzavřenou A je A / ¬ A dokazatelná.
Henkinova teorie: ∀ uzavřenout (∃ x)B ex. konstanta, t.ž. T |- (∃ x)B → Bx[c]
Věta o kanonickém modelu: pro T úplnou a Henkinovu je kanonická struktura M* modelem.
rozšíření jazyka: ∀ symbol L je symbolem L' stejného významu a četnosti,
rozšíření teorie: L' rozš. L, ∀ axiom T je větou T'. konzervativní rozšíření: T' |- A
→ T |- A (∀ A ∈ L)
Henkinova věta: Ke každé teorii lze sestrojit konzervativní rozšíření TH, které je Henkinovou
teorií.
Lindenbaumova věta: každou bezespornou T lze rozšířit do úplné S se stejným jazykem.
L' rozšíření L, M'* interpretace L', redukce M'* do L (M'*|L) vznikne z M'* vynecháním zobrazení
a relací mimo L. M'* je expanzí M*, jestliže M* = M'* | L.
lemma: T' rozš. T ~> model M'* model T' ~> M'*|L model T.
Věta o kompaktnosti: T má model <~> ∀ konečný fragment T má model.
Užitečné lemma: T' rozš. T <~> ∀ M'* (model T'): M'*|L je model T.
T' rozš. T, ∀ M* (model T) lze expandovat do M'*, ~> T' je konzervativní rozš. T.
Věta o definici predikátu: D je fmle L, t.ž. ∀ její volné proměnné jsou mezi x1, .. xn.
L' vznikne z L přidáním nového n-árního predikátu p, T' rozš. T vznikne přidáním axiomu
p(x1, ... xn) ↔ D. potom T' je konzervativní, ∀ fmli B' jazyka L' lze p
eliminovat, t.ž. pro upravenou B platí T' |- B ↔ B'.
Věta o zavedení fčního symbolu: Nechť fmle (∃ y)A z L má všechny volné proměnné mezi
x1, ... xn. T' vznikne rozš. T o nový n-ární fční symbol f a přidáním Ay[f(x1,...xn)],
potom T' je konzervativní rozš. T.
otevřená teorie: ∀ axiomy jsou ot. formule; univerzální fmle: je v prenexním tvaru a
všechny kvantifikátory jsou univerzální (podobně existenční), 2 teorie jsou ekvivalentní, mají-li
stejné věty (mají stejné modely, ∀ axiom T je větou S a naopak).
Skolemova věta: k lib. T lze sestrojit otevřenou T', která je konzervativním rozš. T.
SKolemova varianta fmle: ∀ A sestrojit uzavřenou univerzální As, t.ž. |- As → A.
Věta o definici fčního symbolu: D je fmle L s volnými proměnnými mezi x1, ... xn. T |- (∃ y)D,
T |- D → (Dy[t] → y = t), T' vznikne z T přidáním nové n-ární fce f, axiomu
y = f(x1, ... xn) ↔ D. Potom T' je konzervativní, definovaný symbol lze eliminovat.
T' je rozšířením teorie o definice, když vznikne z T konečným počtem rozšíření o definice fcí
a predikátů. pak je konzerv. rozš. T a ∀ fmli A' z T' ex. A z T, t.ž. T' |- A' ↔ A.