-
Projectivity meets Uniform Post-Interpolant: Classical and Intuitionistic Logic
Authors:
Mojtaba Mojtahedi,
Konstantinos Papafilippou
Abstract:
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 cla…
▽ More
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.
△ Less
Submitted 29 March, 2024; v1 submitted 28 March, 2024;
originally announced March 2024.
-
Relative Unification in Intuitionistic Logic: Towards provability logic of HA
Authors:
Mojtaba Mojtahedi
Abstract:
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 pro…
▽ More
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].
△ Less
Submitted 11 May, 2022;
originally announced June 2022.
-
On Provability Logic of HA
Authors:
Mojtaba Mojtahedi
Abstract:
We axiomatize the provability logic of HA and show that it is decidable. Moreover we axiomatize the preservativity and relative admissibility for several modal logics extending iK4. As a main tool, we also provide some sort of semantics, called provability semantics, for modal logics extending iGL, which is a mixture of usual Kripke semantics and provability in propositional modal logics.
We axiomatize the provability logic of HA and show that it is decidable. Moreover we axiomatize the preservativity and relative admissibility for several modal logics extending iK4. As a main tool, we also provide some sort of semantics, called provability semantics, for modal logics extending iGL, which is a mixture of usual Kripke semantics and provability in propositional modal logics.
△ Less
Submitted 11 May, 2022;
originally announced June 2022.
-
Hard Provability Logics
Authors:
Mojtaba Mojtahedi
Abstract:
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})$,…
▽ More
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})$.
△ Less
Submitted 11 November, 2019;
originally announced November 2019.
-
The $Σ_1$-Provability Logic of HA*
Authors:
Mohammad Ardeshir,
Mojtaba Mojtahedi
Abstract:
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}_σ^*$.
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}_σ^*$.
△ Less
Submitted 27 August, 2018; v1 submitted 12 May, 2018;
originally announced May 2018.
-
Localizing Finite-Depth Kripke Models
Authors:
Mojtaba Mojtahedi
Abstract:
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.…
▽ More
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} $.
△ Less
Submitted 24 October, 2017;
originally announced October 2017.
-
The $Σ$_1 Provability Logic of HA
Authors:
Mohammad Ardeshir,
S. Mojtaba Mojtahedi
Abstract:
In this paper we introduce a modal theory $H_σ$, which is sound and complete for arithmetical $Σ$_1 substitutions in ${\bf HA}$, in other words, we will show that $H_σ$ is the $Σ$_1-provability logic of ${\bf HA}$. Moreover we will show that $H_σ$ is decidable. As a by-product of these results, we show that ${\bf HA} + \Box\bot$ has de Jongh property.
In this paper we introduce a modal theory $H_σ$, which is sound and complete for arithmetical $Σ$_1 substitutions in ${\bf HA}$, in other words, we will show that $H_σ$ is the $Σ$_1-provability logic of ${\bf HA}$. Moreover we will show that $H_σ$ is decidable. As a by-product of these results, we show that ${\bf HA} + \Box\bot$ has de Jongh property.
△ Less
Submitted 2 November, 2017; v1 submitted 19 September, 2014;
originally announced September 2014.
