Independence results for weak systems of intuitionistic arithmetic

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Σ₂. We prove i?₁ ? i?₁, i?₁ ? i?₁, iΠ₂ ? iΣ₂ and iΣ₂ ? iΠ₂. We use Smorynski's operation Σ′ to show HA ? lΠ₁.     

Submodels of Kripke models

A Kripke model ? is a submodel of another Kripke model ℳ if ? is obtained by restricting the set of nodes of ℳ. In this paper we show that the class of formulas of Intuitionistic Predicate Logic that is preserved under taking submodels of Kripke models is precisely the class of semipositive formulas. This result is an analogue of the Łoś-Tarski theorem for the Classical Predicate Calculus. In Appendix A we prove that for theories with decidable identity we can take as the embeddings between domains in Kripke models of the theory, the identical embeddings. This is a well known fact, but we know of no correct proof in the literature. In Appendix B we answer, negatively, a question posed by Sam Buss: whether there is a classical theory T, such that ℋT is HA. Here ℋT is the theory of all Kripke models ℳ such that the structures assigned to the nodes of ℳ all satisfy T in the sense of classical model theory. Received: 4 February 1999 / Published online: 25 January 2001     

Weak Arithmetics and Kripke Models

In the first section of this paper we show that i Π₁ ≡ W⌝⌝lΠ₁ and that a Kripke model which decides bounded formulas forces iΠ₁ if and only if the union of the worlds in any (complete) path in it satisflies IΠ₁. In particular, the union of the worlds in any path of a Kripke model of HA models IΠ₁. 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 Δ₀‐formulas it is necessary and sufficient that the model be Σ_m‐elementary. This implies that if a linear Kripke model forces PEM_prenex, 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.     

Preservation theorems for Kripke models

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)     

A note on effective ultrapowers: Uniform failure of bounded collection

By suitably adapting an argument of Hirschfeld (see [2, Chapter 9]), we show that there is a single Δ₁ formula that defeats “bounded collection” for any model of II₂ Arithmetic that is either a recursive ultrapower or an existentially complete model. Some related facts are noted. MSC: 03F30, 03C62.     

Kripke submodels and universal sentences

We define two notions for intuitionistic predicate logic: that of a submodel of a Kripke model, and that of a universal sentence. We then prove a corresponding preservation theorem. If a Kripke model is viewed as a functor from a small category to the category of all classical models with (homo)morphisms between them, then we define a submodel of a Kripke model to be a restriction of the original Kripke model to a subcategory of its domain, where every node in the subcategory is mapped to a classical submodel of the corresponding classical model in the range of the original Kripke model. We call a sentence universal if it is built inductively from atoms (including ? and ⊥) using ∧, ∨, ?, and →, with the restriction that antecedents of → must be atomic. We prove that an intuitionistic theory is axiomatized by universal sentences if and only if it is preserved under Kripke submodels. We also prove the following analogue of a classical model‐consistency theorem: The universal fragment of a theory Γ is contained in the universal fragment of a theory Δ if and only if every rooted Kripke model of Δ is strongly equivalent to a submodel of a rooted Kripke model of Γ. Our notions of Kripke submodel and universal sentence are natural in the sense that in the presence of the rule of excluded middle, they collapse to the classical notions of submodel and universal sentence. (© 2007 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

On Models Constructed by Means of the Arithmetized Completeness Theorem

In this paper we study the model theory of extensions of models of first‐order Peano Arithmetic (PA) by means of the arithmetized completeness theorem (ACT) applied to a definable complete extension of PA in the original model. This leads us to many interesting model theoretic properties equivalent to reflection principles and ω‐consistency, and these properties together with the associated first‐order schemes extending PA are studied.     

Distinguished Completion of a Direct Product of Lattice Ordered Groups

The distinguished completion E(G) of a lattice ordered group G was investigated by Ball [1], [2], [3]. An analogous notion for MV-algebras was dealt with by the author [7]. In the present paper we prove that if a lattice ordered group G is a direct product of lattice ordered groups G _i (i I), then E(G) is a direct product of the lattice ordered groups E(G _i). From this we obtain a generalization of a result of Ball [3].     

Forking and Incomplete Types

Let Δ be a set of formulas. In this paper we study the following question: under what assumptions on Δ, the concept “a complete Δ-type p over B does not fork over A ? B” behaves well. We apply the results to the structure theory of ω₁-saturated models. Mathematics Subject Classification: 03C45.     

Derived sequences and reverse mathematics

One of the earliest applications of transfinite numbers is in the construction of derived sequences by Cantor [2]. In [6], the existence of derived sequences for countable closed sets is proved in ATR₀. This existence theorem is an intermediate step in a proof that a statement concerning topological comparability is equivalent to ATR₀. In actuality, the full strength of ATR₀ is used in proving the existence theorem. To show this, we will derive a statement known to be equivalent to ATR₀, using only RCA₀ and the assertion that every countable closed set has a derived sequence. We will use three of the subsystems of second order arithmetic defined by H. Friedman ([3], [4]), which can be roughly characterized by the strength of their set comprehension axioms. RCA₀ includes comprehension for Δ definable sets, ACA₀ includes comprehension for arithmetical sets, and ATR₀ appends to ACA₀ a comprehension scheme for sets defined by transfinite recursion on arithmetical formulas. MSC: 03F35, 54B99.     

A note on a theorem of Kanovei

We give a short proof of a theorem of Kanovei on separating induction and collection schemes for _n formulas using families of subsets of countable models of arithmetic coded in elementary end extensions.Mathematics Subject Classification (2000): 03C62     

On the Twistor Spaces of Almost Hermitian Manifolds

We study Grassmannian bundles G_k(M) of analytical 2k-planes over an almost Hermitian manifold M²ⁿ, from the point of view of the generalized twistor spaces of [13], and with the method of the moving frame [9]. G₁(M⁴) is the classical twistor space. We find four distinguished almost Hermitian structures, one of them being that of [13], and discuss their integrability and Kählerianity. For n=2, we compute the corresponding Hermitian connections, and derive consequences about the corresponding first Chern classes.     

A proof of the montague-plemmons-schein theorem on maximal subgroups of the semigroup of binary relations

The theorem in question is that the group of automorphisms of a partially ordered set (X,π), π denoting the order relation on the set X, is isomorphic to the maximal subgroup of ℬ_x containing π, where ℬ_x is the semigroup of all binary relations on X. This theorem is due to Montague and Plemmons [1] for the case X finite or countably infinite, and was extended by Schein to the general case, using a theorem due to Zaretsky [4]. A proof of the general case, based on [1] and results due to Plemmons and West [3], is also given in the preceding note by Plemmons and Schein [2]. The purpose of this note is to give an entirely self-contained proof of this intersesting theorem.     

Modal positive operators

For every modal positive operator, there exists a formula defining a least fixed point for that operator in partially ordered Kripke models with the property of being cofinal for every infinite ascending chain. A similar result obtains also for strict partially ordered Kripke models with the same property. Supported by the Russian Humanitarian Science Foundation (RHSF), grant No. 97-03-04089, and by the Siberian Branch of the Russian Academy of Science through PSO RAN No. 473, grant No. 3. Translated fromAlgebra i Logika, Vol. 38, No. 5, pp. 585–597, September–October, 1999.     

Fragments of Arithmetic and true sentences

By a theorem of R. Kaye, J. Paris and C. Dimitracopoulos, the class of the Π_n+1‐sentences true in the standard model is the only (up to deductive equivalence) consistent Π_n+1‐theory which extends the scheme of induction for parameter free Π_n+1‐formulas. Motivated by this result, we present a systematic study of extensions of bounded quantifier complexity of fragments of first‐order Peano Arithmetic. Here, we improve that result and show that this property describes a general phenomenon valid for parameter free schemes. As a consequence, we obtain results on the quantifier complexity, (non)finite axiomatizability and relative strength of schemes for Δ_n+1‐formulas. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Even permutations and oriented sets: their shifted asymmetry index series

The present authors introduced recently (see [Adv. in Appl. Math. 32 (2004) 576]) the notion of shifted asymmetry index series denoted Γ_F,ξ, for an arbitrary species of structures, F, and a series of weights, ξ. This series generalizes the classical asymmetry index series, Γ_F, of G. Labelle [Discrete Math. 99 (1992) 141] to take into account the substitution of species with non-zero constant term [Combinatoire Énumérative, Lecture Notes in Math., vol. 1234, Springer-Verlag, 1986, pp. 126–159]. In [Adv. in Appl. Math. 32 (2004) 576], we can find explicit formulas for the shifted asymmetry index series of usual species (sets, cycles, permutation, trees, …). The goal of this paper is to complement [Adv. in Appl. Math. 32 (2004) 576] by computing closed formulas for the series Γ_E^±,ξ and Γ_ALT,ξ, of the species E^± of oriented sets and ALT of even permutation of their elements. Oriented sets are, by definition, totally ordered sets modulo an even permutation of their elements. Such structures were used, for example, by Pólya and Read [Combinatorial Enumeration of Groups, Graphs and Chemical Compounds, Springer-Verlag, 1987] in the context of combinatorial chemistry problems (vertex-sets of oriented simplices).     

The logical consequence relation of propositional tense logic

This work concerns the model theory of propositional tense logic with the Kripke relational semantics. It is shown (i) that there is a formula y whose logical consequences form a complete II set, and (ii) that for 0 ≦ m < ω+ ω there are formulas γ_m such that all models of γ_m are isomorphic and have cardinality x_m, where x₀ = χ₀, x_m+1 = 2^xm, and x_ω = lim{x_m < | m ω}. Familiarity with the relational semantics for modal and tense logic ([1] or [3], for example) will be presumed. A knowledge of recursion theory would be helpful, although some background material will be provided.     

Properties of Tense Logics

Based on the results of [11] this paper delivers uniform algorithms for deciding whether a finitely axiomatizable tense logic

• has the finite model property,
• is complete with respect to Kripke semantics,
• is strongly complete with respect to Kripke semantics,
• is d-persistent,
• is r-persistent.

It is also proved that a tense logic is strongly complete iff the corresponding variety of bimodal algebras is complex, and that a tense logic is d-persistent iff it is complete and its Kripke frames form a first order definable class. From this we obtain many natural non-d-persistent tense logics whose corresponding varieties of bimodal algebras are complex. Mathematics Subject Classification: 03B45, 03B25.     

Fixed point results for multivalued contractions on ordered gauge spaces

The purpose of this article is to present fixed point results for multivalued E _≤-contractions on ordered complete gauge space. Our theorems generalize and extend some recent results given in M. Frigon [7], S. Reich [12], I.A. Rus and A. Petruşel [15] and I.A. Rus et al. [16].