
4An infinitary axiomatization of dynamic topological logicLogic Journal of the IGPL. forthcoming.Dynamic topological logic is a multimodal 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 trimodal language has been open for more than one decade. In this paper, we give a natural axiomatization of $\textsf{DTL}$ and prove its str…Read more

68In this paper we discuss some proposed ways for defining the notions of structure and isomorphism between structures in the absence of formal language. We discuss Halvorson’s arguments against the semantic view conception of the notion of structure and Glymour and Lutz’s criticisms on Halvorson’s view. We suggest a new look at structures suggested by homotopy type theory (HoTT). This approach is consistent with both the syntactic and the semantic view in the philosophy of science.

4Forcing and satisfaction in Kripke models of intuitionistic arithmeticLogic Journal of the IGPL 27 (5): 659670. 2019.We define a class of firstorder 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 f…Read more

20Regular cuts in models of bounded arithmeticBulletin of the Section of Logic 42 (1/2): 1120. 2013.

56Some weak fragments of {${\rm HA}$} and certain closure propertiesJournal of Symbolic Logic 67 (1): 91103. 2002.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 o…Read more

91ℋtheories, fragments of HA and PA normalityArchive for Mathematical Logic 41 (1): 101105. 2002.

22Preservation theorems for Kripke modelsMathematical Logic Quarterly 55 (2): 177184. 2009.There are several ways for defining the notion submodel for Kripke models of intuitionistic firstorder 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 th…Read more

54Weak Arithmetics and Kripke ModelsMathematical Logic Quarterly 48 (1): 157160. 2002.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 Πmformulas in a linear Kripke model deciding Δ0formulas it is necessary and sufficient that the model be Σmelemen…Read more

40Intuitionistic weak arithmeticArchive for Mathematical Logic 42 (8): 791796. 2003.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

18Provably recursive functions of constructive and relatively constructive theoriesArchive for Mathematical Logic 49 (3): 291300. 2010.In this paper we prove conservation theorems for theories of classical firstorder 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 BussHarnik’s theories of intuitionistic bounded arithmetic are the intuitionistic theories we consider. For the first group, we use a method described b…Read more

42Some results on Kripke models over an arbitrary fixed frameMathematical Logic Quarterly 49 (5): 479484. 2003.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öwenheimSkolem'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

24On two questions about feasibly constructive arithmeticMathematical Logic Quarterly 49 (4): 425. 2003.IPV is the intuitionistic theory axiomatized by Cook's equational theory PV plus PIND on NPformulas. 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

7Corrigendum to“Weak Arithmetics and Kripke Models”Mathematical Logic Quarterly 50 (6): 637638. 2004.We give a corrected proof of the main result in the paper [2] mentioned in the title.

36Preservation theorems for bounded formulasArchive for Mathematical Logic 46 (1): 914. 2007.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 polyn…Read more

18Independence results for weak systems of intuitionistic arithmeticMathematical Logic Quarterly 49 (3): 250. 2003.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 twonode PAnormal 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…Read more

24Neighborhood Semantics for Basic and Intuitionistic LogicLogic and Logical Philosophy 24 (3). 2015.

23Corrigendum to "Weak Arithmetics and Kripke Models"Mathematical Logic Quarterly 50 (6): 637. 2004.We give a corrected proof of the main result in the paper [2] mentioned in the title

21Homomorphisms and chains of Kripke modelsArchive for Mathematical Logic 50 (34): 431443. 2011.In this paper we define a suitable version of the notion of homomorphism for Kripke models of intuitionistic firstorder 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 …Read more

16Polynomial induction and length minimization in intuitionistic bounded arithmeticMathematical Logic Quarterly 51 (1): 7376. 2005.It is shown that the feasibly constructive arithmetic theory IPV does not prove LMIN, unless the polynomial hierarchy CPVprovably 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

19From forcing to satisfaction in Kripke models of intuitionistic predicate logicLogic Journal of the IGPL 26 (5): 464474. 2018.
Areas of Specialization
Science, Logic, and Mathematics 
Areas of Interest
Philosophy of Mathematics 