Areas of Specialization
Areas of Interest
•  4
##### An infinitary axiomatization of dynamic topological logic with Somayeh Chopoghloo Logic Journal of the IGPL. forthcoming.
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 str…Read more
•  68
##### Type Theoretic Interpretation of Theories and Syntax-Semantics Debate in Philosophy of Science
In 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.
•  4
##### Forcing and satisfaction in Kripke models of intuitionistic arithmetic with Maryam Abiri and Mostafa Zaare Logic Journal of the IGPL 27 (5): 659-670. 2019.
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 f…Read more
•  20
•  56
##### Some weak fragments of {${\rm HA}$} and certain closure properties with Mojtaba Moniri Journal of Symbolic Logic 67 (1): 91-103. 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
•  22
##### Preservation theorems for Kripke models with Mostafa Zaare Mathematical Logic Quarterly 55 (2): 177-184. 2009.
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 th…Read more
•  54
##### Weak Arithmetics and Kripke Models Mathematical Logic Quarterly 48 (1): 157-160. 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 Πm-formulas in a linear Kripke model deciding Δ0-formulas it is necessary and sufficient that the model be Σm-elemen…Read more
•  40
##### Intuitionistic weak arithmetic Archive for Mathematical Logic 42 (8): 791-796. 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
•  18
##### Provably recursive functions of constructive and relatively constructive theories Archive for Mathematical Logic 49 (3): 291-300. 2010.
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 b…Read more
•  42
##### Some results on Kripke models over an arbitrary fixed frame with Seyed Mohammad Bagheri Mathematical Logic Quarterly 49 (5): 479-484. 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ö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
•  24
##### On two questions about feasibly constructive arithmetic Mathematical Logic Quarterly 49 (4): 425. 2003.
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
•  7
##### Corrigendum to“Weak Arithmetics and Kripke Models” Mathematical Logic Quarterly 50 (6): 637-638. 2004.
We give a corrected proof of the main result in the paper [2] mentioned in the title.
•  36
##### Preservation theorems for bounded formulas Archive for Mathematical Logic 46 (1): 9-14. 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
•  18
##### Independence results for weak systems of intuitionistic arithmetic Mathematical 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 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…Read more
•  24
•  23
##### Corrigendum 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
•  21
##### Homomorphisms and chains of Kripke models with Mostafa Zaare Archive for Mathematical Logic 50 (3-4): 431-443. 2011.
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 …Read more
•  16
##### Polynomial induction and length minimization in intuitionistic bounded arithmetic Mathematical Logic Quarterly 51 (1): 73-76. 2005.
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
•  19