bluuebunny/crossref_metadata_2025_split huggingface dataset:
Replacement and collection in intuitionistic set theory
Authors: Goodman Nicolas D. 
Published: May 2006

Intuitionistic Zermelo-Fraenkel set theory, which we call ZFI, was introduced by Friedman and Myhill in [3] in 1970. The idea was to have a theory with the same axioms as ordinary classical ZF, but with Heyting's predicate calculus HPC as the underlying logic. Since some classically equivalent statements are intuitionistically inequivalent, however, it was not always obvious which form of a classical axiom to take. For example, the usual formulation of the axiom of foundation had to be replaced with a principle of transfinite induction on the membership relation in order to avoid having excluded middle provable and thus making the logic classical. In [3] the replacement axiom is taken in its most common classical form:In the presence of the separation axiom,this is equivalent to the axiomIt is this schema Rep that we shall call the replacement axiom.Friedman and Myhill were able to show in [3] that ZFI has a number of desirable “constructive” properties, including the existence property for both numbers and sets. They were not able to determine, however, whether ZFI is proof-theoretically as strong as ZF. This is still open.Three years later, in [2], Friedman introduced a theory ZF− which is like ZFI except that the replacement axiom is changed to the classically equivalent collection axiom:He showed that ZF− is proof-theoretically of the same strength as ZF, and he asked whether ZF− is equivalent to ZFI.
Simplified morasses with linear limits
Authors: Velleman Dan 
Published: May 2006

In a recent series of papers Kanamori ([4], [5], and [6]) defines generalizations of several combinatorial principles known to follow from the existence of morasses. Kanamori proves the consistency of his generalizations by forcing arguments which come close to satisfying the hypotheses of the Martin's Axiom-type characterizations of morasses developed independently by Shelah and Stanley [9] and the author [12]. A similar “almost application” of morasses appears in [11], in which Todorčević uses forcing to prove the consistency of the existence of Kurepa trees with no Aronszajn or Cantor subtrees. In all cases the attempted proofs using morasses fail for the same reason: the partial orders involved do not have strong enough closure properties.In an attempt to solve this problem Shelah and Stanley strengthened their characterization of morasses to allow applications to what they called “good canonical limit” partial orders. However, for rather subtle reasons even this strengthened forcing axiom is not good enough for the proposed applications. The problem this time is that Shelah and Stanley's “weak commutativity of Lim and restriction” requirement (see [9, 3.9(iv)]) is not satisfied. Furthermore, there is reason to believe that an ordinary morass is just not good enough for these applications, since in L morasses exist at all regular uncountable cardinals, but even a weak form of Todorčević's conclusion cannot hold at ineffable cardinals (see the end of §4).A possible solution to this problem is suggested by the fact that □κ is equivalent to a forcing axiom which applies to partial orders satisfying precisely the kind of weak closure conditions involved in the examples described above (see [13]). What is needed to make the proposed morass applications work is something which will do for morass constructions what □κ does for ordinary transfinite recursion constructions. In this paper we show how extra structure can be built into a morass to accomplish this goal.
A normal form theorem for first order formulas and its application to Gaifman's splitting theorem
Authors: Motohashi Nobuyoshi 
Published: May 2006

Let L be a first order predicate calculus with equality which has a fixed binary predicate symbol <. In this paper, we shall deal with quantifiers Cx, ∀x ≦ y, ∃x ≦ y defined as follows: CxA(x) is ∀y∃x(y ≦ x ∧ A(x)), ∀x ≦ yA{x) is ∀x(x ≦ y ⊃ A(x)), and ∃x ≦ yA(x) is ∃x(x ≦ y ∧ 4(x)). The expressions x̄, ȳ, … will be used to denote sequences of variables. In particular, x̄ stands for 〈x1, …, xn〉 and ȳ stands for 〈y1,…, ym〉 for some n, m. Also ∃x̄, ∀x̄ ≦ ȳ, … will be used to denote ∃x1 ∃x2 … ∃xn, ∀x1 ≦ y1 ∀x2 ≦ y2 … ∀xn ≦ yn, …, respectively. Let X be a set of formulas in L such that X contains every atomic formula and is closed under substitution of free variables and applications of propositional connectives ¬(not), ∧(and), ∨(or). Then, ∑(X) is the set of formulas of the form ∃x̄B(x̄), where B ∈ X, and Φ(X) is the set of formulas of the form.Since X is closed under ∧, ∨, the two sets Σ(X) and Φ(X) are closed under ∧, ∨ in the following sense: for any formulas A and B in Σ(X) [Φ(X)], there are formulas in Σ(X)[ Φ(X)] which are obtained from A ∧ B and A ∨ B by bringing some quantifiers forward in the usual manner.
Functional interpretation of the β-rule
Authors: Koletsos George 
Published: May 2006

Since the invention of β-logic by J. Y. Girard, a lot of work has been done concerning different aspects of this logic, β-completeness (classical and intuitionistic), interpolation theorems, and completeness of Lβω are some examples of this (see [2], [4] and [5]).In this paper we examine the question, posed by J. Y. Girard, of the Gödel-functional interpretation for this new logic.The central notion in β-logic is the notion of the β-rule. The β-rule is a functor which appropriately groups x-proofs, for every ordinal x. An x-proof is like a proof in ω-logic but instead of the ω-rule, with premises indexed by ω, we use the x-rule, with premises indexed by x.In order to obtain the Gödel-functional interpretation of the β-rule, we need, first, a functional interpretation of the x-proofs, which require functionals using the x-rule for their construction (the x-functionals) and, second, an appropriate grouping of these x-functionals by means of a functor (the β-functionals).We use the letters x,y,z, … and sometimes the Greek letters α and γ to denote ordinals. ON is the category of ordinals. The objects are the ordinals, and the morphisms from x to y are the members of I(x, y), which is the set of all strictly increasing functions from x to y. ON < ω denotes the restriction of ON to ω, the set of finite ordinals. We denote direct systems, in ON or in more general categories, by (xi, fij) where fij is the morphism from xi, to xj. If the direct limit exists we denote it by (x, fi), where fi is the morphism from xi to x. We write (x, fi) =lim(xifij). In ON the direct limits are unique.
Proper classes via the iterative conception of set
Authors: Sharlow Mark F. 
Published: May 2006

AbstractWe describe a first-order theory of generalized sets intended to allow a similar treatment of sets and proper classes. The theory is motivated by the iterative conception of set. It has a ternary membership symbol interpreted as membership relative to a set-building step. Set and proper class are defined notions. We prove that sets and proper classes with a defined membership form an inner model of Bernays-Morse class theory. We extend ordinal and cardinal notions to generalized sets and prove ordinal and cardinal results in the theory. We prove that the theory is consistent relative to ZFC + (∃x) [x is a strongly inaccessible cardinal].
Natural deduction and sequent calculus for intuitionistic relevant logic
Authors: Tennant Neil 
Published: May 2006

Relevance logic began in an attempt to avoid the so-called fallacies of relevance. These fallacies can be in implicational form or in deductive form. For example, Lewis's first paradox can beset a system in implicational form, in that the system contains as a theorem the formula (A & ∼A) → B; or it can beset it in deductive form, in that the system allows one to deduce B from the premisses A, ∼A.Relevance logic in the tradition of Anderson and Belnap has been almost exclusively concerned with characterizing a relevant conditional. Thus it has attacked the problem of relevance in its implicational form. Accordingly for a relevant conditional → one would not have as a theorem the formula (A & ∼A) → B. Other theorems even of minimal logic would also be lacking. Perhaps most important among these is the formula (A → (B → A)). It is also a well-known feature of their system R that it lacks the intuitionistically valid formula ((A ∨ B) & ∼A) → B (disjunctive syllogism).But it is not the case that any relevance logic worth the title even has to concern itself with the conditional, and hence with the problem in its implicational form. The problem arises even for a system without the conditional primitive. It would still be an exercise in relevance logic, broadly construed, to formulate a deductive system free of the fallacies of relevance in deductive form even if this were done in a language whose only connectives were, say, &, ∨ and ∼. Solving the problem of relevance in this more basic deductive form is arguably a precondition for solving it for the conditional, if we suppose (as is reasonable) that the relevant conditional is to be governed by anything like the rule of conditional proof.
Von Mises' definition of random sequences reconsidered
Authors: van Lambalgen Michiel 
Published: May 2006

AbstractWe review briefly the attempts to define random sequences (§0). These attempts suggest two theorems: one concerning the number of subsequence selection procedures that transform a random sequence into a random sequence (§§1–3 and 5); the other concerning the relationship between definitions of randomness based on subsequence selection and those based on statistical tests (§4).
Alfred Tarski and decidable theories
Authors: Doner John , Hodges Wilfrid 
Published: May 2006

Any list of Alfred Tarski's achievements would mention his decision procedure for real-closed fields. He proved a number of other less publicized decidability results too. We shall survey these results. After surveying them we shall ask what Tarski had in mind when he proved them. Today our emphases and concepts are sometimes different from those of Tarski in the early 1930s. Some of these changes are the direct result of Tarski's own fundamental work in model theory during the intervening years.Tarski's work on decidable theories is important not just for the individual decidability theorems themselves. His method for all these decidability results was elimination of quantifiers, and he systematically used this method to prove a range of related theorems about completeness and definability. He also led several of his students to do important work using this same method. Tarski's use of quantifier elimination has had a deep and cumulative influence on model theory and the logical treatment of algebraic theories.We thank Solomon Feferman, Steven Givant, Haragauri Gupta, Yuri Gurevich. Angus Macintyre, Gregory Moore, Robert Vaught and the referee for helpful discussions and comments. Also we thank Madame Maria Mostowska and Roman Murawski for sending us material from Polish libraries.
Notions of relative ubiquity for invariant sets of relational structures
Authors: Bankston Paul , Ruitenburg Wim 
Published: May 2006

AbstractGiven a finite lexicon L of relational symbols and equality, one may view the collection of all L-structures on the set of natural numbers ω as a space in several different ways. We consider it as: (i) the space of outcomes of certain infinite two-person games; (ii) a compact metric space; and (iii) a probability measure space. For each of these viewpoints, we can give a notion of relative ubiquity, or largeness, for invariant sets of structures on ω. For example, in every sense of relative ubiquity considered here, the set of dense linear orderings on ω is ubiquitous in the set of linear orderings on ω.
Maximal r.e. equivalence relations
Authors: Carroll Jeffrey S. 
Published: May 2006

AbstractThe lattice of r.e. equivalence relations has not been carefully examined even though r.e. equivalence relations have proved useful in logic. A maximal r.e. equivalence relation has the expected lattice theoretic definition. It is proved that, in every pair of r.e. nonrecursive Turing degrees, there exist maximal r.e. equivalence relations which intersect trivially. This is, so far, unique among r.e. submodel lattices.
On infinite series of infinite isols
Authors: Barback Joseph 
Published: May 2006

We are interested in regressive isols, recursive functions, and the extensions of recursive functions to the isols. One of the nicest concepts that has been applied to the study of these notions is of an infinite series of isols. J. C. E. Dekker introduced infinite series of isols in [3]. With this concept one may associate with each number theoretic function u and regressive isol B a value in the isols to correspond to the seriesWhen u is chosen as a recursive function, or as a recursive combinatorial function, many of the sums that one associates with familiar finite series may be generalized to infinite series. For example, if B is any regressive isol, thenThe results presented in our paper were motivated by an interest in extending infinite series to a setting where the terms being summed may be infinite isols. In our paper, we do this in a special way, as will be described below. We would first like to briefly comment on some facts about the concept of defining an infinite series in the isols.
Formal languages defined by the underlying structure of their words
Authors: Ressayre J. P. 
Published: May 2006

Abstracti) We show for each context-free language L that by considering each word of L as a structure in a natural way, one turns L into a finite union of classes which satisfy a finitary analog of the characteristic properties of complete universal first order classes of structures equipped with elementary embeddings. We show this to hold for a much larger class of languages which we call free local languages, ii) We define local languages, a class of languages between free local and context-sensitive languages. Each local language L has a natural extension L∞ to infinite words, and we prove a series of “pumping lemmas”, analogs for each local language L of the “uvxyz theorem” of context free languages: they relate the existence of large words in L or L∞ to the existence of infinite “progressions” of words included in L, and they imply the decidability of various questions about L or L∞. iii) We show that the pumping lemmas of ii) are independent from strong axioms, ranging from Peano arithmetic to ZF + Mahlo cardinals.We hope that these results are useful for a model-theoretic approach to the theory of formal languages.
Constructive validity is nonarithmetic
Authors: McCarty Charles 
Published: May 2006

It follows constructively from weak versions of Markov's principle (MP) and of Church's thesis (WCT) that logical validity for single sentences is not arithmetically definable. This is a direct consequence of the constructive model-theoretic fact that, using MP and WCT, one can prove the categoricity of first-order Heyting arithmetic. By a straightforward refinement of this proof, we then obtain generalizations of the incompleteness theorem of Kreisel [K 2] as presented by van Dalen [Da] and improved by Leivant [L 1]. An analogous result for classical validity in r.e. models appears in [V].Our methods of proof are new in that they rely not upon variants of the ideas of [K2] but upon a constructive proof idea inspired by the classical result of Tennenbaum ([Te], [E&K], [S]) on recursive models of arithmetic. This line of reasoning was suggested by the applications of readability to recursive mathematics described in [McC1], [McC2] and [McC3].
Souslin forcing
Authors: Ihoda Jaime I. , Shelah Saharon 
Published: May 2006

AbstractWe define the notion of Souslin forcing, and we prove that some properties are preserved under iteration. We define a weaker form of Martin's axiom, namely , and using the results on Souslin forcing we show that is consistent with the existence of a Souslin tree and with the splitting number s = ℵ1. We prove that proves the additivity of measure. Also we introduce the notion of proper Souslin forcing, and we prove that this property is preserved under countable support iterated forcing. We use these results to show that ZFC + there is an inaccessible cardinal is equiconsistent with ZFC + the Borel conjecture + -measurability.
A basis result in combinatory logic
Authors: Legrand Remi 
Published: May 2006

The aim of this article is to show that a basis for combinatory logic [2] must contain at least one combinator with rank strictly greater than two. We use notation of [1].Let Q be a primitive combinator given by its reduction rule Qx1 … xn → C, where C is a pure combination of the variables x1,…, xn. n is called the rank of the combinator.A set {Q1,…,Qn} of combinators is a basis for combinatory logic if for every finite set {x1,…,xm} of variables and every pure combination C of these variables, there exists a pure combinator Q of Q1,…,Qn such that Qx1…xm↠C.Property. The Church-Rosser theorem and the (quasi-)normalization theorem are valid for the combinatory reduction system under consideration.Proof. See [4], [5], and [6].Any basis must contain at least one combinator with rank strictly greater than two.Let us assume a basis B with combinators of rank strictly less than 3; then there exists a pure combination X of the combinators in B such that: XABC ↠ CAB.(*) First of all, we remark that if XABC ↠ M ↠ CAB, M must contain at least one occurrence of each of the variables A, B and C.Notation. We denote by E[X1,…,Xn] expressions that contain at least one occurrence of every term X1,…,Xn.
Colimit completions and the effective topos
Authors: Robinson Edmund , Rosolini Giuseppe 
Published: May 2006

The family of readability toposes, of which the effective topos is the best known, was discovered by Martin Hyland in the late 1970's. Since then these toposes have been used for several purposes. The effective topos itself was originally intended as a category in which various recursion-theoretic or effective constructions would live as natural parts of the higher-order type structure. For example the hereditary effective operators become the higher types over N (Hyland [1982]), and effective domains become the countably-based domains in the topos (McCarty [1984], Rosolini [1986]). However, following the discovery by Moggi and Hyland that it contained nontrivial small complete categories, the effective topos has also been used to provide natural models of polymorphic type theories, up to and including the theory of constructions (Hyland [1987], Hyland, Robinson and Rosolini [1987], Scedrov [1987], Bainbridge et al. [1987]).Over the years there have also been several different constructions of the topos. The original approach, as in Hyland [1982], was to construct the topos by first giving a notion of Pω-valued set. A Pω-valued set is a set X together with a function =x: X × X → Pω. The elements of X are to be thought of as codes, or as expressions denoting elements of some “real underlying” set in the topos. Given a pair (x,x′) of elements of X, the set =x (x,x′) (generally written ) is the set of codes of proofs that the element denoted by x is equal to the element denoted by x′.
Anneaux p-adiquement clos et anneaux de fonctions définissables
Authors: Bélair Luc 
Published: May 2006

Nous considérons des théories d'anneaux locaux reliées aux corps p-adiques, p un nombre premier. Dans le §1 nous établissons les axiomatisations données dans [B1], ainsi qu'une autre axiomatisation des anneaux apparaissant dans [R1]. Il s'agit d'anneaux locaux henséliens dont le corps résiduel est élémentairement équivalent à une extension finie d'un corps p-adique. Nous les appelons anneaux locaux p-adiquement clos. Dans le contexte de [R1] et [B1] ils apparaissent comme fibres du faisceau structural (aussi appelé faisceau de Nash dans [BS]) accompagnant les spectres p-adiques. L'intérêt de nos axiomatisations provient de la simplicité des axiomes qui rendent compte des propriétés henséliennes. Dans le §2 nous donnons une axiomatisation d'une théorie d'anneaux locaux qui apparaît naturellement dans le contexte de la théorie des modèles des corps valués, et se trouve être une complétion d'une théorie du §1. Nous appelons ces anneaux, anneaux intègres p-adiquement clos.Dans le §3 nous utilisons §2 pour montrer que les anneaux intègres p-adiquement clos apparaissent aussi comme anneaux quotients d'anneaux de fonctions continues définissables sur les courbes affines p-adiques. Nous représentons alors un idéal premier comme le noyau d'un morphisme d'évaluation en un point non-standard de la courbe. Le spectre p-adique fournit un outil commode qui permet de décrire la situation de façon concise.
On generic elementary embeddings
Authors: Gitik Moti 
Published: May 2006

Suppose that I is a precipitous ideal over a cardinal κ and j is a generic embedding of I. What is the nature of j? If we assume the existence of a supercompact cardinal then, by Foreman, Magidor and Shelah [FMS], it is quite unclear where some of such j's are coming from. On the other hand, if ¬∃κ0(κ) = κ++, then, by Mitchell [Mi], the restriction of j to the core model is its iterated ultrapower by measures of it. A natural question arising here is if each iterated ultrapower of can be obtained as the restriction of a generic embedding of a precipitous ideal. Notice that there are obvious limitations. Thus the ultrapower of by a measure over λ cannot be obtained as a generic embedding by a precipitous ideal over κ ≠ λ. But if we fix κ and use iterated ultrapowers of which are based on κ, then the answer is positive. Namely a stronger statement is true:Theorem. Let τ be an ordinal and κ a measurable cardinal. There exists a generic extension V* of V so that NSℵ1 (the nonstationary ideal on ℵ1) is precipitous and, for every iterated ultrapower i of V of length ≤ τ by measures of V based on κ, there exists a stationary set forcing “the generic ultrapower restricted to V is i”.Our aim will be to prove this theorem. We assume that the reader is familiar with the paper [JMMiP] by Jech, Magidor, Mitchell and Prikry. We shall use the method of that paper for constructing precipitous ideals. Ideas of Levinski [L] for blowing up 2ℵ1 preserving precipitousness and of our own earlier paper [Gi] for linking together indiscernibles will be used also.
Two results on borel orders
Authors: Louveau Alain 
Published: May 2006

AbstractWe prove two results about the embeddability relation between Borel linear orders: For η a countable ordinal, let 2η (resp. 2< η) be the set of sequences of zeros and ones of length η (resp. < η), equipped with the lexicographic ordering. Given a Borel linear order X and a countable ordinal ξ, we prove the following two facts.(a) Either X can be embedded (in a (X, ξ) way) in 2ωξ or 2ωξ + 1 continuously embeds in X.(b) Either X can embedded (in a (X, ξ) way) in 2<ωξ or 2ωξ continuously embeds in X. These results extend previous work of Harrington, Shelah and Marker.