The paper “Tautology elimination, cut elimination, and S5” published in this journal presents a novel method for establishing by proof analysis the admissibility of the rule of tautology elimination for certain sequent calculi. Since tautology elimination will typically imply the admissibility of cut, the method promises a new path to show the admissibility of cut for cut-free calculi on which the standard techniques within structural proof theory seem inapplicable. This paper shows that the method as presented involves an error.
Tautology Elimination, Cut Elimination and S4?
Fjellstad, Andreas
2025
Abstract
The paper “Tautology elimination, cut elimination, and S5” published in this journal presents a novel method for establishing by proof analysis the admissibility of the rule of tautology elimination for certain sequent calculi. Since tautology elimination will typically imply the admissibility of cut, the method promises a new path to show the admissibility of cut for cut-free calculi on which the standard techniques within structural proof theory seem inapplicable. This paper shows that the method as presented involves an error.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
2528.pdf
accesso aperto
Tipologia:
Published (Publisher's Version of Record)
Licenza:
Creative commons
Dimensione
155.2 kB
Formato
Adobe PDF
|
155.2 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.




