Cut rule of ProofTactic allows you to "prove" any theorem

[giammirove]

Cut rule of ProofTactic allows you to "prove" any theorem. For instance:

val thm1 = Theorem(Q(x) /\ !Q(x) |- ()) {
  var l = have((Q(x) /\ !Q(x)) |- (Q(x) /\ !Q(x))) by Restate
  have(thesis) by Cut(l, l)
}
val thm2 = Theorem(() |- Q(x) /\ !Q(x)) {
  var l = have(!(Q(x) /\ !Q(x)) |- !(Q(x) /\ !Q(x))) by Restate
  val l2 = have(!(Q(x) /\ !Q(x)) |- ()) by Cut(l, l)
  have(thesis) by Tautology.from(l2)
}
val thm3 = Theorem(!(Q(x) /\ !Q(x)) |- ()) {
  var l = have(!((Q(x) /\ !Q(x))) |- !((Q(x) /\ !Q(x)))) by Restate
  have(thesis) by Cut(l, l)
}
val thm4 = Theorem(Q(x) |- !Q(x)) {
  var l = have((Q(x), Q(x)) |- (Q(x), Q(x))) by Restate
  val l2 = have((Q(x), Q(x)) |- ()) by Cut(l, l)
  have(thesis) by Tautology.from(l2)
}

The issue arises whenever you use cut with the right part as (). The method withParameters of Cut has internally 4 variables: leftSequent,rightSequent,botK,phiK. The wrong checks that allow the unwanted behavior are:

• !K.isSameSet(botK.left + phiK, leftSequent.left ++ rightSequent.left)
• !K.isSameSet(botK.right + phiK, leftSequent.right ++ rightSequent.right)

For instance in thm1 we would have:

• leftSequent:= (Q(x) /\ !Q(x)) |- (Q(x) /\ !Q(x))
• rightSequent:= (Q(x) /\ !Q(x)) |- (Q(x) /\ !Q(x))
• botK:= Q(x) /\ !Q(x) |- ()
• phiK:= (Q(x) /\ !Q(x)) So:
• botK.right + phiK := (Q(x) /\ !Q(x))
• leftSequent.left ++ rightSequent.left := (Q(x) /\ !Q(x)) , (Q(x) /\ !Q(x))

Therefore it passes the check.

[SimonGuilloud]

Nice catch! The solution is not quite technically correct however, as then something of the form

          |- φ          φ, φ |- Π
        -----------------------------
                   φ |- Π

would not be accepted. It is indeed really a technicality as such a step serves no purpose in practice, but necessary to remain faithful with a more standard sequent calculus presentation where sequents are represented with lists. So the check (efficient) would be something like if LeftSequent.left.contains(phiK) then botK.left.contains(phiK) The actual correction also needs to change different files.

Thanks a lot for the report!

[giammirove]

Oh I see, I'll close the PR then !