Why for proof tree we supposed to start with the negation here, when the proof is pretty straight-forward (e.g. for natural deduction)? λ p2q2r : P → Q → R. λ p2q : P → Q. λ p : P. (p2q2r p) (p2q p) : R : p2q2r : P → Q → R, p2q : P → Q ⊢ P → R : p2q2r : P → Q → R ⊢ (P → Q) → (P → R) : ∅ ⊢ (P → (Q → R)) → ((P → Q) → (P → R)) ■ Q.E.D.
Any chance you’ll ever make a video on sequent calculus?
He actually did
Thanks for the thorough explanation of the side by side examples. Great content!
Thanks! Glad you enjoyed.
Why for proof tree we supposed to start with the negation here, when the proof is pretty straight-forward (e.g. for natural deduction)?
λ p2q2r : P → Q → R.
λ p2q : P → Q.
λ p : P.
(p2q2r p) (p2q p) : R
: p2q2r : P → Q → R, p2q : P → Q ⊢ P → R
: p2q2r : P → Q → R ⊢ (P → Q) → (P → R)
: ∅ ⊢ (P → (Q → R)) → ((P → Q) → (P → R))
■ Q.E.D.
Proof trees start with the negation of the conclusion. The proof you’ve given here is natural deduction style, like the one in the video.
As a bottom line: looks like proof trees more expressive when there's a lot of negations or disjunctions.
They’re just as powerful as one another, but proof trees deal with disjunction in a simpler way
It looks to me like proof trees would be easier to a lot easier automate.