references.bib

@InCollection{A.B05,
  author        = {Artemov, Sergei N. and Beklemishev, Lev D.},
  title         = {Provability {{Logic}}},
  editor        = {Gabbay, D.M. and Guenthner, F.},
  booktitle     = {Handbook of {{Philosophical Logic}}, 2nd {{Edition}}},
  address       = {Dordrecht},
  publisher     = {Springer Netherlands},
  pages         = {189--360},
  year          = 2005,
  doi           = {10.1007/1-4020-3521-7_3},
  urldate       = {2024-09-19},
  isbn          = {978-1-4020-3521-0},
  langid        = {english}
}

@Article{Avi01,
  author        = {Avigad, Jeremy},
  title         = {Algebraic Proofs of Cut Elimination},
  journal       = {The Journal of Logic and Algebraic Programming},
  volume        = {49},
  number        = {1-2},
  pages         = {15--30},
  year          = 2001,
  month         = sep,
  doi           = {10.1016/S1567-8326(01)00009-1},
  issn          = {15678326},
  urldate       = {2025-10-08},
  copyright     = {https://www.elsevier.com/tdm/userlicense/1.0/},
  langid        = {english}
}

@Article{Avi04,
  author        = {Avigad, Jeremy},
  title         = {Forcing in {{Proof Theory}}},
  journal       = {The Bulletin of Symbolic Logic},
  volume        = {10},
  number        = {3},
  publisher     = {[Association for Symbolic Logic, Cambridge University Press]},
  pages         = {305--333},
  year          = 2004,
  eprint        = {3185188},
  eprinttype    = {jstor},
  issn          = {10798986},
  urldate       = {2026-01-29}
}

@Article{Bek90,
  author        = {Beklemishev, L D},
  title         = {On the {{Classification}} of {{Propositional Provability Logics}}},
  journal       = {Mathematics of the USSR-Izvestiya},
  volume        = {35},
  number        = {2},
  pages         = {247--275},
  year          = 1990,
  month         = apr,
  doi           = {10.1070/IM1990v035n02ABEH000701},
  issn          = {0025-5726},
  urldate       = {2024-09-19},
  langid        = {english}
}

@Book{Boo94,
  author        = {Boolos, George},
  title         = {The {{Logic}} of {{Provability}}},
  address       = {Cambridge},
  publisher     = {Cambridge University Press},
  year          = 1994,
  doi           = {10.1017/CBO9780511625183},
  isbn          = {978-0-521-48325-4}
}

@Book{C.Z97,
  author        = {Chagrov, Alexander and Zakharyaschev, Michael},
  title         = {Modal Logic},
  series        = {Oxford Logic Guides},
  number        = {35},
  address       = {Oxford : New York},
  publisher     = {Clarendon Press ; Oxford University Press},
  year          = 1997,
  isbn          = {978-0-19-853779-3},
  lccn          = {QA9.46 .C47 1997}
}

@Book{Che80,
  author        = {Chellas, Brian F.},
  title         = {Modal {{Logic}}: {{An Introduction}}},
  address       = {Cambridge},
  publisher     = {Cambridge University Press},
  year          = 1980,
  doi           = {10.1017/CBO9780511621192},
  isbn          = {978-0-521-29515-4}
}

@Article{F.M.T92,
  author        = {Fitting, Melvin C. and Marek, V. Wiktor and Truszczy{\'n}ski, Miroslaw},
  title         = {The {{Pure Logic}} of {{Necessitation}}},
  journal       = {Journal of Logic and Computation},
  volume        = {2},
  number        = {3},
  pages         = {349--373},
  year          = 1992,
  doi           = {10.1093/logcom/2.3.349},
  issn          = {0955-792X, 1465-363X},
  urldate       = {2025-10-08},
  langid        = {english}
}

@Article{G.J08,
  author        = {Goris, E. and Joosten, J. J.},
  title         = {Modal {{Matters}} for {{Interpretability Logics}}},
  journal       = {Logic Journal of IGPL},
  volume        = {16},
  number        = {4},
  pages         = {371--412},
  year          = 2008,
  month         = jun,
  doi           = {10.1093/jigpal/jzn013},
  issn          = {1367-0751, 1368-9894},
  urldate       = {2025-11-10},
  langid        = {english}
}

@Article{G.J11,
  author        = {Goris, E. and Joosten, J. J.},
  title         = {A New Principle in the Interpretability Logic of All Reasonable Arithmetical Theories},
  journal       = {Logic Journal of IGPL},
  volume        = {19},
  number        = {1},
  pages         = {1--17},
  year          = 2011,
  month         = feb,
  doi           = {10.1093/jigpal/jzp082},
  issn          = {1367-0751, 1368-9894},
  urldate       = {2025-11-05},
  langid        = {english}
}

@Book{G.T.L89,
  author        = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
  title         = {Proofs and types},
  zbl           = {0671.68002},
  series        = {Camb. Tracts Theor. Comput. Sci.},
  volume        = {7},
  publisher     = {Cambridge etc.: Univ. Press},
  year          = {1989},
  fseries       = {Cambridge Tracts in Theoretical Computer Science},
  issn          = {0965-9103},
  isbn          = {0-521-37181-3},
  language      = {English},
  zbmath        = {42059}
}

@Article{Gir91,
  author        = {Girard, Jean-Yves},
  title         = {A New Constructive Logic: Classic Logic},
  journal       = {Mathematical Structures in Computer Science},
  volume        = {1},
  number        = {3},
  publisher     = {Cambridge University Press},
  edition       = {2009/03/04},
  pages         = {255--296},
  year          = 1991,
  doi           = {10.1017/S0960129500001328},
  issn          = {0960-1295}
}

@Book{H.C07,
  author        = {Hughes, George Edward and Cresswell, M. J.},
  title         = {A New Introduction to Modal Logic},
  address       = {London},
  publisher     = {Routledge},
  edition       = {Transferred to digital print},
  year          = 2007,
  isbn          = {978-0-415-12600-7},
  langid        = {english}
}

@Article{J.V04,
  author        = {Joosten, Joost J and Visser, A},
  title         = {How to {{Derive Principles}} of {{Interpretability Logic A Toolkit}}},
  year          = 2004,
  langid        = {english}
}

@Article{Jer16,
  author        = {Je{\v r}{\'a}bek, Emil},
  title         = {Cluster Expansion and the Boxdot Conjecture},
  journal       = {Mathematical Logic Quarterly},
  volume        = {62},
  number        = {6},
  pages         = {608--614},
  year          = 2016,
  month         = dec,
  doi           = {10.1002/malq.201600036},
  shorttitle    = {Cluster Expansion and the Boxdot Conjecture},
  issn          = {09425616},
  urldate       = {2025-10-08},
  copyright     = {http://doi.wiley.com/10.1002/tdm\_license\_1.1},
  langid        = {english}
}

@Article{Jer73,
  author        = {Jeroslow, R. G.},
  title         = {Redundancies in the {{Hilbert-Bernays}} Derivability Conditions for {{G\"odel}}'s Second
                  Incompleteness Theorem},
  journal       = {Journal of Symbolic Logic},
  volume        = {38},
  number        = {3},
  pages         = {359--367},
  year          = 1973,
  month         = sep,
  doi           = {10.2307/2273028},
  issn          = {0022-4812, 1943-5886},
  urldate       = {2024-07-04},
  copyright     = {https://www.cambridge.org/core/terms},
  langid        = {english}
}

@Article{K.O21,
  author        = {Kurahashi, Taishi and Okawa, Yuya},
  title         = {Modal Completeness of Sublogics of the Interpretability Logic {{IL}}},
  journal       = {Mathematical Logic Quarterly},
  volume        = {67},
  number        = {2},
  pages         = {164--185},
  year          = 2021,
  month         = may,
  doi           = {10.1002/malq.202000037},
  issn          = {0942-5616, 1521-3870},
  urldate       = {2025-10-29},
  langid        = {english}
}

@Misc{Kop23,
  author        = {Kopnev, Kirill},
  title         = {The {{Finite Model Property}} of {{Some Non-normal Modal Logics}} with the {{Transitivity Axiom}}},
  number        = {arXiv:2305.08605},
  publisher     = {arXiv},
  year          = 2023,
  month         = may,
  doi           = {10.48550/arXiv.2305.08605},
  eprint        = {2305.08605},
  primaryclass  = {math},
  urldate       = {2025-07-04},
  archiveprefix = {arXiv},
  langid        = {english}
}

@Article{Mik22,
  author        = {Mikec, Luka},
  title         = {On {{Logics}} and {{Semantics}} for {{Interpretability}}},
  journal       = {The Bulletin of Symbolic Logic},
  volume        = {28},
  number        = {2},
  pages         = {265--265},
  year          = 2022,
  month         = jun,
  doi           = {10.1017/bsl.2022.3},
  issn          = {1079-8986, 1943-5894},
  urldate       = {2025-11-03},
  langid        = {english}
}

@Book{Min00,
  author        = {Mints, Grigori E.},
  title         = {A {{Short Introduction}} to {{Intuitionistic Logic}}},
  publisher     = {Kluwer Academic Publishers},
  year          = 2000
}

@Book{Pac17,
  author        = {Pacuit, Eric},
  title         = {Neighborhood {{Semantics}} for {{Modal Logic}}},
  series        = {Short {{Textbooks}} in {{Logic}}},
  address       = {Cham},
  publisher     = {Springer International Publishing},
  year          = 2017,
  doi           = {10.1007/978-3-319-67149-9},
  issn          = {2522-5480, 2522-5499},
  urldate       = {2025-07-14},
  copyright     = {http://www.springer.com/tdm},
  isbn          = {978-3-319-67148-2}
}

@Book{Sch14,
  author        = {Schindler, Ralf},
  title         = {Set {{Theory}}: {{Exploring Independence}} and {{Truth}}},
  series        = {Universitext},
  address       = {Cham},
  publisher     = {Springer International Publishing},
  year          = 2014,
  doi           = {10.1007/978-3-319-06725-4},
  shorttitle    = {Set {{Theory}}},
  urldate       = {2025-10-08},
  copyright     = {https://www.springernature.com/gp/researchers/text-and-data-mining},
  isbn          = {978-3-319-06724-7},
  langid        = {english}
}

@PhDThesis{Seg71,
  author        = {Segerberg, Karl Krister},
  title         = {An {{Essay}} in {{Classical Modal Logic}}},
  year          = 1971,
  school        = {Stanford University}
}

@Article{Sve91,
  author        = {{\v S}vejdar, V{\'i}t{\v e}zslav},
  title         = {Some Independence Results in Interpretability Logic},
  journal       = {Studia Logica},
  volume        = {50},
  number        = {1},
  pages         = {29--38},
  year          = 1991,
  month         = mar,
  doi           = {10.1007/BF00370385},
  issn          = {0039-3215, 1572-8730},
  urldate       = {2025-11-04},
  copyright     = {http://www.springer.com/tdm},
  langid        = {english}
}

@Article{Vis21,
  author        = {Visser, Albert},
  title         = {The Absorption Law: {{Or}}: How to {{Kreisel}} a {{Hilbert}}--{{Bernays}}--{{L\"ob}}},
  journal       = {Archive for Mathematical Logic},
  volume        = {60},
  number        = {3-4},
  pages         = {441--468},
  year          = 2021,
  month         = may,
  doi           = {10.1007/s00153-020-00752-5},
  shorttitle    = {The Absorption Law},
  issn          = {0933-5846, 1432-0665},
  urldate       = {2026-02-20},
  langid        = {english}
}

@Book{Vis88,
  author        = {Visser, A.},
  title         = {Preliminary Notes on Interpretability Logic},
  series        = {Logic {{Group}} Preprint Series},
  number        = {29},
  publisher     = {Department of Philosophy, University of Utrecht},
  year          = 1988
}

@Book{Vis97,
  author        = {Visser, Albert},
  title         = {An Overview of {{Interpretability Logic}}},
  series        = {Logic {{Group}} Preprint Series},
  number        = {53},
  publisher     = {Department of Philosophy, University of Utrecht},
  year          = 1997,
  langid        = {english}
}

@Article{Vuk99,
  author        = {Vukovi{\'c}, Mladen},
  title         = {The {{Principles}} of {{Interpretability}}},
  journal       = {Notre Dame Journal of Formal Logic},
  volume        = {40},
  number        = {2},
  year          = 1999,
  month         = apr,
  doi           = {10.1305/ndjfl/1038949538},
  issn          = {0029-4527},
  urldate       = {2025-11-04},
  langid        = {english}
}