Sequent Calculus Proof of Transitivity of Implication

[CMCDragonkai]

Proving: (A → B) ∧ (B → C) ⊢ A → C

Me and Quoc worked on the above via the rules and guidance given on this page: http://sakharov.net/sequent.html We got:

------      ------
A |- A      B |- B
-------------------  -> left            ------
A -> B, A |- B                           C |- C
--------------------------------------------------  -> left
A, A -> B, B -> C    |-                      C
--------------------------------------------------  -> right
A -> B, B -> C       |-                      A -> C
---------------------------------------------------  &  left
(A -> B) & (B -> C), B -> C          |-      A -> C
---------------------------------------------------  &  left
(A -> B) & (B -> C), (A -> B) & (B -> C)  |- A -> C
---------------------------------------------------  C  left
(A -> B) & (B -> C)             |-           A -> C

However using: http://logitext.mit.edu/Intuitionistic/proving/.28A+.2D.3E+B.29+.2F.5C+.28B+.2D.3E+C.29+.7C.2D+.28A+.2D.3E+C.29 it shows us something like:

-----
C ⊢ C
----------- (W l)
B, C, A ⊢ C
--------------- (→ l)
B, B → C, A ⊢ C
--------------- (→ l)
A → B, B → C, A ⊢ C
------------------- (→ r)
A → B, B → C ⊢ A → C
------------------------- (∧ l)
(A → B) ∧ (B → C) ⊢ A → C

Which one is correct? Are they equivalent?

Also how can left implication be used in the second example when there isn't 2 subformulas on the top of the line?

@plintx

[rowandavies]

As we discussed in person after the session today, that seems to be a non-standard version of the implication left rule that kind of builds in the C |- C and B |- B premises without explicitly showing them.

It wouldn't be complete by itself though - specifically, cut-elimination would fail. So, they must have the more general version too. In fact, you can see this in the example: http://logitext.mit.edu/proving/.28.28A+.2D.3E+B.29+.2D.3E+A.29+.2D.3E+A

So, I'd treat the ->L rule as just an abbreviation where you skip premises like C|-C

[rowandavies]

Oh, and the paper I was thinking of had a similar but not quite the same rule, with a non-standard account of cut elimination - see: http://ai2-s2-pdfs.s3.amazonaws.com/102f/95136b4ef12948110e4d4d777b43b339d6e4.pdf