Skip to content

Commit fdaec8f

Browse files
5HT5HT
committed
format
1 parent 8a4a095 commit fdaec8f

1 file changed

Lines changed: 31 additions & 31 deletions

File tree

β€Žlibrary/foundations/logic/hilbert.andersβ€Ž

Lines changed: 31 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -11,30 +11,30 @@ import library/foundations/mltt/proto
1111

1212
-- [SchΓΆnfinkel] Ukraine, Dnipro
1313

14-
def K := Ξ  (p q: Ξ©) (x: p.1), q.1 β†’ p.1
15-
def S := Ξ  (p q r: Ξ©) (x: p.1 β†’ q.1 β†’ r.1) (y: p.1 β†’ q.1), p.1 β†’ r.1
16-
def E := Ξ  (p : Ξ©), p.1 β†’ p.1
14+
def K := Ξ  (p q: Ξ©') (x: p.1), q.1 β†’ p.1
15+
def S := Ξ  (p q r: Ξ©') (x: p.1 β†’ q.1 β†’ r.1) (y: p.1 β†’ q.1), p.1 β†’ r.1
16+
def E := Ξ  (p : Ξ©'), p.1 β†’ p.1
1717

18-
def k : K := \ (p q : Ξ©) (x: p.1) (y: q.1), x
19-
def s : S := \ (p q r: Ξ©) (f: p.1 β†’ q.1 β†’ r.1) (g: p.1 β†’ q.1) (h: p.1), f h (g h)
20-
def e : E := \ (p : Ξ©) (x: p.1), x
21-
def e₁ : E := \ (p : Ξ©) (x: p.1), s p p p (k p p) (k p p x) x
18+
def k : K := \ (p q : Ξ©') (x: p.1) (y: q.1), x
19+
def s : S := \ (p q r: Ξ©') (f: p.1 β†’ q.1 β†’ r.1) (g: p.1 β†’ q.1) (h: p.1), f h (g h)
20+
def e : E := \ (p : Ξ©') (x: p.1), x
21+
def e₁ : E := \ (p : Ξ©') (x: p.1), s p p p (k p p) (k p p x) x
2222

2323
def X
24-
:= Ξ  (p q r x y z h w: Ξ©)
24+
:= Ξ  (p q r x y z h w: Ξ©')
2525
(k: (p.1 β†’ q.1 β†’ p.1) β†’
2626
((x.1 β†’ y.1 β†’ z.1) β†’ (x.1 β†’ y.1) β†’ x.1 β†’ z.1) β†’
2727
(r.1 β†’ w.1 β†’ r.1) β†’ h.1), h.1
2828

2929
def x : X
30-
:= \ (p q r a b c h w: Ξ©)
30+
:= \ (p q r a b c h w: Ξ©')
3131
(v: (p.1 β†’ q.1 β†’ p.1) β†’
3232
((a.1 β†’ b.1 β†’ c.1) β†’ (a.1 β†’ b.1) β†’ a.1 β†’ c.1) β†’
3333
(r.1 β†’ w.1 β†’ r.1) β†’ h.1),
3434
v (k p q) (s a b c) (k r w)
3535

3636
def x₁ : X
37-
:= \ (p q r x y z h w: Ξ©)
37+
:= \ (p q r x y z h w: Ξ©')
3838
(v: (p.1 β†’ q.1 β†’ p.1) β†’
3939
((x.1 β†’ y.1 β†’ z.1) β†’ (x.1 β†’ y.1) β†’ x.1 β†’ z.1) β†’
4040
(r.1 β†’ w.1 β†’ r.1) β†’ h.1),
@@ -46,37 +46,37 @@ def x=x₁ : PathP (<_>X) x x₁ := <_> x
4646

4747
-- [Łukashewicz]
4848

49-
def L3-1 := Ξ  (p q: Ξ©) (x: p.1), q.1 β†’ p.1
50-
def L3-2 := Ξ  (p q r: Ξ©) (x: p.1 β†’ q.1 β†’ r.1) (y: p.1 β†’ q.1), p.1 β†’ r.1
51-
def L3-3 := Ξ  (p q: Ξ©) (x: Β¬ p.1 β†’ Β¬ q.1), q.1 β†’ p.1
49+
def L3-1 := Ξ  (p q: Ξ©') (x: p.1), q.1 β†’ p.1
50+
def L3-2 := Ξ  (p q r: Ξ©') (x: p.1 β†’ q.1 β†’ r.1) (y: p.1 β†’ q.1), p.1 β†’ r.1
51+
def L3-3 := Ξ  (p q: Ξ©') (x: Β¬ p.1 β†’ Β¬ q.1), q.1 β†’ p.1
5252

5353
-- [Frege]
5454

55-
def THEN-1 := Ξ  (p q: Ξ©) (x: p.1), q.1 β†’ p.1
56-
def THEN-2 := Ξ  (p q r: Ξ©) (x: p.1 β†’ q.1 β†’ r.1) (y: p.1 β†’ q.1), p.1 β†’ r.1
57-
def THEN-3 := Ξ  (p q r: Ξ©) (x: p.1 β†’ q.1 β†’ r.1), q.1 β†’ p.1 β†’ r.1
58-
def FRG-1 := Ξ  (p q: Ξ©) (x: p.1 β†’ q.1), Β¬ q.1 β†’ Β¬ p.1
59-
def FRG-2 := Ξ  (p: Ξ©), Β¬ (Β¬ p.1) β†’ p.1
60-
def FRG-3 := Ξ  (p: Ξ©), p.1 β†’ Β¬ (Β¬ p.1)
55+
def THEN-1 := Ξ  (p q: Ξ©') (x: p.1), q.1 β†’ p.1
56+
def THEN-2 := Ξ  (p q r: Ξ©') (x: p.1 β†’ q.1 β†’ r.1) (y: p.1 β†’ q.1), p.1 β†’ r.1
57+
def THEN-3 := Ξ  (p q r: Ξ©') (x: p.1 β†’ q.1 β†’ r.1), q.1 β†’ p.1 β†’ r.1
58+
def FRG-1 := Ξ  (p q: Ξ©') (x: p.1 β†’ q.1), Β¬ q.1 β†’ Β¬ p.1
59+
def FRG-2 := Ξ  (p: Ξ©'), Β¬ (Β¬ p.1) β†’ p.1
60+
def FRG-3 := Ξ  (p: Ξ©'), p.1 β†’ Β¬ (Β¬ p.1)
6161

6262
-- [Hilbert]
6363

64-
def H-1 := Ξ  (p q: Ξ©) (x: p.1), q.1 β†’ p.1
65-
def H-2 := Ξ  (p q r: Ξ©) (x: p.1 β†’ q.1 β†’ r.1), q.1 β†’ p.1 β†’ r.1
66-
def H-3 := Ξ  (p q r: Ξ©) (x: q.1 β†’ r.1), ((p.1 β†’ q.1) β†’ (p.1 β†’ r.1))
67-
def H-4 := Ξ  (p q: Ξ©) (x: p.1), Β¬ q.1 β†’ p.1
68-
def H-5 := Ξ  (p q: Ξ©) (x: p.1 β†’ q.1), (Β¬ q.1 β†’ p.1) β†’ p.1
64+
def H-1 := Ξ  (p q: Ξ©') (x: p.1), q.1 β†’ p.1
65+
def H-2 := Ξ  (p q r: Ξ©') (x: p.1 β†’ q.1 β†’ r.1), q.1 β†’ p.1 β†’ r.1
66+
def H-3 := Ξ  (p q r: Ξ©') (x: q.1 β†’ r.1), ((p.1 β†’ q.1) β†’ (p.1 β†’ r.1))
67+
def H-4 := Ξ  (p q: Ξ©') (x: p.1), Β¬ q.1 β†’ p.1
68+
def H-5 := Ξ  (p q: Ξ©') (x: p.1 β†’ q.1), (Β¬ q.1 β†’ p.1) β†’ p.1
6969

7070
-- [Church]
7171

72-
def C-1 := Ξ  (p q: Ξ©) (x: p.1), q.1 β†’ p.1
73-
def C-2 := Ξ  (p q r: Ξ©) (x: p.1 β†’ q.1 β†’ r.1) (y: p.1 β†’ q.1), p.1 β†’ r.1
74-
def C-3 := Ξ  (p: Ξ©), ((p.1 β†’ 𝟎) β†’ 𝟎) β†’ p.1
72+
def C-1 := Ξ  (p q: Ξ©') (x: p.1), q.1 β†’ p.1
73+
def C-2 := Ξ  (p q r: Ξ©') (x: p.1 β†’ q.1 β†’ r.1) (y: p.1 β†’ q.1), p.1 β†’ r.1
74+
def C-3 := Ξ  (p: Ξ©'), ((p.1 β†’ 𝟎) β†’ 𝟎) β†’ p.1
7575

7676
-- [Tarski, Bernays]
7777

78-
def TB-1 := Ξ  (p q r: Ξ©) (x: q.1 β†’ r.1), (q.1 β†’ r.1) β†’ (p.1 β†’ r.1)
79-
def TB-2 := Ξ  (p q: Ξ©) (x: p.1), q.1 β†’ p.1
80-
def TB-3 := Ξ  (p q: Ξ©) (x: (p.1 β†’ q.1) β†’ p.1), p.1
81-
def TB-4 := Ξ  (p: Ξ©), 𝟎 β†’ p.1
78+
def TB-1 := Ξ  (p q r: Ξ©') (x: q.1 β†’ r.1), (q.1 β†’ r.1) β†’ (p.1 β†’ r.1)
79+
def TB-2 := Ξ  (p q: Ξ©') (x: p.1), q.1 β†’ p.1
80+
def TB-3 := Ξ  (p q: Ξ©') (x: (p.1 β†’ q.1) β†’ p.1), p.1
81+
def TB-4 := Ξ  (p: Ξ©'), 𝟎 β†’ p.1
8282

0 commit comments

Comments
Β (0)