Skip to content

Instantly share code, notes, and snippets.

@kt3k

kt3k/sketch00.lk

Last active July 16, 2021 05:33
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kt3k/694c0fd4b5cf1d9ad0aa79e60ee1de5e to your computer and use it in GitHub Desktop.
Save kt3k/694c0fd4b5cf1d9ad0aa79e60ee1de5e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
sketch00.lk
|- (p -> r) | (q -> r) -> (p & q -> r)
---
(p -> r) | (q -> r) |- p & q -> r
---
(p -> r) | (q -> r), p & q |- r
---
(p -> r) | (q -> r), p, q |- r
---1-1
p -> r, p, q |- r
---
~p | r, p, q |- r
---2-1
~p, p, q |- r
---
p, q |- r, p <--- axiom
---2-2
r, p, q |- r <--- axiom
---1-2
q -> r, p, q |- r
---
~q | r, p, q |- r
---3-1
~q, p, q |- r
---
p, q |- r, q <--- axiom
---3-2
r, p, q |- r <--- axiom
Raw
sketch01.lk
|- (p -> r) | (q -> r) -> (p & q -> r) --- theorem
(p -> r) | (q -> r) |- p & q -> r
(p -> r) | (q -> r), p & q |- r
(p -> r) | (q -> r), p, q |- r
---1-1
p -> r, p, q |- r
~p | r, p, q |- r
---2-1
~p, p, q |- r
p, q |- r, p <--- axiom
---2-2
r, p, q |- r <--- axiom
---1-2
q -> r, p, q |- r
~q | r, p, q |- r
---3-1
~q, p, q |- r
p, q |- r, q <--- axiom
---3-2
r, p, q |- r <--- axiom
Raw
sketch02.lk
|- (p -> r) | (q -> r) -> (p & q -> r) --- theorem
(p -> r) | (q -> r) |- p & q -> r
(p -> r) | (q -> r), p & q |- r
(p -> r) | (q -> r), p, q |- r
-
p -> r, p, q |- r
~p | r, p, q |- r
-
~p, p, q |- r
p, q |- r, p <--- axiom
-
r, p, q |- r <--- axiom
-
q -> r, p, q |- r
~q | r, p, q |- r
-
~q, p, q |- r
p, q |- r, q <--- axiom
-
r, p, q |- r <--- axiom
Raw
sketch03.lk
th theorem0: (p -> r) | (q -> r) -> (p & q -> r)
p, q |- r, p
~p, p, q |- r
-------------
r, p, q |- r
------------
~p | r, p, q |- r
p -> r, p, q |- r
-----------------
p, q |- r, q
~q, p, q |- r
-------------
r, p, q |- r
------------
~q | r, p, q |- r
q -> r, p, q |- r
-----------------
(p -> r) | (q -> r), p, q |- r
(p -> r) | (q -> r), p & q |- r
(p -> r) | (q -> r) |- p & q -> r
|- (p -> r) | (q -> r) -> (p & q -> r)
Raw
sketch04.lk
th theorem0: (p -> r) | (q -> r) -> (p & q -> r)
p, q |- r, p
~p, p, q |- r --- A
r, p, q |- r --- B
A B
~p | r, p, q |- r
p -> r, p, q |- r --- C
p, q |- r, q
~q, p, q |- r --- D
r, p, q |- r --- E
D E
~q | r, p, q |- r
q -> r, p, q |- r --- F
C F
(p -> r) | (q -> r), p, q |- r
(p -> r) | (q -> r), p & q |- r
(p -> r) | (q -> r) |- p & q -> r
|- (p -> r) | (q -> r) -> (p & q -> r)
Raw
sketch05.lk
th theorem0: (p -> r) | (q -> r) -> (p & q -> r)
p, q |- r, p
~p, p, q |- r --A
r, p, q |- r --B
A=> B=>
~p | r, p, q |- r
p -> r, p, q |- r --C
p, q |- r, q
~q, p, q |- r --D
r, p, q |- r --E
D=> E=>
~q | r, p, q |- r
q -> r, p, q |- r --F
C=> F=>
(p -> r) | (q -> r), p, q |- r
(p -> r) | (q -> r), p & q |- r
(p -> r) | (q -> r) |- p & q -> r
|- (p -> r) | (q -> r) -> (p & q -> r)
Raw
sketch06.lk
th theorem0: (p -> r) | (q -> r) -> (p & q -> r)
p, q |- r, p
~p, p, q |- r --A
r, p, q |- r <=A
~p | r, p, q |- r
p -> r, p, q |- r --B
p, q |- r, q
~q, p, q |- r --C
r, p, q |- r <=C
~q | r, p, q |- r
q -> r, p, q |- r <=B
(p -> r) | (q -> r), p, q |- r
(p -> r) | (q -> r), p & q |- r
(p -> r) | (q -> r) |- p & q -> r
|- (p -> r) | (q -> r) -> (p & q -> r)
Raw
sketch07.lk
th theorem0: (p -> r) | (q -> r) -> (p & q -> r)
(
(
(
(
(
(
(
p, q |- r, p
~p, p, q |- r
)
r, p, q |- r
~p | r, p, q |- r
)
p -> r, p, q |- r
)
(
(
(
p, q |- r, q
~q, p, q |- r
)
r, p, q |- r
~q | r, p, q |- r
)
q -> r, p, q |- r
)
(p -> r) | (q -> r), p, q |- r
)
(p -> r) | (q -> r), p & q |- r
)
(p -> r) | (q -> r) |- p & q -> r
)
|- (p -> r) | (q -> r) -> (p & q -> r)
)
Raw
sketch08.lk
th theorem0: |- (p -> r) | (q -> r) -> (p & q -> r)
p, q |- r, p =>
~p, p, q |- r --A
r, p, q |- r --B
A=> B=>
~p | r, p, q |- r =>
p -> r, p, q |- r --C
p, q |- r, q =>
~q, p, q |- r --D
r, p, q |- r --E
D=> E=>
~q | r, p, q |- r =>
q -> r, p, q |- r --F
C=> F=>
(p -> r) | (q -> r), p, q |- r =>
(p -> r) | (q -> r), p & q |- r =>
(p -> r) | (q -> r) |- p & q -> r =>
|- (p -> r) | (q -> r) -> (p & q -> r)
Raw
sketch09.lk
th theorem0: |- (p -> r) | (q -> r) -> (p & q -> r)
p, q |- r, p =>
~p, p, q |- r => r, p, q |- r =>
~p | r, p, q |- r =>
p -> r, p, q |- r --A
p, q |- r, q =>
~q, p, q |- r => r, p, q |- r =>
~q | r, p, q |- r =>
q -> r, p, q |- r => A =>
(p -> r) | (q -> r), p, q |- r =>
(p -> r) | (q -> r), p & q |- r =>
(p -> r) | (q -> r) |- p & q -> r =>
|- (p -> r) | (q -> r) -> (p & q -> r)
Raw
sketch10.lk
th theorem0: |- (p -> r) | (q -> r) -> (p & q -> r)
p, q |- r, p =>
~p, p, q |- r --
r, p, q |- r --
0=> 1=>
~p | r, p, q |- r =>
p -> r, p, q |- r --X
p, q |- r, q =>
~q, p, q |- r --
r, p, q |- r --
2=> 3=>
~q | r, p, q |- r =>
q -> r, p, q |- r --
X=> 4=>
(p -> r) | (q -> r), p, q |- r =>
(p -> r) | (q -> r), p & q |- r =>
(p -> r) | (q -> r) |- p & q -> r =>
|- (p -> r) | (q -> r) -> (p & q -> r)
Raw
sketch11.lk
th theorem0: |- (p -> r) | (q -> r) -> (p & q -> r)
p, q |- r, p =>
~p, p, q |- r --
r, p, q |- r --
^=> ^^=>
~p | r, p, q |- r =>
p -> r, p, q |- r --X
p, q |- r, q =>
~q, p, q |- r --
r, p, q |- r --
^=> ^^=>
~q | r, p, q |- r =>
q -> r, p, q |- r --
X=> ^=>
(p -> r) | (q -> r), p, q |- r =>
(p -> r) | (q -> r), p & q |- r =>
(p -> r) | (q -> r) |- p & q -> r =>
|- (p -> r) | (q -> r) -> (p & q -> r)
Raw
sketch12.lk
th theorem0: |- (p -> r) | (q -> r) -> (p & q -> r)
p, q |- r, p =>
~p, p, q |- r --
r, p, q |- r --
^1=> ^2=>
~p | r, p, q |- r =>
p -> r, p, q |- r --X
p, q |- r, q =>
~q, p, q |- r --
r, p, q |- r --
^1=> ^2=>
~q | r, p, q |- r =>
q -> r, p, q |- r --
X=> ^1=>
(p -> r) | (q -> r), p, q |- r =>
(p -> r) | (q -> r), p & q |- r =>
(p -> r) | (q -> r) |- p & q -> r =>
|- (p -> r) | (q -> r) -> (p & q -> r)
@kt3k
Copy link
Author

kt3k commented Jul 15, 2021 •
edited

theorem0 =>
|- (p -> r) | (q -> r) -> (p & q -> r)

@kt3k
Copy link
Author

kt3k commented Jul 16, 2021 •
edited

theorem => pub fn
lemma => private fn

import theorem0, theorem1 from ./my-theory.lk

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment