bluuebunny/crossref_metadata_2025_split huggingface dataset:
Intensional logic and two-sorted type theory
Authors: Zimmermann Thomas Ede 
Published: May 2006

Among the symbolic languages used most frequently in the indirect interpretation of natural language are Montague's Intensional Logic IL [5, 384ff.] and its extensional counterpart, the language Ty2 of two-sorted type theory. The question of which of these two formal languages is to be preferred has been obscured by lack of knowledge about the exact relation between them. The present paper is an attempt to clarify the situation by showing that, modulo a small, decidable class of formulas irrelevant to these applications, IL and Ty2 are equivalent in the strong sense that there exists a reversible translation between the terms of either language.In [3, 6Iff.] Gallin has shown that there exists a simple and natural translation * of IL into Ty2. Following Gallin's translation procedure, it is even possible to conceive of IL as a highly restricted sublanguage of Ty2, viz. as that part which only contains expressions of certain intensional types plus one variable of the basic type of indices or worlds. In an obvious sense, this sublanguage has less expressive power than the whole of Ty2, where it is possible to express conditions on entities that do not even exist in IL's ontology. However, by a certain amount of coding, one can translate Ty2 into IL [3, 105]. Conditions on nonintensional entities then become conditions on corresponding intensional objects; and these paraphrases preserve (standard) validity and entailment. On the other hand, this retranslation of Ty2 into IL is not an inversion of *, as can be seen from a simple example.
Classification and interpretation
Authors: Baudisch Andreas 
Published: May 2006

AbstractLet S and T be countable complete theories. We assume that T is superstable without the dimensional order property, and S is interpretable in T in such a way that every model of S is coded in a model of T. We show that S does not have the dimensional order property, and we discuss the question of whether Depth(S) ≤ Depth(T). For Mekler's uniform interpretation of arbitrary theories S of finite similarity type into suitable theories TS of groups we show that Depth(S) ≤ Depth(TS) ≤ 1 + Depth(S).
Plongement dense d'un corps ordonné dans sa clôture réelle
Authors: Delon Françoise 
Published: May 2006

AbstractWe study the structures (K ⊂ Kr), where K is an ordered field and Kr its real closure, in the language of ordered fields with an additional unary predicate for the subfield K. Two such structures (K ⊂ Kr) and (L ⊂ Lr) are not necessarily elementary equivalent when K and L are. But with some saturation assumption on K and L, then the two structures become equivalent, and we give a description of the complete theory.
Systems of illative combinatory logic complete for first-order propositional and predicate calculus
Authors: Barendregt Henk , Bunder Martin , Dekkers Wil 
Published: May 2006

AbstractIllative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the program of Church [1932], [1933] and Curry [1930] to base logic on a consistent system of λ-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent).
Arithmetic definability by formulas with two quantifiers
Authors: Tung Shih Ping 
Published: May 2006

AbstractWe give necessary conditions for a set to be definable by a formula with a universal quantifier and an existential quantifier over algebraic integer rings or algebraic number fields. From these necessary conditions we obtain some undefinability results. For example, N is not definable by such a formula over Z. This extends a previous result of R. M. Robinson.
Local behaviour of the Chebyshev theorem in models of I⊿0
Authors: Paola D'Aquino  
Published: May 2006

Let I⊿0 denote the fragment of Peano arithmetic where induction is restricted only to bounded formulas (⊿0-formulas), i.e. formulas where all the quantifiers are bounded. We will examine the behaviour in I⊿0 of Chebyshev's classical result on the distribution of primes. Chebyshev showed that each of the following functions on N is bounded by a polynomial in each of the others:In his proof he used, as auxiliaries, factorials and binomial coefficients.When we work in a weak system like I⊿0 we have to deal with two problems:(i) There is not an immediate meaning for symbols like xy, Πp≤xp, and x!.(ii) Some basic functions like exponentiation, factorial, and product of primes up to a certain element, are in general only partially definable.The first problem is equivalent to finding ⊿0-formulas representing the relations z = xy, y = Πp≤xp, and y = x!. While we can easily express that y is the product of all primes less than or equal to x in a ⊿0-way, it requires a subtle argument to define z = xy by a ⊿0-formula. The most natural way of expressing it is via the formalization of the Chinese remainder theorem coding the recursion procedure used in the definition of xy. But this can be expressed only via a Σ1-formula. ⊿0-definitions of exponentiation were given by Paris and Bennett (see [GD] and [B]), and all sensible definitions of this type are equivalent (see Remark 1). Later we will examine properties of such a definition E0(x, y, z). The ⊿00-definition of y = Πp≤xp is much more straightforward, since both the relation of being a prime and the divisibility relation are ⊿0-definable. We will give an explicit definition of it and denote it by Ψ(x, y). In this way, by a ⊿0-induction, we will be able to prove the uniqueness of the elements y and z satisfying Ψ(x, y) and E0(x, y, z), respectively.
An intuitionistic proof of Tychonoff's theorem
Authors: Coquand Thierry 
Published: May 2006

Tychonoff's theorem states that a product of compact spaces is compact. In [3], P. Johnstone presents a proof of Tychonoff's theorem in a “localic” framework. The surprise is that the point-free formulation of Tychonoff's theorem is provable without the axiom of choice, whereas in the usual formulation it is equivalent to the axiom of choice (see Kelley [5]).The proof given in [3], however, is classical and seems to use the replacement axiom of Zermelo-Fraenkel. The aim of this paper is to present what we believe to be a more direct proof, which is intuitionistic and can be proved using as primitive only the notion of inductive definition, as it is for instance presented in Martin-Löf [6]. One main point of the paper is to show that the theory of locales can be developed rather naturally in the framework of inductive definitions. We think that our arguments can be presented in the constructive set theory of Aczel [2].The paper is organized as follows. In §1 we show the argument in the case of a product of two spaces. This proof has a direct generalisation to the case of a product over a set with a decidable equality.§1. Product of two spaces. We first recall a possible definition of a point-free space (see Johnstone [3] or Vickers [10]). It is a poset (X, ≤), together with a meet operation ab, written multiplicatively, and, for each a ∈ X, a set Cov(a) of subsets of {x ∈ X ∣ x ≤ a}. We ask that if M ∈ Cov(a) and b ≤ a, then {bs ∈ s ∈ M} ∈ Cov(b). This property of Cov will be called the axiom of covering. The elements of Cov(u) are called basic covers of u ∈ X.
Definable types in -minimal theories
Authors: Marker David , Steinhorn Charles I. 
Published: May 2006

Let L be a first order language. If M is an L-structure, let LM be the expansion of L obtained by adding constants for the elements of M.Definition. A type is definable if and only if for any L-formula , there is an LM-formula so that for all iff M ⊨ dθ(¯). The formula dθ is called the definition of θ.Definable types play a central role in stability theory and have also proven useful in the study of models of arithmetic. We also remark that it is well known and easy to see that for M ≺ N, the property that every M-type realized in N is definable is equivalent to N being a conservative extension of M, whereDefinition. If M ≺ N, we say that N is a conservative extension of M if for any n and any LN -definable S ⊂ Nn, S ∩ Mn is LM-definable in M.Van den Dries [Dl] studied definable types over real closed fields and proved the following result.0.1 (van den Dries), (i) Every type over (R, +, -,0,1) is definable.(ii) Let F and K be real closed fields and F ⊂ K. Then, the following are equivalent:(a) Every element of K that is bounded in absolute value by an element of F is infinitely close (in the sense of F) to an element of F.(b) K is a conservative extension of F.
Fragile measurability
Authors: Hamkins Joel 
Published: May 2006

AbstractLaver [L] and others [G-S] have shown how to make the supercompactness or strongness of κ indestructible by a wide class of forcing notions. We show, alternatively, how to make these properties fragile. Specifically, we prove that it is relatively consistent that any forcing which preserves κ<κ and κ+, but not P(κ), destroys the measurability of κ, even if κ is initially supercompact, strong, or if I1(κ) holds. Obtained as an application of some general lifting theorems, this result is an “inner model” type of theorem proved instead by forcing.
A note on a result of Kunen and Pelletier
Authors: Barbanel Julius B. 
Published: May 2006

AbstractSuppose that U and U′ are normal ultrafilters associated with some supercompact cardinal. How may we compare U and U′? In what ways are they similar, and in what ways are they different? Partial answers are given in [1], [2], [3], [5], [6], and [7]. In this paper, we continue this study.In [6], Menas introduced a combinatorial principle χ(U) of normal ultrafilters U associated with supercompact cardinals, and showed that normal ultrafilters satisfying this property also satisfy a partition property. In [5], Kunen and Pelletier showed that this partition property for U does not imply χ(U). Using results from [3], we present a different method of finding such normal ultrafilters which satisfy the partition property but do not satisfy χ(U). Our method yields a large collection of such normal ultrafilters.
Combinatorics on large cardinals
Authors: Montenegro E. Carlos H. 
Published: May 2006

Our framework is ZFC, and we view cardinals as initial ordinals. Baumgartner ([Bal] and [Ba2]) studied properties of large cardinals by considering these properties as properties of normal ideals and not as properties of cardinals alone. In this paper we study these combinatorial properties by defining operations which take as input one or more ideals and give as output an ideal associated with a large cardinal property. We consider four operations T, P, S and C on ideals of a regular cardinal κ, and study the structure of the collection of subsets they give, and the relationships between them.The operation T is defined using combinatorial properties based on trees 〈X, <T〉 on subsets X ⊆ κ (where α <T β → α < β). Given an ideal I, consider the property *: “every tree on κ with every branching set in I has a branch of size κ” (where a branching set is a maximal set with the same set of <T-predecessors, and a chain is a maximal <T-linearly ordered set; for definitions see §2). Now consider the collection T(I) of all subsets of κ that do not satisfy * (see Definition 2.2 and the introduction to §5). The operation T provides us with the large cardinal property (whether κ ∈ T(I) or not) and it also provides us with the ideal associated with this large cardinal property (namely T(I)); in general, we obtain different notions depending on the ideal I.
Singular σ-dense trees
Authors: Landver Avner 
Published: May 2006

Let be the least cardinal θ such that MAθ fails, (i.e. MA) implies that is regular. Models for regular with are easy to get (see [Ku1]). Fremlin and Miller proved that cof() > ω [Fr, 41C(d)]. The question of whether it is consistent that be singular was solved, in the affirmative, by Kunen [Ku1]. Kunen used a (θ, θ) strong gap in (ω)/Fin, whose splitting partial order is c.c.c. He showed that if cof(θ) = ω1, and P is a c.c.c. partial order of cardinality < θ that may destroy the strong gap, then there exists another c.c.c. partial order Q, which does not destroy the strong gap, and such that ⊩Q “P is not c.c.c”. One then gets Kunen's model by iterating c.c.c. partial orders of cardinality < θ, without destroying the strong (θ, θ) gap. It is unknown whether it is consistent to have ω1 < cof() < .Clearly, there exists a c.c.c. partial order Q with ∣Q∣ = , such that (Q) = (see (1.1)). A partial order P is σ-centered iff P is the union of countably many centered subsets, where a subset A ⊆ P is centered iff p ≤ q. Clearly, a σ-centered partial order is c.c.c. Bell and Szymański proved that (σ-centered) is regular (see [Be] or [Fr, 14C], and [Fr, 21K] or [vD, 3.1(e)]). This implies that if P is a σ-centered partial order, and is singular, then (P) > . In particular, if is singular, then Q is not σ-centered and all c.c.c. partial orders of cardinality < have a Baire number (1.1) strictly greater than . It was suggested in [Ku1] to try and use Q(T) (1.2), where T is a tree with no ω1-branches, to get models with singular . It is well known that when T is such a tree, the forcing Q(T) is c.c.c. [BMR], ∣Q(T)∣ = ∣T∣, and if T is not special, then n(Q(T)) ≤ ∣T∣.
The continuum and first-order intuitionistic logic
Authors: van Dalen D. 
Published: May 2006

Ever since Cantor, we have known that the reals and the rationals are not isomorphic (as equality structures, i.e., sets). Logically speaking, however, they are not all that different; in first-order classical logic they are elementarily equivalent, since the theory of infinite sets is complete. The same holds for ℝ and ℚ as ordered sets; again the theory of dense linear order without end points is complete.From an intuitionistic point of view these matters are more complicated; e.g., the theory of equality of ℚ is decidable, whereas the one of ℝ patently is not. This, in a roundabout way, shows that ℚ and ℝ are not isomorphic; of course, there is no need for such a detour, as Cantor's original proof [2] is intuitionistically correct, and Brouwer's new proof [1] is another alternative intuitionistic argument.In view of the fact that ℚ and ℝ behave so strikingly differently with respect to first-order logic, one is easily tempted to look for elementary equivalences among the subsets of ℝ. Until quite recently most model theoretic investigations of intuitionistic theories made use of special (artificial) notions of “model”, e.g., Kripke models, sheaf models,…; but there is no prima facie reason why one should not practice model theory much the same way as traditional model theorists do. That is to say on the basis of a naive set theory, or, in our case, of naive intuitionistic mathematics.This paper uses the method of (k, p)-isomorphisms of Fraïssé, and it is briefly shown that one half of the Fraïssé theorem holds intuitionistically.
Questions of decidability and undecidability in Number Theory
Authors: Mazur B. 
Published: May 2006

Davis, Matijasevic, and Robinson, in their admirable survey article [D-M-R], interpret the negative solution of Hilbert's Tenth Problem as a resounding positive statement about the versatility of Diophantine equations (that any listable set can be coded as the set of parameter values for which a suitable polynomial possesses integral solutions).One can also view the Matijasevic result as implying that there are families of Diophantine equations parametrized by a variable t, which have integral solutions for some integral values t = a > 0, and yet there is no computable function of t which provides an upper bound for the smallest integral solution for these values a. The smallest integral solutions of the Diophantine equation for these values are, at least sporadically, too large to be bounded by any computable function. This is somewhat difficult to visualize, since there is quite an array of computable functions. But let us take an explicit example. Consider the functionMatijasevic's result guarantees the existence of parametrized families of Diophantine equations such that even this function fails to yield an upper bound for its smallest integral solutions (for all values of the parameter t for which there are integral solutions).Families of Diophantine equations in a parameter t, whose integral solutions for t = 1, 2, 3,… exhibit a certain arythmia in terms of their size, have fascinated mathematicians for centuries, and this phenomenon (the size of smallest integral solution varying wildly with the parameter-value) is surprising, even when the equations are perfectly “decidable”.
A structure theorem for semibounded sets in the reals
Authors: Peterzil Ya'acov 
Published: May 2006

In [MPP] it was shown that in every reduct of = ‹ ℝ, +, ·, <› that properly expands ℳ = ‹ℝ, +, <, λa›a∈ℝ, all the bounded semi-algebraic (that is, -definable) sets are definable. Said differently, every such is an expansion of = ‹ℝ, +, <, λa, Bi›a∈ℝ, i∈I where {Bi}i∈I is the collection of all bounded semialgebraic sets and the λa's are scalar multiplication by a. In [PSS] (see Theorem 1.2 below) it was shown that the structure is a proper reduct of ; that is, one cannot define in it all the semialgebraic sets. In [Pe] we show that is the only reduct properly between ℳ and . As a first step towards this result, we investigate in this paper the definable sets in reducts such as . (We point out that ‘definable’ will always mean ‘definable with parameters’.)Definition 1.1. Let X ⊆ ℝn. X is called semi-bounded if it is definable in the structure ‹ℝ, +, <, λa, B1, …, Bk›a∈ℝ, where the Bi's are bounded subsets of ℝn.The main result of this paper (see Theorem 3.1) shows roughly that, in Ominimal expansions of that satisfy the partition condition (see Definition 2.3), every semibounded set can be partitioned into finitely many sets, each of which is of a form similar to a cylinder. Namely, these sets are obtained through the “stretching” of a bounded cell by finitely many linear vectors. As a corollary (see Theorem 1.4), we get different characterizations of semibounded sets, either in terms of their structure or in terms of their definability power.The following result, by A. Pillay, P. Scowcroft and C. Steinhorn, was the main motivation for this paper. The theorem is formulated here in a slightly stronger form than originally, but the proof itself is essentially the original one. A short version of the proof is included in §4.
Whither relevant arithmetic?
Authors: Friedman Harvey , Meyer Robert K. 
Published: May 2006

AbstractBased on the relevant logic R, the system R#was proposed as a relevant Peano arithmetic. R#has many nice properties: the most conspicuous theorems of classical Peano arithmetic PA are readily provable therein; it is readily and effectively shown to be nontrivial; it incorporates both intuitionist and classical proof methods. But it is shown here that R#is properly weaker than PA, in the sense that there is a strictly positive theorem QRF of PA which is unprovable in R#. The reason is interesting: if PA is slightly weakened to a subtheory P+, it admits the complex ring C as a model; thus QRF is chosen to be a theorem of PA but false in C. Inasmuch as all strictly positive theorems of R#are already theorems of P+, this nonconservativity result shows that QRF is also a nontheorem of R#. As a consequence, Ackermann's rule γ is inadmissible in R#. Accordingly, an extension of R#which retains its good features is desired. The system R##, got by adding an omega-rule, is such an extension. Central question: is there an effectively axiomatizable system intermediate between R#and R#, which does formalize arithmetic on relevant principles, but also admits γ in a natural way?
Non-finite-axiomatizability results in algebraic logic
Authors: Biró Balázs 
Published: May 2006

This paper deals with relation, cylindric and polyadic equality algebras. First of all it addresses a problem of B. Jónsson. He asked whether relation set algebras can be expanded by finitely many new operations in a “reasonable” way so that the class of these expansions would possess a finite equational base. The present paper gives a negative answer to this problem: Our main theorem states that whenever Rs+ is a class that consists of expansions of relation set algebras such that each operation of Rs+ is logical in Jónsson's sense, i.e., is the algebraic counterpart of some (derived) connective of first-order logic, then the equational theory of Rs+ has no finite axiom systems. Similar results are stated for the other classes mentioned above. As a corollary to this theorem we can solve a problem of Tarski and Givant [87], Namely, we claim that the valid formulas of certain languages cannot be axiomatized by a finite set of logical axiom schemes. At the same time we give a negative solution for a version of a problem of Henkin and Monk [74] (cf. also Monk [70] and Németi [89]).Throughout we use the terminology, notation and results of Henkin, Monk, Tarski [71] and [85]. We also use results of Maddux [89a].Notation. RA denotes the class of relation algebras, Rs denotes the class of relation set algebras and RRA is the class of representable relation algebras, i.e. the class of subdirect products of relation set algebras. The symbols RA, Rs and RRA abbreviate also the expressions relation algebra, relation set algebra and representable relation algebra, respectively.For any class C of similar algebras EqC is the set of identities that hold in C, while Eq1C is the set of those identities in EqC that contain at most one variable symbol. (We note that Henkin et al. [85] uses the symbol EqC in another sense.)
Elementary embedding between countable Boolean algebras
Authors: Bonnet Robert , Rubin Matatyahu 
Published: May 2006

AbstractFor a complete theory of Boolean algebras T, let MT denote the class of countable models of T. For B1, B2 ∈ MT, let B1 ≤ B2 mean that B2 is elementarily embeddable in B2. Theorem 1. For every complete theory of Boolean algebras T, if T ≠ Tω, then ‹MT, ≤› is well-quasi-ordered. ∎ We define Tω. For a Boolean algebra B, let I(B) be the ideal of all elements of the form a + s such that B ↾ a is an atomic Boolean algebra and B ↾ s is an atomless Boolean algebra. The Tarski derivative of B is defined as follows: B(0) = B and B(n + 1) = B(n)/I(B(n)). Define Tω to be the theory of all Boolean algebras such that for every n ∈ ω, B(n) ≠ {0}. By Tarski [1949], Tω is complete. Recall that ‹A, < › is partial well-quasi-ordering, it is a partial quasi-ordering and for every {ai, ⃒ i ∈ ω} ⊆ A, there are i < j < ω such that ai ≤ aj. Theorem 2. contains a subset M such that the partial orderings ‹M, ≤ ↾ M› and are isomorphic. ∎ Let M′0 denote the class of all countable Boolean algebras. For B1, B2 ∈ M′0, let B1 ≤′ B2 mean that B1 is embeddable in B2. Remark. ‹M′0, ≤′› is well-quasi-ordered. ∎ This follows from Laver's theorem [1971] that the class of countable linear orderings with the embeddability relation is well-quasi-ordered and the fact that every countable Boolean algebra is isomorphic to a Boolean algebra of a linear ordering.
The consistency of one fixed omega
Authors: Henle J. M. 
Published: May 2006

AbstractThe paper “Partitions of Products” [DiPH] investigated the polarized partition relationThe relation is consistent relative to an inaccessible cardinal if every αi is finite, but inconsistent if two are infinite. We show here that it consistent (relative to an inaccessible) for one to be infinite.Along the way, we prove an interesting proposition from ZFC concerning partitions of the finite subsets of ω.