arXiv subjects

Mojtaba Mojtahedi

Publications and source records attributed to Mojtaba Mojtahedi.

8 recordsLinked to original sources

arXiv2026

Infinitary provability logic

Gödel-Löb provability logic $\GL$ is a propositional modal system that on one hand enjoys completeness with respect to conversely well-founded Kripke frames and on the other hand captures all modal principles about $\PA$-provability that are provable in $\PA$ itself. In the present paper we carry out an initial investigation into the question of what the infinitary counterpart of $\GL$ is. We develop a non-well-founded deep inference proof system $\dgla$ for the modal language with at most countably infinite conjunctions and disjunctions. We show that the calculus is sound and complete for well-founded transitive Kripke frames. Using Kripke-Platek set theory we develop an interpretation of the infinitary modal language in terms of infinitary provability over admissible sets. Then we show that a natural Hilber-style variant of infinitary $\GL$ is sound for this interpretation. We leave open, however, the question if $\dgla$ proves any additional theorems in comparison with the Hilbert-style calculus. Nevertheless, under certain conditions we do show that the infinitary provability logic arising from certain admissible sets lies between the set of theorems of the Hilbert-style calculus and the non-well-founded deep inference system.

math.LO↗

arXiv2026

On the Provability Logic of HA

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.

math.LO↗

arXiv2025

Provability Models

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.

math.LO↗

arXiv2025

Relative Unification in Intuitionistic Logic: Towards provability logic of HA

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].

math.LO↗

arXiv2024

Projectivity meets Uniform Post-Interpolant: Classical and Intuitionistic Logic

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.

math.LO↗

arXiv2019

Hard Provability Logics

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})$.

math.LO↗

arXiv2018

The $Σ_1$-Provability Logic of HA*

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}_σ^*$.

math.LO↗

arXiv2017

Localizing Finite-Depth Kripke Models

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} $.

math.LO↗