Open CMCDragonkai opened 7 years ago
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
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
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:
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:
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