Ian Shillito

Ian Shillito

he/him

Logician formalising in Rocq

Posts by Collection

portfolio

publications

A multi-labelled sequent calculus for Topo-Logic

Published in Journal of Logic and Computation, 2020

We present a labelled sequent calculus for a trimodal epistemic logic exhibited in Baltag et al. (2017, Logic, Rationality, and Interaction, pp. 330–346), an extension of the so called ‘Topo-Logic’. To the best of our knowledge, our calculus is the first proof-calculus for this logic. This calculus is obtained via an adaptation of the label technique by internalizing a semantics over topological spaces. This internalization leads to the generation of two kinds of labels in our calculus and the labelling of formulae by pairs of labels. These novelties give tools to provide a simple calculus that is intuitively connected to the semantics. We prove that this calculus enjoys many structural properties such as admissibility of cut, admissibility of contraction and invertibility of its rules. Finally, we exhibit a proof search strategy for our calculus that allows us to prove completeness in a direct way by the extraction of a countermodel from a failure of proof. To define this strategy, we design a tool for controlling the generation of labels in the construction of a search tree, although the termination of this strategy is still open.

Recommended citation: Shillito, Ian. (2020). "A multi-labelled sequent calculus for Topo-Logic." Journal of Logic and Computation. 30 (2).
Download Paper

Bi-Intuitionistic Logics: A New Instance of an Old Problem

Published in Advances in Modal Logic 2020, 2020

As anyone who reads the literature on bi-intuitionistic logic will know, the numerous papers by Cecylia Rauszer are foundational but confusing. For example: these papers claim and retract various versions of the deduction theorem for bi-intuitionistic logic; they erroneously claim that the calculus is complete with respect to rooted canonical models; and they erroneously claim the admissibility of cut in her sequent calculus for this logic. Worse, authors such as Crolard, have based some of their own foundational work on these confused and confusing results and proofs. We trace this confusion to the axiomatic formalism of RBiInt in which Rauszer first characterized bi-intuitionistic logic and show that, as in modal logic, RBiInt can be interpreted as two different consequence relations. We remove this ambiguity by using generalized Hilbert calculi, which are tailored to capture consequence relations. We show that RBiInt leads to two logics, wBIL and sBIL, with different extensional and meta-level properties, and that they are, respectively, sound and strongly complete with respect to the Kripkean local and global semantic consequence relations

Recommended citation: Goré, Rajeev and Shillito, Ian. (2020). "Bi-Intuitionistic Logics: A New Instance of an Old Problem." Advances in Modal Logic 2020.
Download Paper

Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq

Published in TABLEAUX 2021, 2021

Recently, Brighton gave another cut-admissibility proof for the standard set-based sequent calculus GLS for modal provability logic GL. One of the two induction measures that Brighton uses is novel: the maximum height of regress trees in an auxiliary calculus called RGL. Tautology elimination is established rather than direct cut-admissibility, and at some points the input derivation appears to be ignored in favour of a derivation obtained by backward proof-search. By formalising the GLS calculus and the proofs in Coq, we show that: (1) the use of the novel measure is problematic under the usual interpretation of the Gentzen comma as set union, and a multiset-based sequent calculus provides a more natural formulation; (2) the detour through tautology elimination is unnecessary; and (3) we can use the same induction argument without regress trees to obtain a direct proof of cut-admissibility that is faithful to the input derivation.

Recommended citation: Goré, Rajeev, Ramanayake, Revantha and Shillito, Ian. (2022). "Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq" TABLEAUX 2021.
Download Paper

Direct elimination of additive-cuts in GL4ip: verified and extracted

Published in Advances in Modal Logic 2022, 2022

Recently, van der Giessen and Iemhoff proved cut-admissibility for the sequent calculus GL4ip for propositional intuitionistic provability logic. To do so, they were forced to use an indirection via the GL3ip calculus as GL4ip resists all standard direct cut- admissibility techniques. This indirection leaves little hope for the extraction of a comprehensible cut-elimination procedure for GL4ip from their work. We eliminate this indirection: we prove the admissibility of additive cut for GL4ip in a direct way by using a recently discovered proof technique which requires the existence of a terminating backward proof-search procedure in this calculus. By formalising our results in Coq we: (1) exhibit a successful direct proof technique for cut-admissibility for GL4ip ; (2) extract a syntactic cut-elimination procedure for GL4ip in Haskell ; and (3) use a local measure on sequents based on the shortlex order to show that the proof- search terminates. Once again, we see an unusual phenomenon in that terminating backward proof-search forms the basis for syntactic cut-elimination rather than for semantic cut-free completeness.

Recommended citation: Goré, Rajeev and Shillito, Ian. (2022). "Direct elimination of additive-cuts in GL4ip: verified and extracted" Advances in Modal Logic 2022.
Download Paper

New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq

Published in Australian University, 2023

We contribute to the shift towards logic as a fully formalised science by formalising in the interactive theorem prover Coq both new and known results. Our contribution is threefold. First, we define pen-and-paper general notions required in our dissertation: propo- sitional and first-order syntax, axiomatic calculus, sequent calculus, Kripke semantics, soundness and completeness results. Furthermore, we instantiate these notions in modal logic, both in pen-and-paper and in Coq. Consequently, we constitute a readily available and usable Coq library containing foundational elements of the study of modal logic, which can thus serve as a basis for the formalisation of further works in non-classical logics. Second, we exhibit and rectify a mistake that has gone unnoticed for almost fifty years in the foundations of propositional and first-order bi-intuitionistic logic. We show that both in the propositional and first-order case, what was conceived of as a unique bi-intuitionistic logic is in fact two distinct logics. We trace these confusions back to a fundamental problem in the axiomatic proof theory of propositional and first-order bi-intuitionistic logic: traditional Hilbert calculi are not designed to treat logics as conse- quence relations. They lead to an ambiguous notion of deduction from assumptions that can cause us to conflate distinct rules and thus distinct logics. More precisely, we show that the bi-intuitionistic rule (DN) is ambiguous in a traditional context and splits into two distinct rules in the context of generalized Hilbert calculi. As a consequence, we obtain two generalized Hilbert calculi in the propositional (wBIH and sBIH) and first-order (FOwBIH and FOsBIH) case, for bi-intuitionistic logic that differ only in the disambiguated version of the (DN) rule they incorporate. Unsurprisingly, these systems capture two distinct propositional logics (wBIL and sBIL) and first-order logics (FOwBIL and FOsBIL), which have been conflated in the literature. Third, we obtain cut-elimination results for the sequent calculi GLS and GL4ip, which are sequent calculi for, respectively, the classical modal provability logic GLL and the in- tuitionistic modal provability logic iGLL. These results involve a novel proof technique for the admissibility of additive-cut called the “mhd proof technique”, which relies on the fact that terminating backward proof-search allows us to attribute a “maximal height of derivations” to each sequent. So, for each of the calculi GLS and GL4ip, we define a back- ward proof-search procedure for it and develop a thorough termination argument using a local measure on sequents and a well-founded relations along which this measure decreases upwards in the proof-search. Then, we directly prove the admissibility of additive-cut for both calculi using the mhd proof technique. We use this number, the mhd of a sequent, as an induction measure in arguments involving local and syntactic transformations, allowing us to exhibit and hence extract from our Coq formalisation Haskell programs constituting cut-elimination procedures.

Recommended citation: Shillito, Ian. (2023). "New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq" PhD thesis, Australian National University.
Download Paper

A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised (Best paper award)

Published in TABLEAUX 2023, 2023

We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direct way, leading to a straightforward cut-elimination procedure. All proofs have been formalised in the interactive theorem prover Coq.

Recommended citation: Shillito, Ian, van der Giessen, Iris, Goré, Rajeev and Iemhoff, Rosalie. (2023). "A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised" TABLEAUX 2023.
Download Paper

A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic

Published in Conference on Certified Programs and Proofs 2024, 2024

Using the Coq proof assistant, we investigate the minimal non-constructive principles needed to show soundness and completeness of propositional bi-intuitionistic logic. Before being revisited and corrected by Goré and Shillito, the completeness of bi-intuitionistic logic, an extension of intuitionistic logic with a dual operation to implication, had a rather erratic history, making it an ideal case for computer mechanisation. Moreover, contributing a constructive perspective, we observe that the completeness of bi-intuitionistic logic explicates the same characteristics already observed in an ongoing effort to analyse completeness theorems in general.

Recommended citation: Shillito, Ian and Dominik Kirst. (2024). "A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic" CPP 2024.
Download Paper

Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL (Best paper award)

Published in IJCAR 2024, 2024

The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) Godel-Lob logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong Lob logic iSL, for which this is the first proof-theoretic construction of uniform interpolants. Our work also yields verified programs that allow one to compute the propositional quantifiers on any formula in this logic.

Recommended citation: Férée, Hugo, van der Giessen, Iris, van Gool, Sam and Shillito, Ian. (2024). "Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL" IJCAR 2024.
Download Paper

Intuitionistic S4 as a logic of topological spaces

Published in Journal of Logic and Computation, 2024

We design and study various topological semantics for the diamond-free intuitionistic modal logic iS4⁠, an intuitionistic analogue of S4⁠. Ultimately we prove that ordinary topological spaces can be used as semantics, using the specialization order to interpret intuitionistic implication and the interior for the modality. Some of our soundness and completeness results are mechanised in Coq.

Recommended citation: de Groot, Jim and Shillito, Ian. (2024). "Intuitionistic S4 as a logic of topological spaces" Journal of Logic and Computation.
Download Paper

Completeness of First-Order Bi-Intuitionistic Logic

Published in Computer Science Logic 2025, 2025

We provide a succinct and verified completeness proof for first-order bi-intuitionistic logic, relative to constant domain Kripke semantics. By doing so, we make up for the almost-50-year-old substantial mistakes in Rauszer’s foundational work, detected but unresolved by Shillito two years ago. Moreover, an even earlier but historically neglected proof by Klemke has been found to contain at least local errors by Olkhovikov and Badia, that remained unfixed due to the technical complexity of Klemke’s argument. To resolve this unclear situation once and for all, we give a succinct completeness proof, based on and dualising a standard proof for constant domain intuitionistic logic, and verify our constructions using the Coq proof assistant to guarantee correctness.

Recommended citation: Kirst, Dominik and Shillito, Ian. (2025). "Completeness of First-Order Bi-Intuitionistic Logic" Computer Science Logic 2025.
Download Paper

Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents

Published in Computer Science Logic 2025, 2025

It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of models into a constant domain. This makes it an interesting problem to find a sound and complete proof system for first-order bi-intuitionistic logic with non-constant domains that is also conservative over first-order intuitionistic logic. We solve this problem by presenting the first sound and complete proof system for first-order bi-intuitionistic logic with increasing domains. We formalize our proof system as a polytree sequent calculus (a notational variant of nested sequents), and prove that it enjoys cut-elimination and is conservative over first-order intuitionistic logic. A key feature of our calculus is an explicit eigenvariable context, which allows us to control precisely the scope of free variables in a polytree structure. Semantically this context can be seen as encoding a notion of Scott’s existence predicate for intuitionistic logic. This turns out to be crucial to avoid the collapse of domains and to prove the completeness of our proof system. The explicit consideration of the variable context in a formula sheds light on a previously overlooked dependency between the residuation principle and the existence predicate in the first-order setting, which may help to explain the difficulty in designing a sound and complete proof system for first-order bi-intuitionistic logic.

Recommended citation: Lyon, Tim, Shillito, Ian and Tiu, Alwen. (2025). "Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents" Computer Science Logic 2025.
Download Paper

talks

teaching

Teaching experience 1

Undergraduate course, University 1, Department, 2014

This is a description of a teaching experience. You can use markdown like any other post.

Teaching experience 2

Workshop, University 1, Department, 2015

This is a description of a teaching experience. You can use markdown like any other post.