bluuebunny/crossref_metadata_2025_split huggingface dataset:
Systems of modal logic which are not unreasonable in the sense of Halldén
Authors: McKinsey J. C. C. 
Published: May 2006

Halldén, in [1], has recently pointed out that it is highly undesirable, in a system of sentential calculus, for there to exist two formulas α and β such that: (i) α and β contain no variable in common; (ii) neither α nor β is provable; (iii) α ∨ β is provable. We shall call a system unreasonable (in the sense of Halldén) if there exists a pair of formulas α and β having properties (i), (ii), and (iii). Halldén shows (in [1]) that the Lewis systems S1 and S3 are unreasonable in this sense; and that the same is true of any system which is between S1 and S3, as well as of every system which is stronger than S3 but weaker than both S4 and S7. In the present note we shall show that this defect does not occur in S4, nor in S5, nor in any “quasi-normal” extension of S5; we give an example, on the other hand, of an unreasonable system which lies between S4 and S5.When we speak, in what follows, of a system of modal logic, we shall mean a system having the same class of well-formed formulas as have the various Lewis calculi. Thus the well-formed formulas of a system of modal logic, when written in unabbreviated form, are just those formulas which can be built up from sentential variables by use of the binary connective ‘·’ (conjunction sign), and the two unary connectives ‘˜’ (negation sign) and ‘◇’ (possibility sign). We shall, however, also make use of some of the defined signs of Lewis.
On the independence of the axioms of definiteness (Axiome der Bestimmtheit)
Authors: Robinsohn Abraham 
Published: May 2006

The question of the independence of the axioms of the theory of sets has been dealt with in a number of works, although not in a final manner. The writer will be concerned solely with the axiomatic system of Zermelo and Fraenkel, and only with that feature of the system whereby all the objects of the underlying domain are sets (so that there is no difference between objects in general and sets in particular).A special place among the axioms is occupied by a purely relational one, an axiom of definiteness, which establishes the character of equality within the system.Zermelo introduces equality intensionally—if two symbolsxandyrepresent the same object, we write = (x, y). According to this there is no necessity for axioms to assure the interchangeability of equal objects as arguments of the primitive relationϵ( , ). For under the intensional interpretation it is clear that:Similarly it is clear that there is no necessity for a separate axiom that will assure to equality the properties of an equivalence relation. Therefore Zermelo introduces only the followingaxiom of extensionality:(if one set is a subset of another set, and the second set is also a subset of the first, then the two sets are equal).
A note on transfinite iteration
Authors: Schwarz Gideon 
Published: May 2006

For some of the well-known set-theoretic operations a natural definition of transfinite iterations (powers) seems impossible. If, however, an operator D has the property that, for every X, D(X) ⊃ X, we may write the formula Dn(X) = D(Dn−1(X)) (which defines as usual the finite powers of D) in the form . Assuming this formula to be valid when n is any ordinal, we obtain a natural definition of transfinite powers of those operators. Obviously the dual definition would work in the case D(X) ⊂ X.As an example of the use of this definition, we show how the sets used by von Neumann to represent ordinals can be constructed by means of the operator N(X) = X⋃{X}. Denoting the union of the elements of X by S(X), we have for the set E(ξ), which represents the ordinal ξ, E(ξ) = S(Nξ({ϕ})), as can easily be verified by transfinite induction. As the sets E(ξ) are different for different values of ξ, the powers of N are all different as well.This is not always the case. The powers of certain operators start repeating themselves from a certain ordinal onward. If an operator has the property that, for every set A of sets a, , then the sequence of its powers becomes constant already from ω on. This is a special case of the following theorem.
The consistency of Leśniewski's mereology relative to the real number system
Authors: Clay Robert E. 
Published: May 2006

It is known that Leśniewski constructed an interpretation of mereology in the real number system using binary expansions.2 Unfortunately, this construction is no longer extant. The following paper, except for a slight variation, is an attempt to reconstruct this interpretation.Leśniewski probably considered sequences of 0's and I's (except for the sequence of all 0's) and defined a first sequence as an element of the second if every place in which the first has a I, so also does the second.
Interpretations of Kleene's metamathematical predicate Γ ∣ a in intuitionistic arithmetic
Authors: Robinson T. Thacher 
Published: May 2006

Let Pp, Pd, and N be the intuitionistic systems of prepositional calculus, predicate calculus, and elementary arithmetic, respectively, described in [3].Kleene [4] introduces a metamathematical predicate Γ ∣ A for each of the systems Pp, Pd, and N, where Γ ranges over finite sequences of wffs, and A ranges over wffs, of that system. In the case of N, if Γ is consistent, then ‘ Γ ∣ A’ is essentially the result of deleting all references to recursive functions from the metamathematical predicate ‘A is realizable-(Γ ⊦)’ described in [3], pp. 502–503.Through use of this predicate, Kleene [4] obtains elegant constructive proofs of the following results for N:Metatheorem 0.1. If B ∨ C is a closed theorem of N, then ⊦ B or ⊦ C.Metatheorem 0.2. If (∃a)D(a) is a closed theorem of N, then there is a numeral n such that ⊦D(n).Metatheorem 0.3. If A is a closed wff of N, then A ∣ A is a necessary and sufficient condition that, for all closed B, C, (∃a)D(a) inN:(0.3.1) ⊦ A ⊃ B ∨ C implies ⊦ A ⊃ B or ⊦A ⊃ Cand(0.3.2) ⊦A ⊃ (∃)D(a) implies there is a numeral n such that ⊦ A ⊃ D(n).
Can there be no nonrecursive functions?
Authors: Moschovakis Joan Rand 
Published: May 2006

In 1936 Alonzo Church proposed the following thesis: Every effectively computable number-theoretic function is general recursive. The classical mathematician can easily give examples of nonrecursive functions, e.g. by diagonalizing a list of all general recursive functions. But since no such function has been found which is effectively computable, there is as yet no classical evidence against Church's Thesis.The intuitionistic mathematician, following Brouwer, recognizes at least two notions of function: the free-choice sequence (or ordinary number-theoretic function, thought of as the ever-finite but ever-extendable sequence of its values) and the sharp arrow (or effectively definable function, all of whose values can be specified in advance).
A note on S5
Authors: Castaneda Hector-Neri 
Published: May 2006

This is really a note to Wajsberg's [4].In [3] J. C. C. McKinsey proved the following two completeness theorems: (1) theorem 6: If A is a wff of S2 with just r (proper or improper) sub-wffs, then A is provable in S2 iff A is satisfied by every normal S2-matrix with no more than 22r+1 elements; (2) theorem 13: if A is a wff of S4 with just r sub-wffs, then A is provable in S4 iff A is satisfied by every normal S4-matrix with no more than 22r elements. Now, a similar theorem has not been explicitly formulated for S5, even though a similar, even simpler, theorem has been almost at hand since Wajsberg's [4] was published in 1933, namely:Theorem. If A is a wff of S5 with just n propositional variables, then A is provable in S5 iff A is satisfied by a normal SS-matrix with 22n elements.
Finite nest structures and propositional logic
Authors: Smullyan Raymond M. 
Published: May 2006

Our terminology and notation is the same as that of [1], of which this note is a sequel.We wish to show that if we take the natural deduction system (N) described in [1], and delete the rules for the quantifiers, we obtain a complete system for propositional logic. [Of course we now construe “X”, “Y”, “Z” as syntactic variables ranging over formulas of propositional logic, rather than sentences of quantification theory.] Moreover the system serves as a neat decision procedure.
Pure three-valued Łukasiewiczian implication
Authors: McCall Storrs , Meyer R. K. 
Published: May 2006

The matrix defining Łukasiewicz's three-valued logic, constructed in 1920 and described at length in [1], is the following:
This matrix was axiomatized in 1931 by Wajsberg (see [6]), who showed that the following axioms together with the rules of substitution and modus ponens were sufficient:
Axiomatizable theories with few axiomatizable extensions
Authors: Martin D. A. , Pour-El M. B. 
Published: May 2006

In this paper we prove two theorems. They answer questions raised by Myhill in 1956. (We recall the well-known fact that Myhill's invention of the maximal set in 1956 [2] stemmed from his attempt to prove I below.)I. There exists an axiomatizable, essentially undecidable theory in standard formalization such that all axiomatizable extensions of are finite extensions.II. There exists an axiomatizable but undecidable theory in standard formalization such that(a) has a consistent, complete, decidable extension ,(b) If is an axiomatizable extension of then either(i) is a finite extension of , or(ii) is a finite extension of .
Many-valued logics of extended Gentzen style II
Authors: Takahashi Moto-o 
Published: May 2006

In the monograph [1] of Chang and Keisler, a considerable extent of model theory of the first order continuous logic (that is, roughly speaking, many-valued logic with truth values from a topological space) is ingeniously developed without using any notion of provability.In this paper we shall define the notion of provability in continuous logic as well as the notion of matrix, which is a natural extension of one in finite-valued logic in [2], and develop the syntax and semantics of it mostly along the line in the preceding paper [2]. Fundamental theorems of model theory in continuous logic, which have been proved with purely model-theoretic proofs (i.e. those proofs which do not use any proof-theoretic notions) in [1], will be proved with proofs which are natural extensions of those in two-valued logic.
The diversity of quantifier prefixes
Authors: Keisler H. Jerome , Walkoe Wilbur 
Published: May 2006

The Arithmetical Hierarchy Theorem of Kleene [1] states that in the complete theory of the standard model of arithmetic there is for each positive integer r a Σr0 formula which is not equivalent to any Πr0 formula, and a Πr0 formula which is not equivalent to any Πr0 formula. A Πr0 formula is a formula of the formwhere φ has only bounded quantifiers; Πr0 formulas are defined dually.The Linear Prefix Theorem in [3] is an analogous result for predicate logic. Consider the first order predicate logic L with identity symbol, countably many n-placed relation symbols for each n, and no constant or function symbols. A prefix is a finite sequenceof quantifier symbols ∃ and ∀, for example ∀∃∀∀∀∃. By a Q formula we mean a formula of L of the formwhere v1, …, vr are distinct variables and φ has no quantifiers. A sentence is a formula with no free variables. The Linear Prefix Theorem is as follows.Linear Prefix Theorem. Let Q and q be two different prefixes of the same length r. Then there is a Q sentence which is not logically equivalent to any q sentence.Moreover, for each s there is a Q formula with s free variables which is not logically equivalent to any q formula with s free variables.For example, there is an ∀∃∀∀∀∃ sentence which is not logically equivalent to any ∀∃∃∀∀∃ sentence, and vice versa. Recall that in arithmetic two consecutive ∃'s or ∀'s can be collapsed; for instance all ∀∃∀∀∀∃ and ∀∃∃∀∀∃ formulas are logically equivalent to Π40 formulas. But the Linear Prefix Theorem shows that in predicate logic the number of quantifiers in each block, as well as the number of blocks, counts.
On degrees of unsolvability and complexity properties
Authors: Marques Ivan 
Published: May 2006

In this paper we present two theorems concerning relationships between degrees of unsolvability of recursively enumerable sets and their complexity properties.The first theorem asserts that there are nonspeedable recursively enumerable sets in every recursively enumerable Turing degree. This theorem disproves the conjecture that all Turing complete sets are speedable, which arose from the fact that a rather inclusive subclass of the Turing complete sets, namely, the subcreative sets, consists solely of effectively speedable sets [2]. Furthermore, the natural construction to produce a nonspeedable set seems to lower the degree of the resulting set.The second theorem says that every speedable set has jump strictly above the jump of the recursive sets. This theorem is an expected one in view of the fact that all sets which are known to be speedable jump to the double jump of the recursive sets [4].After this paper was written, R. Soare [8] found a very useful characterization of the speedable sets which greatly facilitated the proofs of the results presented here. In addition his characterization implies that an r.e. degree a contains a speed-able set iff a′ > 0′.
Ordinal spectra of first-order theories
Authors: Schlipf John Stewart 
Published: May 2006

The notion of the next admissible set has proved to be a very useful notion in definability theory and generalized recursion theory, a unifying notion that has produced further interesting results in its own right. The basic treatment of the next admissible set above a structure ℳ of urelements is to be found in Barwise's [75] book Admissible sets and structures. Also to be found there are many of the interesting characterizations of the next admissible set. For further justification of the interest of the next admissible set the reader is referred to Moschovakis [74], Nadel and Stavi [76] and Schlipf [78a, b, c].One of the most interesting single properties of is its ordinal (ℳ). It coincides, for example, with Moschovakis' inductive closure ordinal over structures ℳ with pairing functions—and over some, such as algebraically closed fields of characteristic 0, without pairing functions (by recent work of Arthur Rubin) (although a locally famous counterexample of Kunen, a theorem of Barwise [77], and some recent results of Rubin and the author, show that the inductive closure ordinal may also be strictly smaller in suitably pathological structures). Further justification for looking at (ℳ) alone may be found in the above-listed references. Loosely, we can consider the size of to be a useful measure of the complexity of ℳ. One of the simplest measures of the size of —and yet a very useful measure—is its ordinal, (ℳ). Keisler has suggested thinking of (ℳ) as the information content of a model—the supremum of lengths of wellfounded relations characterizable in the model.
Sets equipollent to their power set in NF
Authors: Boffa Maurice 
Published: May 2006

In this note we define a class of properties for which the following holds: If we can prove in NF that the property holds for the universe V, then we can prove in NF that it holds for every set equipollent to its power set.Definition. For any stratified formula A and any variable υ which does not occur in A, let Aυ be the formula obtained by replacing in A each quantifier (Qx) by the bounded quantifier (Qx ∈ SCi(υ)), where i is the type of x in A. We will say that a property P(υ) is typed when there is a stratified sentence S such that P(υ) ↔ Sυ holds in NF.Examples of typed properties are: “υ is Dedekind-infinite”, “υ is not well-orderable”. Specker [3] proved that these typed properties hold for the universe V, and C. Ward Henson [1] extended this result to any set equipollent to its power set. We will show that such an extension holds for any typed property.Theorem. For any typed property P(υ):Proof. Fix a bijective map h: υ → SC(υ) and define for i = 0, 1, 2, …, n, … a bijective map hi: υ → SCi(υ) as follows:For every formula A, let A(h) be obtained by replacing in A each atomic part (x ∈ y) by (x ∈ h(y)) and each quantifier (Qx) by (Qx ∈ υ).
Projective algebra and the calculus of relations
Authors: Bednarek A. R. , Ulam S. M. 
Published: May 2006

In [1] there were given postulates for an abstract “projective algebra” which, in the words of the authors, represented a “modest beginning for a study of logic with quantifiers from a boolean point of view”. In [5], D. Monk observed that the study initiated in [1] was an initial step in the development of algebraic versions of logic from which have evolved the cylindric and polyadic algebras.Several years prior to the publication of [1], J. C. C. McKinsey [3] presented a set of postulates for the calculus of relations. Following the publication of [1], McKinsey [4] showed that every projective algebra is isomorphic to a subalgebra of a complete atomic projective algebra and thus, in view of the representation given in [1], every projective algebra is isomorphic to a projective algebra of subsets of a direct product, that is, to an algebra of relations.Of course there has since followed an extensive development of projective algebra resulting in the multidimensional cylindric algebras [2]. However, what appears to have been overlooked is the correspondence between the Everett–Ulam axiomatization and that of McKinsey.It is the purpose of this paper to demonstrate the above, that is, we show that given a calculus of relations as defined by McKinsey it is possible to introduce projections and a partial product so that this algebra is a projective algebra and conversely, for a certain class of projective algebras it is possible to define a multiplication so that the resulting algebra is McKinsey's calculus of relations.
Equality in
Authors: Seldin Jonathan P. 
Published: May 2006

In [CLg. II, §15B6], the problem of representing equality in the system by means of an ob Q is discussed; it is shown there that if Q is taken to be a canonical atom of degree 2 and if the axiom schemeis postulated, then it follows by Rule Eq thatand, if no other properties are postulated for Q, then the converse of (1), Q-consistency, also holds. However, it is also desirable to have, in addition, the propertyat least for some obs Z, and the statement is made in [CLg. II, §15B6] that no known way of incorporating this principle existed (at the time this statement was written) in such a way that there was a proof of Q-consistency. In this paper it is shown that if Z is restricted to be a basic canob of degree 1, i.e., if Z is restricted to be a predicate of one argument, then a system in which (2) is postulated can be proved Q-consistent.The notations and conventions of [CLg. II] especially §15B, will be used throughout the paper.
A converse of the Barwise completeness theorem
Authors: Stavi Jonathan 
Published: May 2006

In this paper a converse of Barwise's completeness theorem is proved by cut-elimination considerations applied to inductive definitions. We show that among the transitive sets T satisfying some weak closure conditions (closure under primitive-recursive set-functions is more than enough), only the unions of admissible sets satisfy Barwise's completeness theorem in the form stating that if φ ∊ T is a sentence which has a derivation (in the universe) then φ has a derivation in T. See §1 for the origin of the problem in Barwise's paper [Ba].Stated quite briefly the proof is as follows (a step-by-step account including relevant definitions is given in the body of the paper):Let T be a transitive prim.-rec. closed set, and let is nonempty, transitive and closed under pairs}. For each let κ(A) be the supremum of closure ordinals of first-order positive operators on subsets of A (first-order with respect to By Theorem 1 of [BGM], it is enough to prove that rank(T) in order to obtain that T is a union of admissible sets. (The rank of a set is defined by rank(x) = supy ∊ x (rank(y) + 1); since T is prim.-rec. closed, rank(T) = smallest ordinal not in T.)Let We show how to find in T (in fact, in Lω(A)) a derivable sentence τ that has no derivation D such that rank(D) ≤ α. Thus, if τ is to have a derivation in T, rank(T) > α. α is arbitrary (< κ(A)), so rank(T) ≥ κ(A). Q.E.D.
The relation of A to Prov ˹A˺ in the Lindenbaum sentence algebra
Authors: Kent C. F. 
Published: May 2006

Let U be a consistent axiomatic theory containing Robinson's Q [TMRUT, p. 51]. In order for the results below to be of interest, U must be powerful enough to carry out certain arguments involving versions of the “derivability conditions,” DC(i) to DC(iii) below, of [HBGM, p. 285], [F60, Theorem 4.7], or [L55]. Thus it must contain, at least, mathematical induction for formulas whose prenex normal forms contain at most existential quantifiers. For convenience, U is assumed also to contain symbols for primitive recursive functions and relations, and their defining equations. One of these is used to form the standard provability predicate, Prov ˹A˺, “there exists a number which is the Gödel number of a proof of A.” Upper corners denote numerals for Gödel numbers for the enclosed sentences, and parentheses are often omitted in their presence.This paper contains some results concerning the relation between the sentence A, and the sentence Prov ˹A˺ in the Lindenbaum Sentence Algebra (LSA) for U, the Boolean algebra induced by the pre-order relation A ≤ B ⇔ ⊦A → B. Half of the answer is provided by a theorem of Löb [L55], which states that ⊦Prov ˹A˺ → A ⇔ ⊦A. Hence, in the presence of DC(iii), below, it is never true that Prov ˹A˺ < A in the LSA. However, there is a large and interesting set of sentences, denoted here by Γ, for which A < Prov ⌜A⌝.
The word problem for free fields
Authors: Cohn P. M. 
Published: May 2006

It has long been known that every free associative algebra can be embedded in a skew field [11]; in fact there are many different embeddings, all obtainable by specialization from the ‘universal field of fractions’ of the free algebra (cf. [5, Chapter 7]). This makes it reasonable to call the latter the free field; see §2 for precise definitions. The existence of this free field was first established by Amitsur [1], but his proof is rather indirect and does not provide anything like a normal form for the elements of the field. Actually one cannot expect to find such a normal form, since it does not even exist in the field of fractions of a commutative integral domain, but at least one can raise the word problem for free fields: Does there exist an algorithm for deciding whether a given expression for an element of the free field represents zero?Now some recent work has revealed a more direct way of constructing free fields ([4], [5], [6]), and it is the object of this note to show how this method can be used to solve the word problem for free fields over infinite ground fields. In this connexion it is of interest to note that A. Macintyre [9] has shown that the word problem for skew fields is recursively unsolvable. Of course, every finitely generated commutative field has a solvable word problem (see e.g. [12]).The construction of universal fields of fractions in terms of full matrices is briefly recalled in §2, and it is shown quite generally for a ringRwith a field of fractions inverting all full matrices, that if the set of full matrices overRis recursive, then the universal field has a solvable word problem. This holds more generally if the precise set of matrices overRinverted over the field is recursive, but it seems difficult to exploit this more general statement.