Proof Checking
Language and Logic
p : P interpreted as “p is a proof of P”
p : P -> Q is furthermore interpreted as
“p is a rule for converting a proof of P into a proof of Q”.
The language of propositions revisited
Truth Falsity P, Q, … P and Q P or Q P -> Q
not P = P -> Falsity
Proofs are created via rules.
Postulates: and-elimination
Postulates: and-introduction
Postulates: or-introduction
Postulates: or-elimination
Postulates: falsity-elimination
Postulates: double-negation-elimination
Postulates
Modus ponens
P, Q, R : P ⋀ (Q ⋀ R)
P⋀Q : Q⋀P
P⋀Q , Q→R : R
¬¬P, P → Q : P ∧ (Q ∨ R)
P → (Q ∧ R) : P → Q
P →(Q→R) : Q→(P →R)
P∨(Q∧R), S : (S∧P)∨Q
Q→¬P : ¬(P∧Q)
¬P → Q, ¬Q : P
P ∨ Q, P → R, S → ¬Q : R ∨ ¬S
Online installation: http://bit.ly/2ID3jN6