Error when trying to proof SCombinator

Master / Vertiefung Logikbasierte Wissensrepräsentation
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

Error when trying to proof SCombinator
Hello everyone,

I tried to proof SCombinator in MMT to get better understanding.
Yet I keep running in to errors. Appreciate if some one could help with debug:

SCombinator_proof : {P,Q,R} (P ⟹ (Q ⟹ R)) ⟹ ((P ⟹ Q) ⟹ (P ⟹ R)) ❘
                   = [P,Q,R] impI ([p1] impI ([p2] impI ([p3] impE (impE p1 p3) (impE p2 p3)))) ❙

The most important error message I think is following:

  • inferred type must conform to expected type; the term is: impI [p1]impI [p2]impI [p3]impE impE p1 p3 impE p2 p3
    Judgment P:o, Q:o, R:o |- ⊦(/I/13 P Q R)⟹(/I/14 P Q R) <: (P⟹(Q⟹R))⟹((P⟹Q)⟹(P⟹R))
    not obviously equal, trying subtyping rules

Somehow MMT failed to infer the type of p1, p2 and p3, which should be ⊦ P⟹(Q⟹R), ⊦Q⟹R and ⊦ P.

3

weird… can you show me tomorrow? Then we can debug together…