Smullyan signed tableaux system and the Sequent Calculus
formulas prefixed by T or F correspond to the position on the left or on the right in the sequents:
T ¬X
F X
F ¬X
T X
T X ∧ Y
T X
T Y
F X ∧ Y
F X F Y
T X ∨ Y
T X T Y
F X ∨ Y
F X
F Y
T X → Y
F X T Y
F X → Y
T X
F Y
Example:
F(¬(A ∧ B) → (¬A ∨ ¬B))
T¬(A ∧ B)
F¬A ∨ ¬B
FA ∧ B
F¬A
F¬B
TA
TB
FA FB
× ×
A A
A, ¬A
A, (¬A ∨ ¬B)
B B
B, ¬B
B, (¬A ∨ ¬B)
A ∧ B, (¬A ∨ ¬B)
¬(A ∧ B) (¬A ∨ ¬B)
¬(A ∧ B) → (¬A ∨ ¬B)
1
5. The cut rule corresponds to growth of deduction at the root:
A A B C
L→
A, A → B C
forms a deduction
A
·
·
·
A A → B
→E
B
·
·
·
C
growing towards the root
A A B B
L→
A, A → B C B A → B
cut
A, B B
corresponds to
A
·
·
·
A
B
·
·
·
A → B
→E
B
2
Cut-elimination: To any proof of A B, there exists a cut-free proofA B.
We need to remove each
A A+
, B C, A+
D
A, C B, D
Depening on A+
:
A+
= B ∧ C:
A B, B A C, B
R∧
A, A B ∧ C, B, B
C, B D
L1∧
C, B ∧ C D
cut
A, A , C B, B , D
transforms into
A B, B C, B D
cut
A, A , C B, B , D
A+
= B ∨ C:
A C, B
R2∨
A B ∨ C, B
C, B D B , C D
L∨
B, B , B ∨ C D, D
cut
A, A , C B, B , D
transforms into
A B, B C, B D
cut
A, A , C B, B , D
3
4
5