-
Hilbertovská dedukce používá jaký jazyk? (jaké operátory?)
Jazyk PL s operátory ¬, →, ∀.
-
Vyjmenuj axiomy se kterými pracuje Hilbertovská dedukce
- Ax 1-3: staří známí z VL:)
- Ax4: Axiom specifikace
- Ax5: Axiom distribuce
- Ax6: Axiom identity
- Ax7: Leibnizův zákon substitutivity identit
- Ax8: beze jména:)
-
Jak zní první tři axiomy Hilbertovské dedukce?
- Ax 1: A→(B→A)
- Ax 2: (A→(B→C))→((A→B)→(A→C))
- Ax 3: (¬B→¬A)→(A→B)
-
Axiom specifikace
Ax 4: ∀xA → A[t/x]
-
Axiom distribuce
- Ax 5: ∀x(A → B) → (A → ∀xB)
- (kde A neobsahuje žádný volný výskyt proměnné x)
-
Axiom identity
Ax 6: ∀x(x = x)
-
Leibnizův zákon substitutivity identit
Ax 7: ∀x∀y((x = y) → (A ↔ A[y/x]))
-
poslední nepojmenovaný axiom?:)
Ax 8: ∀x∀y((x = y) → (f(x) ↔ f(y)))
-
Jaká pravidla odvození Hilbertovská dedukce používá?
-
Dokažte ∀x A ٟI- A[t/x], tedy tzv. Pravidlo univerzální instanciace (UI), jež je obdobou Axiomu specifi kace:
- 1. ∀x A ...předpoklad
- 2. ∀x A→A[t/x] ...Axiom specifikace (tj. Ax 4)
- 3. A[t/x] ...MP (2,1)
- S pomocí VD bychom dané pravidlo dokázali jednoduše takto:
- 1. ٟI- ∀ x A→A[t/x] ...Axiom specifikace (tj. Ax 4)
- 2. ∀x A ٟI- A[t/x] ...VD (1)
-
Dokažte, že jestliže ٟI- A, tak ٟI- A[t/x]. Tedy, že je-li dokazatelná formule A, tak je dokazatelná každá její instance (tzv. Věta o instancích):
- 1. A ...předpoklad
- 2. ∀x A ...PG (1)
- 3. ∀x A→A[t/x] ...Axiom specifikace (tj. Ax 4)
- 4. A[t/x] ...MP (3,2)
-
(Dokažte (A→B) ٟI- (A→∀x B), tedy Pravidlo zavedení ∀ do konsekventu:
- 1. A→B ...předpoklad
- 2. ∀x (A→B) ...PG (1)
- 3. ∀x (A→B)→(A→∀x B) ...Axiom distribuce (tj. Ax 5)
- 4. A→∀x B MP ...(3,2)
-
Dokažte ∀x∀y A ٟI- ∀y∀x A:
- 1. ∀x∀y A předpoklad
- 2. ∀x∀y A→∀y A Axiom specifi kace (tj. Ax 4)
- 3. ∀y A ...MP (2,1)
- 4. ∀y A→A ...Axiom specifikace (tj. Ax 4)
- 5. A ...MP (4,3)
- 6. ∀x A ...PG (5)
- 7. ∀y∀x A ...PG (6)
-
Dokažte ∀x (P(x)→Q(x)), ∀x P(x) ٟI- ∀x Q(x) s pomocí již dokázaného pravidla Univerzální instanciace (UI)
- 1. ∀x (P(x)→Q(x)) ...předpoklad
- 2. ∀x P(x) ...předpoklad
- 3. P(x)→Q(x) ...UI (1) (naším t je x)
- 4. P(x) ...UI (2) (naším t je x)
- 5. Q(x) ...MP (3,4)
- 6. ∀x Q(x) ...PG (5)
-
Dokažte ∀x (P(x)→Q(x)), ∀x P(x) ٟI- ∀x Q(x) bez pomoci UI:
- 1. ∀x (P(x)→Q(x)) ...předpoklad
- 2. ∀x P(x) ...předpoklad
- 3. ∀x P(x)→P(x) ...Axiom specifikace (tj. Ax 4)
- 4. P(x) ...MP (3,2)
- 5. ∀x (P(x)→Q(x))→(P(x)→Q(x)) ...Axiom specifikace (tj. Ax 4)
- 6. P(x)→Q(x) ...MP (5,3)
- 7. Q(x) ...MP (6,4)
- 8. ∀x Q(x) ...PG (7)
-
Dokažte ٟI- A[t/x]→∃x A, tj. zákon existenční generalizace. Vypomůžeme si tautologiemi VL a DM pro záměnu kvantifikátorů:
- 1. I- ٟ∀ x ¬A→¬A[t/x] ...Axiom specifikace (tj. Ax 4)
- 2. ٟI- ∀¬¬ x ¬A→¬A[t/x] ...tautologie VL (z. ¬¬; 1)
- 3. ٟI- A[t/x]→¬∀x ¬A ...tautologie VL (z. transpozice →; 2)
- 4. ٟI- A[t/x]→∃x A ...DM (3)
-
Dokažte A→B (kdy x není volná proměnná v B) ٟI- ∃x A→B. Vypomůžeme si tautologiemi VL a dále DM pro záměnu kvantifikátorů, dále v důkazu využijeme pravidlo pro převod ∀ do konsekventu, ∀x (A→B) / (A→∀x B):
- 1. I- ٟA→B ...předpoklad
- 2. ٟI- ¬ B→¬A ...tautologie VL (z. transpozice →; 1)
- 3. ٟI- ∀ x (¬B→¬A) ...PG (2)
- 4. ٟI- ¬ B→∀x ¬A ...pravidlo zavedení ∀ do konsekventu (3)
- 5. ٟI- ¬ B→¬¬∀x ¬A ...tautologie VL (z. ¬¬; 4)
- 6. ٟI- ¬ ∀x ¬A→B ...tautologie VL (z. kontrapozice →; 5)
- 7. ٟI- ∃ x A→B ...DM (6)
|
|
