-
Notifications
You must be signed in to change notification settings - Fork 4
/
01-logika.lean
112 lines (75 loc) · 2.16 KB
/
01-logika.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
example : p ∧ q ↔ q ∧ p :=
sorry
example : p ∨ q ↔ q ∨ p :=
sorry
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
sorry
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
sorry
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
sorry
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
sorry
example : (p → (q → r)) ↔ (p ∧ q → r) :=
sorry
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
sorry
-- Demorganovi zakoni
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
sorry
example : ¬p ∨ ¬q → ¬(p ∧ q) :=
sorry
-- Zakon neprotivrečnosti
example : ¬(p ∧ ¬p) :=
sorry
example : p ∧ ¬q → ¬(p → q) :=
sorry
example : ¬p → (p → q) :=
sorry
example : (¬p ∨ q) → (p → q) :=
sorry
example : p ∨ False ↔ p :=
sorry
example : p ∧ False ↔ False :=
sorry
example : (p → q) → (¬q → ¬p) :=
sorry
open Classical
theorem dne {p : Prop} (h : ¬¬p) : p :=
sorry
theorem imp_or {p q : Prop} (h : p → q) : ¬p ∨ q :=
sorry
theorem or_imp {p q : Prop} (h : ¬p ∨ q) : p → q :=
sorry
variable (p q r s : Prop)
example : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
sorry
example : ¬(p ∧ q) → ¬p ∨ ¬q :=
sorry
example : ¬(p → q) → p ∧ ¬q :=
sorry
example : (p → q) → (¬p ∨ q) :=
sorry
example : (¬q → ¬p) → (p → q) :=
sorry
example : p ∨ ¬p :=
sorry
example : (((p → q) → p) → p) :=
sorry
------------------------------ Logika prvog reda -------------------------------
variable (p q : α → Prop)
example {α : Type} {φ : α → Prop} : (∀ x : α, φ x) ↔ (¬ ∃ x : α, ¬ φ x) :=
sorry
example {α : Type} {φ : α → Prop} : (∃ x : α, φ x) ↔ ¬(∀ x : α, ¬ φ x) :=
sorry
example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
sorry
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
sorry
example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
sorry
example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
sorry
example {road : Type} {toRome : road → Prop} :
¬ ∀ r : road, toRome r → ∃ r : road, ¬ toRome r :=
sorry