7 papers
Proof Theory and Interpolation for Sacchetti's Logics
Borja Sierra Miranda, Thomas Studer
We study the proof theory of Sacchetti's modal logics, a family of logics generalizing Gödel--Löb provability logic by replacing transitivity with n-transitivity. We make three m…
Uniform Lyndon Interpolation via Non-wellfounded Proofs
Borja Sierra Miranda, Thomas Studer
Non-wellfounded proof theory has been applied to establish uniform interpolation and Lyndon interpolation (separately) for multiple logics. However, it has not yet been used to pro…
Proof Theory for Bimodal Provability Logics
Borja Sierra Miranda, Thomas Studer
We provide the first (non-labelled) sequent calculi for bimodal provability logics with "usual" provability predicates. In particular, we introduce calculi for the logics CS, CSM a…
Uniform interpolation for interpretability logic
Sebastijan Horvat, Borja Sierra Miranda, Thomas Studer
We present a proof-theoretical study of the interpretability logic IL, providing a wellfounded and a non-wellfounded sequent calculus for IL. The non-wellfounded calculus is used t…
Cut elimination for a non-wellfounded system for the master modality
Borja Sierra Miranda, Thomas Studer
In previous work we provided a method for eliminating cuts in non-wellfounded proofs with a local-progress condition, these being the simplest kind of non-wellfounded proofs. The m…
Knowledge and Common Knowledge of Strategies
Borja Sierra Miranda, Thomas Studer
Most existing work on strategic reasoning simply adopts either an informed or an uninformed semantics. We propose a model where knowledge of strategies can be specified on a fine-g…