bluuebunny/crossref_metadata_2025_split huggingface dataset:
A new version of Beth semantics for intuitionistic logic
Authors: Gabbay Dov M. 
Published: May 2006

We use the notation of Kripke's paper [1]. Let M = (G, K, R) be a tree structure and D a domain and η a Beth model on M. The truth conditions of the Beth semantics for ∨ and ∃ are (see [1]):(a) η (A ∨ B, H) = T iff for some B ⊆ K, B bars H and for each H′ ∈ B, either η(A, H′) = T or η(B, H′) = T.(b) η(∃xA(x), H) = T iff for some B ⊆ K, B bars H and for each H′ ∈ B there exists an a ∈ D such that η(A (a), H′) = T.Suppose we change the truth definition η to η* by replacing condition (b) by the condition (b*) (well known from the Kripke interpretation):Call this type of interpretation the new version of Beth semantics. We proveTheorem 1. Intuitionistic predicate logic is complete for the new version of the Beth semantics.Since Beth structures are of constant domains, and in the new version of Beth semantics the truth conditions for ∧, →, ∃, ∀, ¬ are the same as for the Kripke interpretation, we get:Corollary 2. The fragment without disjunction of the logic CD of constant domains (i.e. with the additional schema ∀x(A ∨ B(x))→ A ∨ ∀xB(x), x not free in A) equals the fragment without disjunction of intuitionistice logic.
α-decompositions of α-spaces
Authors: Fowler Northrup 
Published: May 2006

The concept of an α-space was introduced and studied by Dekker in [1] and [2] from which we take our terminology and notation. The reader is assumed to be familiar with their contents. In this paper we are interested in the following conjecture which appears in [2, p. 493]:(*) S ⊕ C = V and S ∥ C and V an α-space ⇒ both S and C are α-spaces.It can be simply rephrased as:(**) The two components of an α-decomposition of an α-space are both α-spaces.In either form it is relevant to the ideas of α-subspace and α-homomorphism. Dekker [2, T5] has established (*) in the case S (or C) is an isolic α-space. In this paper we will prove (*) in two specific cases, one of which is a generalization of Dekker's result.
The infinite injury priority method
Authors: Soare Robert I. 
Published: May 2006

One of the most important and distinctive tools in recursion theory has been the priority method whereby a recursively enumerable (r.e.) set A is constructed by stages to satisfy a sequence of conditions {Rn}n∈ω called requirements. If n < m, requirement Rn is given priority over Rm and action taken for Rm at some stage s may at a later stage t > s be undone for the sake of Rn thereby injuring Rm at stage t. The first priority method was invented by Friedberg [2] and Muchnik [11] to solve Post's problem and is characterized by the fact that each requirement is injured at most finitely often.Shoenfield [20, Lemma 1], and then independently Sacks [17] and Yates [25] invented a much more powerful method in which a requirement may be injured infinitely often, and the method was applied and refined by Sacks [15], [16], [17], [18], [19] and Yates [25], [26] to obtain many deep results on r.e. sets and their degrees. In spite of numerous simplifications and variations this infinite injury method has never been as well understood as the finite injury method because of its apparently greater complexity.The purpose of this paper is to reduce the Sacks method to two easily understood lemmas whose proofs are very similar to the finite injury case. Using these lemmas we can derive all the results of Sacks on r.e. degrees, and some by Yates and Robinson as well, in a manner accessible to the nonspecialist. The heart of the method is an ingenious observation of Lachlan [7] which is combined with a further simplification of our own.
A result concerning cardinalities of ultraproducts
Authors: Keisler H. Jerome , Prikry Karel 
Published: May 2006

The cardinality problem for ultraproducts is as follows: Given an ultrafilter over a set I and cardinals αi, i ∈ I, what is the cardinality of the ultraproduct ? Although many special results are known, several problems remain open (see [5] for a survey). For example, consider a uniform ultrafilter over a set I of power κ (uniform means that all elements of have power κ). It is open whether every countably incomplete has the property that, for all infinite α, the ultra-power has power ακ. However, it is shown in [4] that certain countably incomplete , namely the κ-regular , have this property.This paper is about another cardinality property of ultrafilters which was introduced by Eklof [1] to study ultraproducts of abelian groups. It is open whether every countably incomplete ultrafilter has the Eklof property. We shall show that certain countably incomplete ultrafilters, the κ-good ultrafilters, do have this property. The κ-good ultrafilters are important in model theory because they are exactly the ultrafilters such that every ultraproduct modulo is κ-saturated (see [5]).Let be an ultrafilter on a set I. Let αi, n, i ∈ I, n ∈ ω, be cardinals and αi, n, ≥ αi, m if n < m. Let.Then ρn are nonincreasing and therefore there is some m and ρ such that ρn = ρ if n ≥ m. We call ρ the eventual value (abbreviated ev val) of ρn.
A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property
Authors: Gabbay D. M. , De Jongh D. H. J. 
Published: May 2006

The intuitionistic propositional logic I has the following (disjunction) property.We are interested in extensions of the intuitionistic logic which are both decidable and have the disjunction property. Systems with the disjunction property are known, for example the Kreisel-Putnam system [1] which is I + (∼ϕ → (ψ ∨ α))→ ((∼ϕ→ψ) ∨ (∼ϕ→α)) and Scott's system I + ((∼ ∼ϕ→ϕ)→(ϕ ∨ ∼ϕ))→ (∼∼ϕ ∨ ∼ϕ). It was shown in [3c] that the first system has the finite-model property.In this note we shall construct a sequence of intermediate logics Dn with the following properties:These systems are presented both semantically and syntactically, using the remarkable correspondence between properties of partially ordered sets and axiom schemata of intuitionistic logic. This correspondence, apart from being interesting in itself (for giving geometric meaning to intuitionistic axioms), is also useful in giving independence proofs and obtaining proof theoretic results for intuitionistic systems (see for example, C. Smorynski, Thesis, University of Illinois, 1972, for independence and proof theoretic results in Heyting arithmetic).
Models for recursion theory
Authors: Moldestad Johan , Normann Dag 
Published: May 2006

Several results in the theory of recursion in higher types indicate that the effect of a higher type functional on the lower types does not reflect the high type, i.e. the same effect could be obtained by functionals of relatively low type. The two main results here are:Plus -1 - Theorem (G. Sacks [6] for k = 1, [7] for k > 1). Let H be a normal functional of type ≥ k + 1. Then there exists a normal functional F of type k + 1 such that k-sc(F) = k-sc(H), i.e. the same subsets of tp(k − 1) are recursive in F and H.Plus - 2 - Theorem (L. Harrington [1]). Let H be a normal functional of type ≥ k + 2. Then there exists a normal functional F of type k +2 such that k-en(H) = k-en(F), i.e. the same subsets of tp(k − 1) are semirecursive in F and H.The results in this paper also indicate that higher types cannot have too much influence on lower types. The key is the Skolem-Löwenheim theorem. Among the results we mention:(1) Let n < m. A ⊆ tp(n) × tp(m) be Kleene-semicomputable. Let x ∈ B ⇔ ∀y∈tp(m), ⟨x, y⟩ ∈ A. Then B is . This result may be relativized to a functional of type n + 1.(2) Let k0 be the type-k-functional that is constant zero. Let F be a functional of type < k. Then, for i ≤ k −2, i-sc(F ,k0) = i-sc(F), i-en(F, k0) = ∀tp(i)(i-en(F)).
Zermelo-Fraenkel consistency results by Fraenkel-Mostowski methods
Authors: Pincus David 
Published: May 2006

Fraenkel-Mostowski models are a particularly simple and conceptual tool for proving consistency results involving the axiom of choice, AC. These models satisfy the theory, FM, of a well founded universe of sets built from a ground set of individuals. Zermelo-Fraenkel set theory, ZF, is the extension of FM in which the set of individuals is assumed to be empty. In this paper we show that there is a large class of statements whose consistency with ZF can be proven directly by means of a Fraenkel-Mostowski model.A statement, Φ, of set theory is said to be transferable if there is a metatheorem: If Φ is true in a Fraenkel-Mostowski model then Φ is consistent with ZF. Jech and Sochor introduced, in [12], the class of boundable statements and proved them to be transferable. Most existential contradictions of AC are boundable. It remains to find criteria under which Ψ ∧ Φ is transferable where Ψ is a universal consequence of AC and Φ is an existential contradiction of AC. To this end we give two classes of statements. Each class is closed under conjunction, contains the boundable statements, and contains a number of universal consequences of AC. Nearly every Fraenkel-Mostowski consistency in the literature falls into one of these two classes.In §2 we give two generalizations of the boundable statements. In §§3 and 4 the classes of transferable statements are discussed. In §5 we discuss the transfer problem and prove a metatheorem concerning nontransferable statements.
On n-quantifier induction
Authors: Parsons Charles 
Published: May 2006

In this paper we discuss subsystems of number theory based on restrictions on induction in terms of quantifiers, and we show that all the natural formulations of ‘n-quantifier induction’ are reducible to one of two (for n ≠ 0) nonequivalent normal forms: the axiom of induction restricted to (or, equivalently, ) formulae and the rule of induction restricted to formulae.Let Z0 be classical elementary number theory with a symbol and defining equations for each Kalmar elementary function, and the rule of inductionrestricted to quantifier-free formulae. Given the schemalet IAn be the restriction of IA to formulae of Z0 with ≤n nested quantifiers, IAn′ to formulae with ≤n nested quantifiers, disregarding bounded quantifiers, the restriction to formulae, the restriction to , formulae. IRn, IRn′, , are analogous.Then, we show that, for every n, , , IAn, and IAn′, are all equivalent modulo Z0. The corresponding statement does not hold for IR. We show that, if n ≠ 0, is reducible to ; evidently IRn is reducible to . On the other hand, IRn′ is obviously equivalent to IAn′ [10, Lemma 2].
Major subspaces of recursively enumerable vector spaces
Authors: Kalantari Iraj 
Published: May 2006

The main point of this paper is a further development of some aspects of the recent theory of recursively enumerable (r.e.) algebraic structures. Initial work in this area is due to Frölich and Shepherdson [4] and Rabin [10]. Here we are only concerned with vector space structure. The previous work on r.e. vector spaces is due to Dekker [2], [3], Metakides and Nerode [8], Remmel [11], Retzlaff [13], and the author [5].Our object of study is V∞ a countably infinite dimensional fully effective vector space over a countable recursive field . By fully effective we mean that V∞. under a fixed Godel numbering has the following properties:(i) Operations of vector addition and scalar multiplication on V∞ are presented by partial recursive functions on the Gödel numbers of elements of V∞.(ii) V∞ has a dependence algorithm, i.e., there is a uniform effective procedure which applied to any n vectors of V∞ determines whether or not they are linearly independent.We also study , the lattice of r.e. subspaces of V∞ (under the operations of intersection, ⋂ and (weak) sum, +). We note that if is not distributive and is merely modular (see [1]). This fact indicates the essential difference between the lattice of r.e. sets and .
Amalgamation of nonstandard models of arithmetic
Authors: Blass Andreas 
Published: May 2006

AbstractAny two models of arithmetic can be jointly embedded in a third with any prescribed isomorphic submodels as intersection and any prescribed relative ordering of the skies above the intersection. Corollaries include some known and some new theorems about ultrafilters on the natural numbers, for example that every ultrafilter with the “4 to 3” weak Ramsey partition property is a P-point. We also give examples showing that ultrafilters with the “5 to 4” partition property need not be P-points and that the main theorem cannot be improved to allow a prescribed ordering of lower skies.
The Hanf number for complete Lω1,ω-sentences (without GCH)
Authors: Baumgartner James E. 
Published: May 2006

The Hanf number for sentences of a language L is defined to be the least cardinal κ with the property that for any sentence φ of L, if φ has a model of power ≥ κ then φ has models of arbitrarily large cardinality. We shall be interested in the language Lω1,ω (see [3]), which is obtained by adding to the formation rules for first-order logic the rule that the conjunction of countably many formulas is also a formula.Lopez-Escobar proved [4] that the Hanf number for sentences of Lω1,ω is ⊐ω1, where the cardinals ⊐α are defined recursively by ⊐0 = ℵ0 and ⊐α = Σ{2⊐β: β < α} for all cardinals α > 0. Here ω1 denotes the least uncountable ordinal.A sentence of Lω1,ω is complete if all its models satisfy the same Lω1,ω-sentences. In [5], Malitz proved that the Hanf number for complete sentences of Lω1,ω is also ⊐ω1, but his proof required the generalized continuum hypothesis (GCH). The purpose of this paper is to give a proof that does not require GCH.More precisely, we will prove the following:Theorem 1. For any countable ordinal α, there is a complete Lω1,ω-sentence σαwhich has models of power ⊐α but no models of higher cardinality.Our basic approach is identical with Malitz's. We simply use a different combinatorial fact at the crucial point.
Models of set theory with more real numbers than ordinals
Authors: Cohen Paul E. 
Published: May 2006

Suppose M is a countable standard transitive model of set theory. P. J. Cohen [2] showed that if κ is an infinite cardinal of M then there is a one-to-one function Fκ from κ into the set of real numbers such that M[Fκ] is a model of set theory with the same cardinals as M.If Tκ is the range of Fκ then Cohen also showed [2] that M[Tκ] fails to satisfy the axiom of choice. We will give an easy proof of this fact.If κ, λ are infinite we will also show that M[Tκ] is elementarily equivalent to M[Tλ] and that (] in M[Fλ]) is elementarily equivalent to (] in M[FK]).Finally we show that there may be an N ∈ M[GK] which is a standard model of set theory (without the axiom of choice) and which has, from the viewpoint of M[GK], more real numbers than ordinals.We write ZFC and ZF for Zermelo-Fraenkel set theory, respectively with and without the axiom of choice (AC). GBC is Gödel-Bernays' set theory with AC. DC and ACℵo are respectively the axioms of dependent choice and of countable choice defined in [6].Lower case Greek characters (other than ω) are used as variables over ordinals. When α is an ordinal, R(α) is the set of all sets with rank less than α.
Omitting types in set theory and arithmetic
Authors: Knight Julia F. 
Published: May 2006

In [7] it is shown that if Σ is a type omitted in the structure = ω, +, ·, < and complete with respect to Th() then Σ is omitted in models of Th() of all infinite powers. The proof given there extends readily to other models of P. In this paper the result is extended to models of ZFC. For pre-tidy models of ZFC, the proof is a straightforward combination of the methods in [7] and in Keisler and Morley ([9], [6]). For other models, the proof involves forcing. In particular, it uses Solovay and Cohen's original forcing proof that GB is a conservative extension of ZFC (see [2, p. 105] and [5, p. 77]).The method of proof used for pre-tidy models of set theory can be used to obtain an alternate proof of the result for This new proof yields more information. First of all, a condition is obtained which resembles the hypothesis of the “Omitting Types” theorem, and which is sufficient for a theory T to have a model omitting a type Σ and containing an infinite set of indiscernibles. The proof that this condition is sufficient is essentially contained in Morley's proof [9] that the Hanf number for omitting types is so the condition will be called Morley's condition.If T is a pre-tidy theory, Morley's condition guarantees that T will have models omitting Σ in all infinite powers.
A reduction class containing formulas with one monadic predicate and one binary function symbol
Authors: Hughes Charles E. 
Published: May 2006

AbstractA new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.
Approximation theorems and model theoretic forcing
Authors: Harnik Victor 
Published: May 2006

We suggest the name “approximation theorems” for a new kind of theorems which are strong versions of preservation theorems. A typical preservation theorem has the form:A sentence φ is preserved by the relation R (i.e. and imply ) iff there exists φ* ϵ Φ such that ⊧φ↔ φ*where R is a relation between structures and Φ is a class of sentences (depending, of course, on R). Usually, Φ is described in syntactical terms and it is easy to see that every element of it is, indeed, preserved by R. A typical approximation theorem has the form:For every sentence Φ there is a sentence Φ* ϵ Φ (the “approximation” of Φ) such that, for all sentences δ which are preserved under R,(a) if ⊧δ → φ then ⊧δ → φ* and(b) if ⊧φ → δ then ⊧φ* → δ.An approximation theorem obviously implies the corresponding preservation theorem.The first approximation theorem was proved by Vaught in [14] (see Corollary 2.3 below). That paper inspired the present one. Vaught's result is stated in topological terms. It says that for each Borel set B there is an invariant Borel set B* explicitly defined by an Lω1ω sentence, such that B− ⊆ B* ⊆ B+ where B− (B+) is the largest (smallest) invariant set included in (containing) B.
Selection in abstract recursion theory
Authors: Harrington L. A. , Macqueen D. B. 
Published: May 2006

In [1] Gandy established the following selection theorem for recursion in type-2 objects.Theorem. Let F be a normal type-2 object. Then it is possible to select (uniformly and effectively in F) an integer from each nonempty set of integers semirecursive in F.Notice that this really asserts that the predicates semirecursive in F are closed under existential quantification over type-0. Moschovakis [6] has essentially proven this theorem for F of arbitrary type.In [2] Grilliot stated a powerful generalization of Gandy's result, namely:Grilliot's Selection Theorem. Let F be a normal type-(n + 2) object (n an arbitrary integer). Then it is possible to select (uniformly and effectively in F) a nonempty recursive in F subset of each nonempty semirecursive in F set oftype-(n − 1) objects.Notice again that this actually says that predicates semirecursive in F are closed under quantification over type-(n − 1) objects.Despite the similarity of these two results, Gandy and Grilliot proposed rather different methods of proof. Furthermore, the proof that Grilliot presented in [2] contains an error which cannot easily be corrected. (We will comment on the nature of this error at the end of §1.) Fortunately, however, Grilliot's theorem is valid. We will present a proof of Grilliot's selection theorem which is a direct generalization of the proof of Gandy's theorem given in [6]. In fact, we will prove a general result (the theorem stated in §2) which subsumes both Gandy's and Grilliot's results.
An axiomatisation of quantum logic
Authors: Clark Ian D. 
Published: May 2006

The purpose of this paper is to give an axiom system for quantum logic. Here quantum logic is considered to have the structure of an orthomodular lattice. Some authors assume that it has the structure of an orthomodular poset.In finding this axiom system the implication algebra given in Finch [1] has been very useful. Finch shows there that this algebra can be produced from an orthomodular lattice and vice versa.Definition. An orthocomplementation N on a poset (partially ordered set) whose partial ordering is denoted by ≤ and which has least and greatest elements 0 and 1 is a unary operation satisfying the following:(1) the greatest lower bound of a and Na exists and is 0,(2) a ≤ b implies Nb ≤ Na,(3) NNa = a.Definition. An orthomodular lattice is a lattice with meet ∧, join ∨, least and greatest elements 0 and 1 and an orthocomplementation N satisfyingwhere a ≤ b means a ∧ b = a, as usual.Definition. A Finch implication algebra is a poset with a partial ordering ≤, least and greatest elements 0 and 1 which is orthocomplemented by N. In addition, it has a binary operation → satisfying the following:An orthomodular lattice gives a Finch implication algebra by defining → byA Finch implication algebra can be changed into an orthomodular lattice by defining the meet ∧ and join ∨ byThe orthocomplementation is unchanged in both cases.
A characterization of terms of the λI-calculus having a normal form
Authors: Barendregt Henk 
Published: May 2006

The theorem proved in this paper answers some transitivity questions (in the geometric sense) for the type free λ-calculus: Which objects can be mapped on all other objects? How much can an object do by applying it to other objects (see footnote 2)?The main result is that, for closed terms of the λI-calculus, the following conditions are equivalent:(a) M has a normal form.(b) FM = I for some λI-term F.(c) MN1 … Nn = I for some λI-terms N1 …, Nn.By the same method it follows that if M is a closed term of the λK-calculus having a normal form, then for some λI-terms (sic) N1, …, Nn, MN1… Nn = I is provable in the λK-calculus.The theorem of Böhm [2] states that if M1, M2 are terms of the λK-calculus having different βη-normal forms, then ∀A1, A2 ∃N1, …, NnMiN1 … Nn = Ai is provable in the λK-βη-calculus for i = 1, 2. As a consequence of this it was shown (implicitly) in [1, 3.2.20 1/2 (1)] that if M has a normal form, then for some λK-terms N1, …, Nn, MN1 … Nn =I is provable in the λK-calculus.It was not clear that this also could be proved for the λK-calculus since the proof of the theorem of Böhm essentially made use of λK-terms.We conjecture that, using the results of this paper, the full theorem of Böhm can be proved for the λI-calculus.
Degrees joining to 0′
Authors: Posner David B. , Robinson Robert W. 
Published: May 2006

AbstractIt is shown that if and are sets of degrees uniformly recursive in 0′ with 0 ∈ then there is a degree b with b′ = 0′, b ∪ c = 0′ for every c ∈ , and a ≰ b for every a ∈ ˜ {0}. The proof is given as an oracle construction recursive in 0′. It follows that any nonrecursive degree below 0′ can be joined to 0′ by a degree strictly below 0′. Also, if a < 0′ and a″ = 0″ then there is a degree b such that a ∪ b = 0′ and a ∩ b = 0.