LK0
Take single source code from cli ./lk0 source.lk
evaluate it as a proof
show errors if any
show result if proof is valid or not
Proof consists of series of Sequents
Proof := Sq0\n+"---"\n+Sq1\n+"---"+\nSq2
Sequent consists of left and right sets of propositions. They are separeted by turnstile |-:
Sequent := Anticedents |- Succedents
Cedents := Anticedents | Succedents
Cedents are also called Pro
In cedents, propositions are separated by comma ,:
Propositions := empty | Proposition [, Propositions]
Note: There can be empty propositions.
A proposition
Symbols:
|- turnstile
E exists
A any
& and
| or
-> implies
, comma
~ not
--- denotes separator of sequents (inference line)
Example.0
code:lk
|-
---
A |- A
Ex.1
code:lk
p, r |- q, r
Ex. 2 (long, reversed)
code: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