bluuebunny/crossref_metadata_2025_split huggingface dataset:
Another intuitionistic completeness proof
Authors: De Swart H. 
Published: May 2006

In March 1973, W. Veldman [1] discovered that, by a slight modification of a Kripke-model, it was possible to give an intuitionistic proof of the completeness-theorem for the intuitionistic predicate calculus (IPC) with respect to modified Kripke models. The modification was the following: Let f represent absurdity, then we allow the possibility that and we agree that, for all sentences ϕ, , if . Just one modified Kripke model is constructed such that validity in implies derivability in IPC. While usually one thinks of as some subset of ⋃nNatn and of as the discrete natural ordering in ⋃nNatn, in Veldman's model , is a spread and , where Γα and Γβ are sets of sentences associated with α, resp. β, is a nondiscrete ordering.In the completeness-proofs, both for Beth and for Kripke models that we present here, we consider only models over ⋃nNatn, with the natural discrete ordering and we need validity in all models, not just in one, to get derivability in IPC. Also we have to modify the definition of a model in a somewhat different way than Veldman did. We agree that if ∨s[M⊨sf], then M⊨sϕ for each s ∈ ⋃nNatn and for each sentence ϕ.One can view a single model of the type constructed in [1] as the result of throwing together all the models of (the type constructed in) this paper into one big model, which has the somewhat strange properties mentioned above.
Higher Souslin trees and the generalized continuum hypothesis
Authors: Gregory John 
Published: May 2006

The existence of an ω2-Souslin tree will be proved (Theorem 2.2 or §3) from the Generalized Continuum Hypothesis (GCH) plus Jensen's combinatorial principle □ω1. Thus, it follows from Jensen's 1.4(2) that the consistency of the formal theory T given by ZFC + GCH + “ω2-Souslin Hypothesis” implies the consistency of ZFC + “there exists a Mahlo cardinal.” So one does not hope to prove the consistency of this T relative to the consistency of ZFC + “there is an inaccessible cardinal, hence there are transitive models of ZFC.”Silver [5, Theorem 5.8] has shown that the consistency of ZFC + “there is a weakly compact cardinal” implies the consistency of ZFC + not GCH + “there is no ω2-Aronszajn tree, hence no ω2-Souslin tree”; this is one reason why we deal with GCH here. Jensen has shown that the consistency of ZFC implies the consistency of ZFC +GCH + “ω1-Souslin Hypothesis.”In the preliminary §1, we state some definitions and known results about trees and some of Jensen's combinatorial principles, including □ and ◇*(E).Our main Lemma 2.1 states (a fortiori) that GCH implies ◇* at ω-cofinal elements of ω2 (i.e., in our notation, ◇*(E(ω) ∩ ω2)). From Lemma 2.1 and the known facts of §1, it is proved (2.5) that if □k, the cofinality cf(k)> ω, and GCH, then there is a k+-Souslin tree. For k = ω1, this implies the result mentioned above for ω2-Souslin trees.
The consistency problem for NF
Authors: Boffa M. 
Published: May 2006

Although this problem is still open, there are a few related results concerning (i) theories equiconsistent with NF and (ii) consistent fragments of NF. Concerning (i) we will discuss the following results(1) Specker's result about the equiconsistency of NF with an extension of the theory of types [16],(2) the equiconsistency of NF with fragments of NF containing NFU [2], [10],and a new one about(3) the equiconsistency of NF with an extension of Zermelo's set theory with the axiom of comprehension restricted to bounded formulas.Concerning (ii) we will give a simplified proof and a generalization of (4) Jensen's result about the consistency of NFU [13].Only a few words will be devoted to(5) Grishin's results and refinements [4], [5], [8], [9], treated with more details in [4].The reader who is unfamiliar with NF or who has a natural repulsion for this system is first invited to read the excellent account contained in [7, Chapter III, §3].
A theorem on shortening the length of proof in formal systems of arithmetic
Authors: di Paola Robert A. 
Published: May 2006

This note is concerned with an aspect of the length of proof of formulas in recursively enumerable theories T adequate for recursive arithmetic. In particular, we consider the relative length of proof of formulas in the theories T and T(S), where F represents an r.e. set A in T and T(S) is the theory obtained from T by adjunction, as a new axiom, of a sentence S undecidable in T.Throughout the sequel T is a consistent, r.e. theory with standard formalization [7] in which all recursive functions of one variable are definable, and in which there is a binary formula x ≤ satisfying the well-known conditions [7]:Here is the constant term corresponding to the natural number n. Wn is the nth r.e. set in a standard enumeration of the r.e. sets. Also, we assume an a priori Gödel numbering of our formalism satisfying the usual conditions, so that all formulas are numbers ab initio.In the more common applications of the theorem below, if F is a k-ary formula of T, is a natural number that measures in some way the length of the shortest proof of in T.
On finite lattices of degrees of constructibility of reals
Authors: Adamowicz Zofia 
Published: May 2006

Theorem. Assume that there exists a standard model of ZFC + V = L. Then there is a model of ZFC in which the partial ordering of the degrees of constructibility of reals is isomorphic with a given finite lattice.The proof of the theorem uses forcing. The definition of the forcing conditions and the proofs of some of the lemmas are connected with Lerman's paper on initial segments of the upper semilattice of the Turing degrees [2]. As an auxiliary notion we shall introduce the notion of a sequential representation of a lattice, which slightly differs from Lerman's representation.Let K be a given finite lattice. Assume that the universe of K is an integer l. Let ≤K be the ordering in K. A sequential representation of K is a sequence Ui ⊆ Ui+1 of finite subsets of ωi such that the following holds:(1) For any s, s′ Є Ui, i Є ω, k, m Є l, k ≤Km & s(m) = s′(m) → s(k) = s′(k).(2) For any s Є Ui, i Є ω, s(0) = 0 where 0 is the least element of K.(3) For any s, s′ Є i Є ω, k,j Є l, if k y Kj = m and s(k) = s′(k) & s(j) = s′(j) → s(m) = s′(m), where vK denotes the join in K.
Noncharacterizability of the syntax set
Authors: Paulos John 
Published: May 2006

Craig showed in [3] that Beth's theorem fails for 2nd order logic. This is so since the syntax for 2nd order logic can be represented in the structure of natural numbers and itself can be characterized in 2nd order logic. Thus the satisfaction relation S is implicitly definable yet not explicitly definable (by a Tarski diagonal argument) and Beth fails. Kreisel pointed out in a review of Craig's paper that a similar argument shows that Beth's theorem fails for ω-logic or for any logic whose syntax can be represented in and in which can be characterized. In this paper we use the abstract model-theoretic notions of truth adequacy, truth-maximality and truth-completeness developed by Feferman in [4] to prove the following generalization of Craig's result: If L is a truth-complete logic, then no structure in which the syntax is represented is L-characterizable. This is applied via a corollary to give new examples of failures of Beth's theorem. Another way to construe this result is that truth-complete logics L have the desirable model-theoretic property (see [5]) that the structure in which the syntax is represented is not generalized finite (interpreting generalized finite as L-characterizability).Since the basic notions of [4] are defined in terms of many-sorted logics, we will consider all our logics to be many-sorted.
Relative consistency of an extension of Ackermann's set theory
Authors: Lake John 
Published: May 2006

The set theory AFC was introduced by Perlis in [2] and he noted that it both includes and is stronger than Ackermann's set theory. We shall give a relative consistency result for AFC.AFC is obtained from Ackermann's set theory (see [2]) by replacing Ackermann's set existence schema with the schema(where ϕ, ψ, are ∈-formulae, x is not in ψ, w is not in ϕ, y is y1, …, yn, z is z1, …, zm and all free variables are shown) and adding the axiom of choice for sets. Following [1], we say that λ is invisible in Rκ if λ < κ and we haveholding for every ∈-formula θ which has exactly two free variables and does not involve u or υ. The existence of a Ramsey cardinal implies the existence of cardinals λ and κ with λ invisible in Rκ, and Theorem 1.13 of [1] gives some further indications about the relative strength of the notion of invisibility.Theorem. If there are cardinals λ and κ with λ invisible in Rκ, then AFC is consistent.Proof. Suppose that λ is invisible in Rκ and we will show that 〈Rκ, Rλ, ∈〉 ⊧ AFC (Rλ being the interpretation of V, of course).
Effective coloration
Authors: Bean Dwight R. 
Published: May 2006

AbstractWe are concerned here with recursive function theory analogs of certain problems in chromatic graph theory. The motivating question for our work is: Does there exist a recursive (countably infinite) planar graph with no recursive 4-coloring? We obtain the following results: There is a 3-colorable, recursive planar graph which, for all k, has no recursive k-coloring; every decidable graph of genus p ≥ 0 has a recursive 2(x(p) − 1)-coloring, where x(p) is the least number of colors which will suffice to color any graph of genus p; for every k ≥ 3 there is a k-colorable, decidable graph with no recursive k-coloring, and if k = 3 or if k = 4 and the 4-color conjecture fails the graph is planar; there are degree preserving correspondences between k-colorings of graphs and paths through special types of trees which yield information about the degrees of unsolvability of k-colorings of graphs.
Adding a closed unbounded set
Authors: Baumgartner J. E. , Harrington L. A. , Kleinberg E. M. 
Published: May 2006

The extreme interest of set theorists in the notion of “closed unbounded set” is epitomized in the following well-known theorem:Theorem A. For any regular cardinal κ > ω, the intersection of any two closed unbounded subsets of κ is closed and unbounded.The proof of this theorem is easy and in fact yields a stronger result, namely that for any uncountable regular cardinal κ the intersection of fewer than κ many closed unbounded sets is closed and unbounded. Thus, if, for κ a regular uncountable cardinal, we let denote {A ⊆ κ ∣ A contains a closed unbounded subset}, then, for any such κ, is a κ-additive nonprincipal filter on κ.Now what about the possibility of being an ultrafilterκ It is routine to see that this is impossible for κ > ℵ1. However, for κ = ℵ1 the situation is different. If were an ultrafilter, ℵ1 would be a measurable cardinal. As is well-known this is impossible if we assume the axiom of choice; however if ZF + “there exists a measurable cardinal” is consistent, then so is ZF + “ℵ1 is a measurable cardinal” [2]. Furthermore, under the assumption of certain set theoretic axioms (such as the axiom of determinateness or various infinite exponent partition relations) can be proven to be an ultrafilter. (See [3] and [5].)
Model Theoretic Algebra
Authors: Cherlin G. L. 
Published: May 2006

Since the late 1940's model theory has found numerous applications to algebra. I would like to indicate some of the points of contact between model theoretic methods and strictly algebraic concerns by means of a few concrete examples and typical applications.§1. The Lefschetz principle. Algebraic geometry has proved to be a fruitful source of model theoretic ideas. What exactly is algebraic geometry? We consider a field K, and let Kn be the set of n-tuples (a1 … an) with coordinates ai in K. Kn is called affine n-space over K. Fix polynomials p1 …, pk in K[x1, …, xn] and definethat is V(p1 …, pk) is the locus of common zeroes of the pi in Kn. We call V(Pi …, Pk) the algebraic variety determined by p1, …, pk. With this terminology we may say:Algebraic geometry is the study of algebraic varieties defined over an arbitrary field K. This definition lacks both rigor and accuracy, and we will indicate below how it may be improved.So far we have placed no restrictions on the base field K. Following Weil [4] it is convenient to start with a so-called “universal domain”; in other words take K to be algebraically closed and of infinite transcendence degree over the prime field. Any particular field can of course be embedded in such a universal domain.
A complete infinitary logic
Authors: Slonneger Kenneth 
Published: May 2006

This paper is concerned with the proof theoretic development of certain infinite languages. These languages contain the usual infinite conjunctions and disjunctions, but in addition to homogeneous quantifiers such as ∀x0x1x2 … and ∃y0y1y2 …, we shall investigate particular subclasses of the dependent quantifiers described by Henkin [1]. The dependent quantifiers of Henkin can be thought of as partially ordered quantifiers defined by a function from one set to the power set of another set. This function assigns to each existentially bound variable, the set of universally bound variables on which it depends.The natural extension of Gentzen's first order predicate calculus to an infinite language with homogeneous quantifiers results in a system that is both valid and complete, and in which a cut elimination theorem can be proved [2]. The problem then arises of devising, if possible, a logical system dealing with general dependent quantifiers that is valid and complete. In this paper a system is presented that is valid and complete for an infinite language with homogeneous quantifiers and dependent quantifiers that are anti-well-ordered, for example, … ∀x2∃y2∀x1∃y1∀x0∃y0.Certain notational conventions will be employed in this paper. Greek letters will be used for ordinal numbers. The ordinal ω is the set of all natural numbers, and 2ω is the set of all ω -sequences of elements of 2 = {0,1}. The power set of S is denoted by P(S). μα[A(α)] stands for the smallest ordinal α such that A (α) holds.
Comparison of Russell's resolution of the semantical antinomies with that of Tarski
Authors: Church Alonzo 
Published: May 2006

In this paper we treat the ramified type theory of Russell [6], afterwards adopted by Whitehead and Russell inPrincipia mathematica[12], so that we may compare Russell's resolution of the semantical antinomies by ramified type theory with the now widely accepted resolution of them by the method of Tarski in [7], [8], [9].To avoid impredicativity the essential restriction is that quantification over any domain (type) must not be allowed to add new members to the domain, as it is held that adding new members changes the meaning of quantification over the domain in such a way that a vicious circle results. As Whitehead and Russell point out, there is no one particular form of the doctrine of types that is indispensable to accomplishing this restriction, and they have themselves offered two different versions of the ramified hierarchy in the first edition ofPrincipia(seePreface, p. vii). The version in §§58–59 of the writer's [1], which will be followed in this paper, is still slightly different.To distinguish Russellian types or types in the sense of the ramified hierarchy from types in the sense of the simple theory of types, let us call the formerr-types.There is an r-typeito which the individual variables belong. Ifβ1,β2, …,βmare any given r-types,m≧ 0, there is an r-type (β1,β2, …,βm)/nto which there belongm-ary functional variables of leveln,n≧ 1. The r-type (α1,α2, …,αm)/kis said to bedirectly lowerthan the r-type (β1,β2, …,βm)/nifα1=β1,α2=β2, …,αm=βm,k<n.
The intersection of nonstandard models of arithmetic
Authors: Blass Andreas 
Published: May 2006

If two nonstandard models of complete arithmetic are elementarily embedded in a third, then their intersection may be considerably smaller than either of them; indeed, the intersection may be only the standard model. For example, if D and E are nonprincipal ultrafilters on ω, then the nonstandard models D-prod and E-prod (where is the standard model) have canonical elementary embeddings into D-prod (E-prod , and the intersection of their images is easily seen to be the (canonical image of the) standard model. In this paper, we shall prove that, under certain conditions, this phenomenon will not occur. Our main result (Theorem 3) is that the intersection of countably many pairwise cofinal models is itself cofinal with these models, provided that at least one of them is generated by a single element. (Precise definitions will be given below.)The theorems in this paper were first formulated in terms of ultrafilters, then rephrased (using the methods of Chapter III of [1]) as statements about ultra-powers of , and finally generalized to their present form. Since the theorems and their proofs are now entirely model-theoretic, they are presented here separately from the study of ultrafilters in which they originated. That study, including applications of the present results, will appear in [2].Let L be the first-order language whose n-place relation symbols are all the relations R ⊆; ωn and whose n-place function symbols are all the functions f: ωn → ω. Let be the standard model for L; its universe is ω and every nonlogical symbol of L denotes itself. Let be an elementary extension of . The relation (or function) denoted by R (or f) in will be called *R (or *f).
Semantic analysis of tense logics
Authors: Thomason S. K. 
Published: May 2006

Although we believe the results reported below to have direct philosophical import, we shall for the most part confine our remarks to the realm of mathematics. The reader is referred to [4] for a philosophically oriented discussion, comprehensible to mathematicians, of tense logic.The “minimal” tense logicT0is the system having connectives ∼, →,F(“at some future time”), andP(“at some past time”); the following axioms:(whereGandHabbreviate ∼F∼ and ∼P∼ respectively); and the following rules:(8) fromαandα → β, inferβ,(9) fromα, infer any substitution instance ofα,(10) fromα, inferGα,(11) fromα, inferHα.A tense logic is a systemTwhose language is that ofT0and whose axioms and rules include (1)–(11). The axioms and rules ofTother than (1)–(11) are calledproperaxioms and rules.We shall investigate three systems of semantics for tense logics, i.e. three notions ofstructureand three relations ⊧ which stand between structures and formulas. One reads⊧αas “αis valid in.” A structureis amodelof a tense logicTif every formula provable inTis valid in. A semantics isadequateforTif the set of models ofTin the semantics is characteristic forT, i.e. if wheneverT ∀ αthen there is a modelofTin the semantics such that∀ α. Two structuresand, possibly from different semantics, are calledequivalent(∼) if exactly the same formulas are valid inas in.
Σn sets which are Δn-incomparable (uniformly)
Authors: Shore Richard A. 
Published: May 2006

In this paper we will present an application of generalized recursion theory to (noncombinatorial) set theory. More precisely we will combine a priority argument in α-recursion theory with a forcing construction to prove a theorem about the interdefinability of certain subsets of admissible ordinals.Our investigation was prompted by G. Sacks and S. Simpson asking [6] if it is obvious that there are, for each Σn-admissible α, Σn (over Lα) subsets of α which are Δn-incomparable. If one understands “B is Δn in C” to mean that there are Σn/Lα reduction procedures which put out B and when one feeds in C, then the answer is an unqualified “yes.” In this sense “Δn in” is a direct generalization of “α-recursive in” (replace Σ1 by Σn in the definition) and so amenable to the methods of [7, §§3, 5]. Indeed one simply chooses a complete Σn−1 set A and mimics the construction of [6] as modified in [7, §5] to produce two α-A-r.e. sets B and C neither of which is α-A-recursive in the other. By the remarks on translation [7, §3] this will immediately give the desired result for this definition of “Δn in.”There is, however, the more obvious and natural notion of “Δn in” to be considered: B is Δn in C iff there are Σn and Πn formulas of ⟨Lα, C⟩ which define B.
On power-like models for hyperinaccessible cardinals
Authors: Schmerl James H. , Shelah Saharon 
Published: May 2006

The main result of this paper is the following transfer theorem: If T is an elementary theory which has a κ-like model where κ is hyperinaccessible of type ω, then T has a λ-like model for each λ > card(T). Helling [3] obtained the same conclusion under the stronger hypothesis that κ is weakly compact. Fuhrken conjectured in [1] that the same conclusion would result if κ were merely inaccessible. (He also showed there the connection with a problem about generalized quantifiers.) Thus, our theorem lies properly between Helling's theorem and Fuhrken's conjecture. In [9] it is shown that this theorem is actually the best possible. This theorem and the other results of this paper were announced by the authors in [10].In §1 we prove as Theorem 1 a slightly stronger form of the above theorem. This theorem is generalized in §2 to Theorem 2 which concerns theories which permit the omitting of types. The methods used in §§1 and 2 are also applicable to problems regarding Hanf numbers as well as to two-cardinal problems.
On the undecidability of finite planar cubic graphs
Authors: Garfunkel Solomon , Shank Herbert 
Published: May 2006

In the March, 1971 issue of this Journal [1] a paper of ours was published purporting to prove the hereditary undecidability of the first-order theory of finite planar graphs. The proof presented there contains an error which is unfortunately “unfixable” by the methods of that paper. The theorem however is true and we demonstrate here a generalization to finite cubic (exactly three edges at each vertex) planar graphs. The method involves coding the halting problem for a Turing machine into the theory of these graphs by considering special printouts of computations. Let us first consider a discussion of the aforementioned mistake and see what can be learned from it.By a graph we will mean a nonempty set V of points together with a set I of unordered pairs of points of V. Each point i = {u, v) ∈ I is an edge of A graph is called finite if ∣V∣ is finite. A graph is said to be planar iff it can be embedded in the plane (i.e., drawn in the plane so that no two edges intersect).In the earlier paper the method of proof was a semantic embedding of certain binary relations into finite planar graphs. The essential idea was, for a given relation, to let the vertices of the graph interpret the field of the relation and the edges represent the related pairs. This method works for arbitrary graphs, but in the planar case has two main difficulties.
Ordinals connected with formal theories for transfinitely iterated inductive definitions
Authors: Pohlers W. 
Published: May 2006

Let Th be a formal theory extending number theory. Call an ordinal ξ provable in Th if there is a primitive recursive ordering which can be proved in Th to be a wellordering and whose order type is > ξ. One may define the ordinal ∣ Th ∣ of Th to be the least ordinal which is not provable in Th. By [3] and [12] we get , where IDN is the formal theory for N-times iterated inductive definitions. We will generalize this result not only to the case of transfinite iterations but also to a more general notion of ‘the ordinal of a theory’.For an X-positive arithmetic formula [X,x] there is a natural norm ∣x∣: = μξ (x ∈ Iξ), where Iξ is defined as {x: [∪μ<ξIμ, x]} by recursion on ξ (cf. [7], [17]). By P we denote the least fixed point of [X,x]. Then P = ∪ξξ holds. If Th allows the formation of P, we get the canonical definitions ∥Th()∥ = sup{∣x∣ + 1: Th ⊢ x ∈ P} and ∥Th∥ = sup{∥Th()∥: P is definable in Th} (cf. [17]). If ≺ is any primitive recursive ordering define Q≺[X,x] as the formula ∀y(y ≺ x → y ∈ X) and ∣x∣≺:= ∣x∣O≺. Then ∣x∣≺ turns out to be the order type of the ≺ -predecessors of x and P is the accessible part of ≺. So Th ⊢ x ∈ P implies the provability of ∣x∣≺ in Th.