We study the relations of being substructure and elementary substructure between Kripke models of intuitionistic predicate logic with the same arbitrary frame. We prove analogues of Tarski's test and Löwenheim-Skolem's theorems as determined by our definitions. The relations between corresponding worlds of two Kripke models [MATHEMATICAL SCRIPT CAPITAL K] ⪯ [MATHEMATICAL SCRIPT CAPITAL K]′ are studied.

There are several ways for defining the notion submodel for Kripke models of intuitionistic first‐order logic. In our approach a Kripke model A is a submodel of a Kripke model B if they have the same frame and for each two corresponding worlds Aα and Bα of them, Aα is a subset of Bα and forcing of atomic formulas with parameters in the smaller one, in A and B, are the same. In this case, B is called an extension of (...) A. We characterize theories that are preserved under taking submodels and also those that are preserved under taking extensions as universal and existential theories, respectively. We also study the notion elementary submodel defined in the same style and give some results concerning this notion. In particular, we prove that the relation between each two corresponding worlds of finite Kripke models A ≤ B is elementary extension (in the classical sense) (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim). (shrink)

For a classical theory T, ℋ(T) denotes the intuitionistic theory of T-normal (i.e. locally T) Kripke structures. S. Buss has asked for a characterization of the theories in the range of ℋ and raised the particular question of whether HA is an ℋ-theory. We show that Ti∈ range(ℋ) iff Ti = ℋ(T). As a corollary, no fragment of HA extending iΠ1 belongs to the range of ℋ. A. Visser has already proved that HA is not in the range of H (...) by different methods. We provide more examples of theories not in the range of ℋ. We show PA-normality of once-branching Kripke models of HA + MP, where it is not known whether the same holds if MP is dropped. (shrink)

This paper proves some independence results for weak fragments of Heyting arithmetic by using Kripke models. We present a necessary condition for linear Kripke models of arithmetical theories which are closed under the negative translation and use it to show that the union of the worlds in any linear Kripke model of HA satisfies PA. We construct a two-node PA-normal Kripke structure which does not force iΣ2. We prove i∀1 ⊬ i∃1, i∃1 ⊬ i∀1, iΠ2 ⊬ iΣ2 and iΣ2 ⊬ (...) iΠ2. We use Smorynski's operation Σ′ to show HA ⊬ lΠ1. (shrink)

We show that Intuitionistic Open Induction iop is not closed under the rule DNS(∃ - 1 ). This is established by constructing a Kripke model of iop + $\neg L_y(2y > x)$ , where $L_y(2y > x)$ is universally quantified on x. On the other hand, we prove that iop is equivalent with the intuitionistic theory axiomatized by PA - plus the scheme of weak ¬¬LNP for open formulas, where universal quantification on the parameters precedes double negation. We also show (...) that for any open formula φ(y) having only y free, $(PA^-)^i \vdash L_y\varphi(y)$ . We observe that the theories iop, i∀ 1 and iΠ 1 are closed under Friedman's translation by negated formulas and so under VR and IP. We include some remarks on the classical worlds in Kripke models of iop. (shrink)

Ladyman and Presnell have recently argued that the Hole argument is naturally resolved when spacetime is represented within homotopy type theory rather than set theory. The core idea behind their proposal is that the argument does not confront us with any indeterminism, since the set-theoretically different representations of spacetime involved in the argument are homotopy type-theoretically identical. In this article, we will offer a new resolution based on ZFC set theory to the argument. It neither relies on a constructive-intuitionistic form (...) of mathematics, as used by Ladyman and Presnell, nor is foundationally problematic, such as the existing set-theoretic suggestions. (shrink)

In the first section of this paper we show that i Π1 ≡ W⌝⌝lΠ1 and that a Kripke model which decides bounded formulas forces iΠ1 if and only if the union of the worlds in any path in it satisflies IΠ1. In particular, the union of the worlds in any path of a Kripke model of HA models IΠ1. In the second section of the paper, we show that for equivalence of forcing and satisfaction of Πm-formulas in a linear Kripke (...) model deciding Δ0-formulas it is necessary and sufficient that the model be Σm-elementary. This implies that if a linear Kripke model forces PEMprenex, then it forces PEM. We also show that, for each n ≥ 1, iΦn does not prove ℋ(IΠn's are Burr's fragments of HA. (shrink)

In this paper, we study bounded versions of some model-theoretic notions and results. We apply these results to the context of models of bounded arithmetic theories as well as some related complexity questions. As an example, we show that if the theory \(\rm S_2 ^1(PV)\) has bounded model companion then \(\rm NP=coNP\). We also study bounded versions of some other related notions such as Stone topology.

We define a class of first-order formulas $\mathsf{P}^{\ast }$ which exactly contains formulas $\varphi$ such that satisfaction of $\varphi$ in any classical structure attached to a node of a Kripke model of intuitionistic predicate logic deciding atomic formulas implies its forcing in that node. We also define a class of $\mathsf{E}$-formulas with the property that their forcing coincides with their classical satisfiability in Kripke models which decide atomic formulas. We also prove that any formula with this property is an $\mathsf{E}$-formula. (...) Kripke models of intuitionistic arithmetical theories usually have this property. As a consequence, we prove a new conservativity result for Peano arithmetic over Heyting arithmetic. (shrink)

Dynamic topological logic is a multi-modal logic that was introduced for reasoning about dynamic topological systems, i.e. structures of the form $\langle{\mathfrak{X}, f}\rangle $, where $\mathfrak{X}$ is a topological space and $f$ is a continuous function on it. The problem of finding a complete and natural axiomatization for this logic in the original tri-modal language has been open for more than one decade. In this paper, we give a natural axiomatization of $\textsf{DTL}$ and prove its strong completeness with respect to (...) the class of all dynamic topological systems. Our proof system is infinitary in the sense that it contains an infinitary derivation rule with countably many premises and one conclusion. It should be remarked that $\textsf{DTL}$ is semantically non-compact, so no finitary proof system for this logic could be strongly complete. Moreover, we provide an infinitary axiomatic system for the logic ${\textsf{DTL}}_{\mathcal{A}}$, i.e. the $\textsf{DTL}$ of Alexandrov spaces, and show that it is strongly complete with respect to the class of all dynamical systems based on Alexandrov spaces. (shrink)

In this paper we first introduce a new neighbourhood semantics for propositional intuitionistic logic. We then naturally extend this semantics to first-order intuitionistic logic. We also study bisimulation between neighbourhood models and prove some of their basic properties for both propositional and first-order intuitionistic logic.

We give a corrected proof of the main result in the paper [2] mentioned in the title.

We give a corrected proof of the main result in the paper [2] mentioned in the title.

In this paper we define a suitable version of the notion of homomorphism for Kripke models of intuitionistic first-order logic and characterize theories that are preserved under images and also those that are preserved under inverse images of homomorphisms. Moreover, we define a notion of union of chain for Kripke models and define a class of formulas that is preserved in unions of chains. We also define similar classes of formulas and investigate their behavior in Kripke models. An application to (...) intuitionistic first-order arithmetic is also given. (shrink)

We construct ω-framed Kripke models of i∀1 and iΠ1 non of whose worlds satisfies ∀x∃y(x=2y∨x=2y+1) and ∀x,y∃zExp(x, y, z) respectively. This will enable us to show that i∀1 does not prove ¬¬∀x∃y(x=2y∨x=2y+1) and iΠ1 does not prove ¬¬∀x, y∃zExp(x, y, z). Therefore, i∀1⊬¬¬lop and iΠ1⊬¬¬iΣ1. We also prove that HA⊬lΣ1 and present some remarks about iΠ2.

IPV is the intuitionistic theory axiomatized by Cook's equational theory PV plus PIND on NP-formulas. Two extensions of IPV were introduced by Buss and by Cook and Urquhart by adding PIND for formulas of the form A ∨ B, respectively ¬¬A, where A is NP and x is not free in B. Cook and Urquhart posed the question of whether these extensions are proper. We show that in each of the two cases the extension is proper unless the polynomial hierarchy (...) collapses. (shrink)

It is shown that the feasibly constructive arithmetic theory IPV does not prove LMIN, unless the polynomial hierarchy CPV-provably collapses. It is proved that PV plus LMIN intuitionistically proves PIND. It is observed that PV + PIND does not intuitionistically prove NPB, a scheme which states that the extended Frege systems are not polynomially bounded.

In this paper we prove conservation theorems for theories of classical first-order arithmetic over their intuitionistic version. We also prove generalized conservation results for intuitionistic theories when certain weak forms of the principle of excluded middle are added to them. Members of two families of subsystems of Heyting arithmetic and Buss-Harnik’s theories of intuitionistic bounded arithmetic are the intuitionistic theories we consider. For the first group, we use a method described by Leivant based on the negative translation combined with a (...) variant of Friedman’s translation. For the second group, we use Avigad’s forcing method. (shrink)

In this paper we naturally define when a theory has bounded quantifier elimination, or is bounded model complete. We give several equivalent conditions for a theory to have each of these properties. These results provide simple proofs for some known results in the model theory of the bounded arithmetic theories like CPV and PV1. We use the mentioned results to obtain some independence results in the context of intuitionistic bounded arithmetic. We show that, if the intuitionistic theory of polynomial induction (...) on strict $\Pi_2^{b}$ formulas proves decidability of $\Sigma_1^b$ formulas, then P=NP. We also prove that, if the mentioned intuitionistic theory proves ${\rm LMIN}(\Sigma_{1}^{b})$ , then P=NP. (shrink)