In this article we study the complexity of disjunction property for intuitionistic logic, the modal logics S4, S4.1, Grzegorczyk logic, Gödel-Löb logic, and the intuitionistic counterpart of the modal logic K. For S4 we even prove the feasible interpolation theorem and we provide a lower bound for the length of proofs. The techniques we use do not require proving structural properties of the calculi in hand, such as the cut-elimination theorem or the normalization theorem. This is a key point of our approach, since it allows us to treat logics for which only Hilbert-style characterizations are known
Ferrari, M., Fiorentini, C., Fiorino, G. (2005). On the complexity of the disjunction property in intuitionistic and modal logics. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 6(3), 519-538 [10.1145/1071596.1071598].
On the complexity of the disjunction property in intuitionistic and modal logics
Fiorino, G
2005
Abstract
In this article we study the complexity of disjunction property for intuitionistic logic, the modal logics S4, S4.1, Grzegorczyk logic, Gödel-Löb logic, and the intuitionistic counterpart of the modal logic K. For S4 we even prove the feasible interpolation theorem and we provide a lower bound for the length of proofs. The techniques we use do not require proving structural properties of the calculi in hand, such as the cut-elimination theorem or the normalization theorem. This is a key point of our approach, since it allows us to treat logics for which only Hilbert-style characterizations are known
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
