Back to main site.
Epistemic logics formalize knowledge and related concepts. Artemov and Protopopescu defined an epistemic logic \(\mathsf{IEL}\) to formalize intuitionistic knowledge. The central idea of this logic is that intuitionistic truth implies intuitionistic knowledge. This heavily contrasts with the classical case, where classical knowledge implies classical truth.
The modality \(K\) is interpreted in \(\mathsf{IEL}\) as \[ K\varphi \text{ holds iff it is intuitionistically known that \(\varphi\)}, \] for all formula \(\varphi\). \(\mathsf{IEL}\) satisfies the principles of co-reflection \(\varphi\to K\varphi\) and weak reflection \(K\varphi\to \neg\neg\varphi\). Note that, in a classical setting, these imply that truth and knowledge coincide.
We extend \(\mathsf{IEL}\) with a modality \(\hat K\) for epistemic possibility. We will show that, for all formula \(\varphi\), \(\hat K P\) is equivalent to \(\neg\neg P\). This implies that \(\varphi\) is epistemically possible iff it one can show that it is impossible to prove the negation of \(\varphi\).
\(\mathsf{IGL}\) is an intuitionistic version of the provability logic \(\mathsf{GL}\) using both box and diamond modalities. It was first studied by Das, van der Giessen, and Marin, who provided two ill-founded proof systems and two semantics for this logic. Later, Aguilera and P. defined a cyclic proof system \(\mathsf{cm\ell IGL}\) for \(\mathsf{IGL}\); they also proved that the set of theorems of \(\mathsf{IGL}\) is recursively enumerable.
We define a well-founded labeled proof system \(\mathsf{\omega m\ell IGL}\) for \(\mathsf{IGL}\) characterized by the following \(\omega\)-rule: \[ \frac{x:\Box^n\bot, \mathbf{R}, \Gamma \vdash \Delta \; (\forall n\in\omega)}{\mathbf{R},\Gamma \vdash \Delta}, \] where \(x\) is a label variable. To prove that all valid formulas of \(\mathsf{IGL}\) can be proved using the \(\omega\)-rule, we use a proof search game argument. To show the soundness of the \(\omega\)-rule are valid, we closely analyze the completeness of \(\mathsf{cm\ell IGL}\). Note that an \(\omega\)-rule for classical \(\mathsf{GL}\) was studied by Tanaka.
Full abstract. Slides soon.
We comment on behavior of constructive diamonds in three settings. First, we review a result of Das and Marin showing that the diamond-free fragment constructive and intuitionistic variants of the modal logic K do not coincide. Second, we show that the constructive and intuitionistic variants of S5 coincide. Last, we show that diamonds are equivalent to double negation in Artemov and Protopopescu's intuitionistic epistemic logic.
We prove that the constructive and intuitionistic variants of the modal logic \(\mathsf{𝖪𝖡}\) coincide. This result contrasts with a recent result by Das and Marin, who showed that the constructive and intuitionistic variants of \(\mathsf{𝖪}\) do not prove the same diamond-free formulas.
Both the intuitionistic propositional calculus \(IPC\) and the modal logic \(S4\) are complete with respect to topological spaces. I will sketch how to combine these their topological semantics to obtain bi-topological semantics for the intuitionistic modal logic \(IS4\). Before that, I will briefly describe the history of topological semantics and \(IS4\). I will also comment on bi-topological semantics for other non-classical variations of \(S4\) and other related ongoing work.
The modal \(\mu\)-calculus is obtained by adding least and greatest fixed-point operators to modal logic. It's alternation hierarchy classifies the \(\mu\)-formulas by their alternation depth: a measure of the codependence of their least and greatest fixed-point operators. The \(\mu\)-calculus' alternation hierarchy is strict over the class of all Kripke frames: for all \(n\), there is a \(\mu\)-formula with alternation depth \(n+1\) which is not equivalent to any formula with alternation depth \(n\). This does not always happen if we restrict the semantics. For example, every \(\mu\)-formula is equivalent to a formula without fixed-point operators over \(\mathsf{S5}\) frames. We show that the multimodal \(\mu\)-calculus' alternation hierarchy is strict over non-trivial fusions of modal logics. We also comment on two examples of multimodal logics where the \(\mu\)-calculus collapses to modal logic.
Das, van der Giessen and Marin recently defined an intuitionistic version of the provability logic \(\mathsf{GL}\). They define birelational and predicate semantics and two non-wellfounded proof systems \(\ell\mathsf{IGL}\) and \(m\ell\mathsf{IGL}\). They prove the completeness and soundness of the two proof systems with respect to both semantics. In the proof of the completeness of \(m\ell\mathsf{IGL}\) with respect to the predicate semantics, they use \(\Sigma^1_1\)-determinacy; a statement not provable in \(\mathsf{ZFC}\). We define a cyclic proof system \(c\ell\mathsf{IGL}\) for IGL and prove its completeness with respect to predicate semantics using open determinacy. In particular, this implies that the completeness of \(m\ell\mathsf{IGL}\) does not need \(\Sigma^1_1\)-determinacy.
We prove that the constructive and intuitionistic variants of the modal logic 𝖪𝖡 coincide. This result contrasts with a recent result by Das and Marin, who showed that the constructive and intuitionistic variants of 𝖪 do not prove the same diamond-free formulas.
Das, van der Giessen and Marin recently defined an intuitionistic version of the provability logic \(\mathsf{GL}\). They define birelational and predicate semantics and two non-wellfounded proof systems \(\ell\mathsf{IGL}\) and \(m\ell\mathsf{IGL}\). They prove the completeness and soundness of the two proof systems with respect to both semantics.
In the proof of the completeness of \(m\ell\mathsf{IGL}\) with respect to the predicate semantics, they use \(\Sigma^1_1\)-determinacy; a statement not provable in \(\mathsf{ZFC}\). We define a cyclic proof system \(c\ell\mathsf{IGL}\) for \(\mathsf{IGL}\) and prove its completeness with respect to predicate semantics using open determinacy. In particular, this implies that the completeness of \(m\ell\mathsf{IGL}\) does not need \(\Sigma^1_1\)-determinacy.
Feedback Turing machines are Turing machines which can query a halting oracle which has information on the convergence or divergence of feedback computations. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A natural question to ask is: what about feedback Turing machines which can ask if computations of the same type converge, diverge, or freeze? We define \(\alpha\)th order feedback Turing machines for each computable ordinal \(\alpha\). We also describe feedback computable and semi-computable sets using inductive definitions and Gale–Stewart games.
Feedback Turing machines are Turing machines which can query a halting oracle which has information on the convergence or divergence of feedback computations. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A natural question to ask is: what about feedback Turing machines which can ask if computations of the same type converge, diverge, or freeze? We define \(\alpha\)th order feedback Turing machines for each computable ordinal \(\alpha\). We also describe feedback computable and semi-computable sets using inductive definitions and Gale–Stewart games.
Feedback Turing machines are Turing machines which can query a halting oracle which has information on the convergence or divergence of feedback computations. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A natural question to ask is: what about feedback Turing machines which can ask if computations of the same type converge, diverge, or freeze? We define \(\alpha\)th order feedback Turing machines for each computable ordinal \(\alpha\). We also describe feedback computable and semi-computable sets using inductive definitions and Gale–Stewart games.
Feedback Turing machines are Turing machines which can query a halting oracle which has information on the convergence or divergence of feedback computations. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A natural question to ask is: what about feedback Turing machines which can ask if computations of the same type converge, diverge, or freeze? We define \(\alpha\)th order feedback Turing machines for each computable ordinal \(\alpha\). We also describe feedback computable and semi-computable sets using inductive definitions and Gale–Stewart games.
We describe a constructive variation of the provability logic \(\mathsf{GL}\) based on Mendler and de Paiva's constructive modal logic \(\mathsf{CK}\).
The modal \(\mu\)-calculus is obtained by adding least and greatest fixed-point operators to modal logic. It's alternation hierarchy classifies the \(\mu\)-formulas by their alternation depth: a measure of the codependence of their least and greatest fixed-point operators. The \(\mu\)-calculus' alternation hierarchy is strict over the class of all Kripke frames: for all \(n\), there is a \(\mu\)-formula with alternation depth \(n+1\) which is not equivalent to any formula with alternation depth \(n\). This does not always happen if we restrict the semantics. For example, every \(\mu\)-formula is equivalent to a formula without fixed-point operators over \(\mathsf{S5}\) frames. We show that the multimodal \(\mu\)-calculus' alternation hierarchy is strict over non-trivial fusions of modal logics. We also comment on two examples of multimodal logics where the \(\mu\)-calculus collapses to modal logic.
Feedback Turing machines are Turing machines which can query a halting oracle which has information on the convergence or divergence of feedback computations. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A natural question to ask is: what about feedback Turing machines which can ask if computations of the same type converge, diverge, or freeze? We define \(\alpha\)th order feedback Turing machines for each computable ordinal \(\alpha\). We also describe feedback computable and semi-computable sets using inductive definitions and Gale–Stewart games.
Blackboard presentation.
Artemov and Protopopescu defined an intuitionistic epistemic logic IEL to reason about intuitionistic knowledge. While classical knowledge implies classical truth, intuitionistic truth implies intuitionistic knowledge. We describe Artemov and Protopopescu's IEL and its BHK interpretation. We characterize epistemic possibility in IEL.
I will talk about the connection between reflection principles and the existence of sequences of beta-models in second-order arithmetic. The reflection principles are of the form: if a formula is provable in a given system, then they are true. Beta-models are coded models which have the same ordinals as the ground model. I comment on how to use this connection to characterize determinacy axioms in reverse mathematics.
We define a constructive version of the \(\mu\)-calculus by adding least and greatest fixed-point operators to constructive modal logic. We define game semantics for the constructive \(\mu\)-calculus and prove its equivalence to bi-relational Kripke semantics. For applications, we study the logic \(\mu\mathsf{CS5}\), a constructive variation of \(\mathsf{S5}\) with fixed-points operators.
The \(\mu\)-calculus is obtained by adding least and greatest fixed-point operators \(\mu\) and \(\nu\) to modal logic. The alternation depth of a formula measures the entanglement of its least and greatest fixed-point operators. Bradfield showed that, for all \(n\in\mathbb{N}\), there is a formula \(W_n\) such that \(W_n\) has alternation depth \(n\) and, over all Kripke frames, \(W_n\) is not equivalent to any formula with alternation depth smaller than \(n\).
The same may not happen over restricted classes of frames: Alberucci and Facchini showed that, the \(\mu\)-calculus collapses to modal logic over \(\mathsf{S5}\) frames. That is, every \(\mu\)-formula is equivalent to a formula without fixed point operators over \(\mathsf{S5}\) frames. Later, Pacheco and Tanaka proved that the \(\mu\)-calculus also collapses to the \(\mu\)-calculus over \(\mathsf{S4.4}\) and \(\mathsf{S4.3.2}\) frames.
We show how Alberucci and Facchini's proof generalize to the \(\mu\)-calculus's collapse over \(n\)-pigeonhole frames. Let \(n\in\omega\). A frame \(F =\langle W,R\rangle\) is an \(n\)-pigeonhole frame iff, for all sequence \(w_0 R^+ w_1 R^+ \cdots R^+ w_n\), there is \(i< j\leq n\) such that \(w_{i}R = w_{j}R\). We also comment about ongoing work to prove the converse: if the \(\mu\)-calculus collapses to modal logic over a class of frames \(\mathsf{F}\), then there is \(n\in\omega\) such all frames \(F\in\mathsf{F}\) are \(n\)-pigeonhole.
(This is joint work with Kazuyuki Tanaka.)
I will review some recent results on the reverse mathematics of automata on infinite words. This is still a new subarea of reverse mathematics, but it already touches very weak and very strong subsystems of second order arithmetic. I also comment on some of my recent research on the reverse mathematics of the Wagner hierarchy.
The \(\mu\)-calculus is obtained by adding to modal logic the least and greatest fixed-point operators \(\mu\) and \(\nu\). The alternation depth of a formula measures the entanglement of its least and greatest fixed-point operators. Bradfield showed that, for all \(n\in\mathbb{N}\), there is a formula \(W_n\) such that \(W_n\) has alternation depth \(n\) and, over all Kripke frames, \(W_n\) is not equivalent to any formula with alternation depth smaller than \(n\).
The same may not happen over restricted classes of frames: Alberucci and Facchini showed that, over frames of \(\mathsf{S5}\), every \(\mu\)-formula is equivalent to a formula without fixed point operators. In this case, we say the \(\mu\)-calculus collapses to modal logic over frames of \(\mathsf{S5}\).
We show how Alberucci and Facchini’s proof generalize to the \(\mu\)-calculus’s collapse over frames of intuitionistic \(\mathsf{S5}\). This generalization can also be done for some non-normal logics and for graded modal logics. We also show that, on the other hand, the \(\mu\)-calculus does not collapse over the bimodal logic \(\mathsf{S5}_2\).
We study some consequences of the \(\mu\)-calculus' alternation hierarchy collapse on some variations of epistemic logic with only one agent; and sketch how to prove that the alternation hierarchy is strict if we have more than one agent. Slides.
The \(\mu\)-calculus is obtained by adding fixed-point operators to modal logic. Alberucci and Facchini showed that every \(\mu\)-formula is equivalent to some modal formula over frames of \(\mathsf{S5}\). The modal logic \(\mathsf{IS5}\) is an intuitionistic variation of \(\mathsf{S5}\), first defined by Prior in 1957. We show that, with slight changes, Alberucci and Facchini's proof also works in frames of \(\mathsf{IS5}\). That is, every \(\mu\)-formula is equivalent to some modal formula over frames of \(\mathsf{IS5}\). This is joint work with Kazuyuki Tanaka. Slides.
It is known that the \(\mu\)-calculus collapses to its alternation-free fragment over transitive frames and to modal logic over equivalence relations. We adapt a proof by D'Agostino and Lenzi to show that the \(\mu\)-calculus collapses to its alternation-free fragment over weakly transitive frames. As a consequence, we show that the \(\mu\)-calculus with derivative topological semantics collapses to its alternation-free fragment. We also study the collapse over frames of \(\mathsf{S4.2}\), \(\mathsf{S4.3}\), \(\mathsf{S4.3.2}\), \(\mathsf{S4.4}\) and \(\mathsf{KD45}\), logics important for Epistemic Logic. At last, we use the \(\mu\)-calculus to define degrees of ignorance on Epistemic Logic and study the implications of \(\mu\)-calculus's collapse over the logics above. This is joint work with Kazuyuki Tanaka. Slides.
It is well-known that several variations of the axiom of determinacy play important roles in the study of reverse mathematics, and the relation between the hierarchy of determinacy (especially the level of \(\Sigma^0_2\) and \(\Sigma^0_3\)) and comprehension axioms are revealed by Tanaka, Nemoto, Montalbán, Shore, and others. In this talk, we show variations of a result by Kołodziejczyk and Michalewski relating determinacy and reflection in second-order arithmetic based on a model-theoretic characterization of the reflection principles. Slides. Video.
Working in second order arithmetic, we characterize determinacy of finite differences of open and \(\Sigma^0_2\) sets as reflection principles. In order to do so we study sequences of coded \(\beta\)-models. More precisely, we prove that: over \(\mathsf{ACA}_0\), \(\Pi^1_2\)-\(\mathsf{Ref}(\mathsf{ACA}_0)\) is equivalent to \(\forall n.(\Sigma^0_1)_n\)-\(\mathsf{Det}^*_0\), and \(\Pi^1_3\)-\(\mathsf{Ref}(\Pi^1_1\)-\(\mathsf{CA}_0)\) is equivalent to \(\forall n.(\Sigma^0_1)_n\)-\(\mathsf{Det}\); over \(\mathsf{ATR}_0\), \(\Pi^1_3\)-\(\mathsf{Ref}(\Pi^1_2\)-\(\mathsf{CA}_0)\) is equivalent to \(\forall n.(\Sigma^0_2)_n\)-\(\mathsf{Det}\). This is joint work with Keita Yokoyama.
This is joint work with Kazuyuki Tanaka. The extended abstract is available in the booklet here.
We study the reflection axioms of the form: if a \(\Pi^1_n\) sentence \(\varphi\) is provable in \(T\), then \(\varphi\) is true (for a fixed theory \(T\)). We prove the relation between the existence of sequence of \(\beta_k\) models and reflection axioms for theories of dependent choices. We also comment on the consequences of these results for determinacy in second-order arithmetic. This is joint work with Keita Yokoyama.
We investigate the alternation hierarchy of the \(\mu\)-calculus in some modal logics commonly used for epistemic logic.
Epistemic logic is the logic of knowledge, belief and related notions. In this presentation I define and motivate three different modal semantics for epistemic logic: relational semantics, topological semantics and neighborhood semantics. I also comment on the relation between these semantics and common knowledge. I assume no knowledge of modal logic.