arXiv subjects
Publications and source records attributed to Mojtaba Mojtahedi.
We axiomatize the provability logic of $\HA$ and prove its decidability. Furthermore, we axiomatize the preservativity and relative admissibility relations for several modal logics extending iK4. A principal technical tool is the introduction of a new type of semantics, termed \emph{provability models}, for modal logics extending iGL. This semantics combines elements of standard Kripke semantics with provability in propositional modal logics.
In this paper, we study a new Kripke-style semantics for classical modal logic, named as provability models. We study provability models for the propositional modal logics K, K4, S4 GL, GLP and the interpretability logic ILM. Provability models combine features of Kripke models with the assignment of logics to individual worlds. Originally introduced in [Mojtahedi, 2022], these models allowed the first author to establish arithmetical completeness for intuitionistic provability logic. Interestingly, we show that the ILM is complete for the same provability models of GL. We improve provability models to predicative and decidable provability models in the case of GL and ILM. Furthermore, we prove a soundness and completeness of GLP for provability models.
This paper studies relative unification and admissibility in the intuitionistic logic. We generalize results of [Ghilardi, 1999; Iemhoff, 2001a] and prove them relative in NNIL(par) propositions, the class of propositions with No Nested Implications in the Left made up from parameters. The main application of such generalization is to characterize provability logic of Heyting Arithmetic HA and prove its decidability [Mojtahedi, 2022].
We examine the interplay between projectivity (in the sense that was introduced by S.~Ghilardi) and uniform post-interpolant for the classical and intuitionistic propositional logic. More precisely, we explore whether a projective substitution of a formula is equivalent to its uniform post-interpolant, assuming the substitution leaves the variables of the interpolant unchanged. We show that in classical logic, this holds for all formulas. Although such a nice property is missing in intuitionistic logic, we provide Kripke semantical characterisation for propositions with this property. As a main application of this, we show that the unification type of some extensions of intuitionistic logic are finitary. In the end, we study admissibility for intuitionistic logic, relative to some sets of formulae. The first author of this paper recently considered a particular case of this relativised admissibility and found it useful in characterising the provability logic of Heyting Arithmetic.
Let $\mathcal{PL}({\sf T},{\sf T}')$ and $\mathcal{PL}_{Σ_1}({\sf T},{\sf T}')$ respectively indicates the provability logic and $Σ_1$-provability logic of ${\sf T}$ relative in ${\sf T}'$. In this paper we characterize the following relative provability logics: $\mathcal{PL}_{Σ_1}({\sf HA},\mathbb{N})$, $\mathcal{PL}_{Σ_1}({\sf HA},{\sf PA})$, $\mathcal{PL}_{Σ_1}({\sf HA}^*,\mathbb{N})$, $\mathcal{PL}_{Σ_1}({\sf HA}^*,{\sf PA})$, $\mathcal{PL}({\sf PA},{\sf HA})$, $\mathcal{PL}_{Σ_1}({\sf PA},{\sf HA})$, $\mathcal{PL}({\sf PA}^*,{\sf HA})$, $\mathcal{PL}_{Σ_1}({\sf PA}^*,{\sf HA})$, $\mathcal{PL}({\sf PA}^*,{\sf PA})$, $\mathcal{PL}_{Σ_1}({\sf PA}^*,{\sf PA})$, $\mathcal{PL}({\sf PA}^*,\mathbb{N})$, $\mathcal{PL}_{Σ_1}({\sf PA}^*,\mathbb{N})$ (see Table \ref{Table-Theories}). It turns out that all of these provability logics are decidable. The notion of {\em reduction} for provability logics, first informally considered in \cite{reduction}. In this paper, we formalize a generalization of this notion (\Cref{Definition-Reduction-PL}) and provide several reductions of provability logics (See diagram \ref{Diagram-full}). The interesting fact is that $\mathcal{PL}_{Σ_1}({\sf HA},\mathbb{N})$ is the hardest provability logic: the arithmetical completenesses of all provability logics listed above, as well as well-known provability logics like $\mathcal{PL}({\sf PA},{\sf PA})$, $\mathcal{PL}({\sf PA},\mathbb{N})$, $\mathcal{PL}_{Σ_1}({\sf PA},{\sf PA})$, $\mathcal{PL}_{Σ_1}({\sf PA},\mathbb{N})$ and $\mathcal{PL}_{Σ_1}({\sf HA},{\sf HA})$ are all propositionally reducible to the arithmetical completeness of $\mathcal{PL}_{Σ_1}({\sf HA},\mathbb{N})$.
For the Heyting Arithmetic HA, HA* is defined as the theory $\{A\mid {\sf HA}\vdash A^{\Box}\}$, where $A^{\Box}$ is called the box translation of $A$. We characterize the $Σ_1$-provability logic of HA* as a modal theory ${\sf iH}_σ^*$.
We can look at a first-order (or propositional) intuitionistic Kripke model as an ordered set of classical models. In this paper, we show that for a finite-depth Kripke model in an arbitrary first-order language or propositional language, local (classical) truth of a formula is equivalent to non-classical truth (truth in the Kripke semantics) of a Friedman's translation of that formula, i.e. $ α\Vdash A^ρ\Leftrightarrow \mathfrak{M}_α\models A$. We introduce some applications of this fact. We extend the result of [Ardeshir and Hessam 2002] and show that semi-narrow Kripke models of Heyting Arithmetic $ {\sf HA} $ are locally $ {\sf PA} $.