18 found
Order:
See also
  1.  19
    From Forcing to Satisfaction in Kripke Models of Intuitionistic Predicate Logic.Maryam Abiri, Morteza Moniri & Mostafa Zaare - 2018 - Logic Journal of the IGPL 26 (5):464-474.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  2.  22
    Neighborhood Semantics for Basic and Intuitionistic Logic.Morteza Moniri & Fatemeh Shirmohammadzadeh Maleki - 2015 - Logic and Logical Philosophy 24 (3).
  3.  38
    Some Results on Kripke Models Over an Arbitrary Fixed Frame.Seyed Mohammad Bagheri & Morteza Moniri - 2003 - Mathematical Logic Quarterly 49 (5):479-484.
    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.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  4.  22
    Preservation Theorems for Kripke Models.Morteza Moniri & Mostafa Zaare - 2009 - Mathematical Logic Quarterly 55 (2):177-184.
    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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  5.  81
    ℋ-Theories, Fragments of HA and PA -Normality.Morteza Moniri - 2002 - Archive for Mathematical Logic 41 (1):101-105.
  6.  16
    Independence Results for Weak Systems of Intuitionistic Arithmetic.Morteza Moniri - 2003 - Mathematical Logic Quarterly 49 (3):250.
    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 ⊬ (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  21
    On Two Questions About Feasibly Constructive Arithmetic.Morteza Moniri - 2003 - Mathematical Logic Quarterly 49 (4):425.
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  8.  12
    Polynomial Induction and Length Minimization in Intuitionistic Bounded Arithmetic.Morteza Moniri - 2005 - Mathematical Logic Quarterly 51 (1):73-76.
    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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  9.  39
    Intuitionistic Weak Arithmetic.Morteza Moniri - 2003 - Archive for Mathematical Logic 42 (8):791-796.
    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.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  10.  45
    Weak Arithmetics and Kripke Models.Morteza Moniri - 2002 - Mathematical Logic Quarterly 48 (1):157-160.
    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 (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  11.  35
    Preservation Theorems for Bounded Formulas.Morteza Moniri - 2007 - Archive for Mathematical Logic 46 (1):9-14.
    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 (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  12.  4
    Forcing and Satisfaction in Kripke Models of Intuitionistic Arithmetic.Maryam Abiri, Morteza Moniri & Mostafa Zaare - 2019 - Logic Journal of the IGPL 27 (5):659-670.
    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. (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  13.  19
    Corrigendum to "Weak Arithmetics and Kripke Models".Morteza Moniri - 2004 - Mathematical Logic Quarterly 50 (6):637.
    We give a corrected proof of the main result in the paper [2] mentioned in the title.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  14.  19
    Regular Cuts in Models of Bounded Arithmetic.Morteza Moniri & S. Hosein Sajjadi - 2013 - Bulletin of the Section of Logic 42 (1/2):11-20.
    Direct download  
     
    Export citation  
     
    Bookmark  
  15.  17
    Homomorphisms and Chains of Kripke Models.Morteza Moniri & Mostafa Zaare - 2011 - Archive for Mathematical Logic 50 (3-4):431-443.
    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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  16.  17
    Provably Recursive Functions of Constructive and Relatively Constructive Theories.Morteza Moniri - 2010 - Archive for Mathematical Logic 49 (3):291-300.
    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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  17.  7
    Corrigendum to“Weak Arithmetics and Kripke Models”.Morteza Moniri - 2004 - Mathematical Logic Quarterly 50 (6):637-638.
    We give a corrected proof of the main result in the paper [2] mentioned in the title.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  18.  52
    Some Weak Fragments of {${\Rm HA}$} and Certain Closure Properties.Morteza Moniri & Mojtaba Moniri - 2002 - Journal of Symbolic Logic 67 (1):91-103.
    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 (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   1 citation