bluuebunny/crossref_metadata_2025_split huggingface dataset:
Widerspruchsfreier Aufbau der Logik I
Authors: Ackermann Wilhelm 
Published: May 2006

Die vorliegenden Untersuchungen haben sich aus solchen entwickelt, die ich an andrer Stelle früher veröffentlichte. Die Kenntnis dieser früheren Arbeit wird in keiner Weise hier vorausgesetzt und ist für das folgende unwesentlich. Es sei mir jedoch gestattet, für den Kenner der früheren Arbeit einige Bemerkungen voraufzuschicken. In der genannten Arbeit hatte ich, angeregt ursprünglich durch Gedankengänge von Herrn Behmann, ein typenfreies System der Logik aufgebaut, das allein auf dem Gedanken fußte, daß der Definitionsbereich der Prädikate im allgemeinen beschränkt ist, sodaß nur bestimmte Zusammenstellungen von Prädikaten und Dingen sinnvolle, d.h. wahre oder falsche Aussagen ergeben, und das diesen Gesichtspunkt meiner Meinung nach konsequent durchführte. Eine anschließende Arbeit sollte dann die Widerspruchsfreiheit des Systems untersuchen. Diese Untersuchung ist inzwischen geschehen. Es zeigte sich, daß sich die Widerspruchsfreiheit des Systems nur dann beweisen ließ, falls die in ihm enthaltene Vollständigkeit von → die sich durch das Bestehen eines Deduktionstheorems zeigte, fallen gelassen wurde. Die Grundformeln (13) und (14) mußten wegbleiben. Die Widerspruchsfreiheit des restlichen Systems ließ sich dann durch eine dem System eigentümliche Methode der Beweistransformation zeigen.Diese anschließienden Untersuchungen, die ihrer Zeit nicht mehr veröffentlicht werden konnten, sind inzwischen durch die vorliegenden überholt. Es war das Unbefriedigende bei dem genannten Aufbau, daß hinterher doch wieder eine Einschränkung gemacht werden mußte, die sich nicht aus den zugrunde gelegten Prinzipien ergab, sondern von ihnen aus unvorhergesehen war. Diese Einschränkung bewirkte übrigens, daß keine volle Zahlentheorie in dem System zu gewinnen war.
Another variant of natural deduction
Authors: Copi Irving M. 
Published: May 2006

Since 1934 various different techniques for natural deduction have been developed by Gentzen, Jaśkowski, Rosser, Quine, and others (see [1], pp. 147–167; [2], especially footnotes 1, 3, and 4; and [3], pp. 75-83, 96-107, and 289-294). It has been pointed out to me by Professor Donald Kalish of U.C.L.A. that the restrictions placed upon Universal Generalization (UG) and Existential Instantiation (EI) in [3] force one to construct a less natural proof than seems desirable for such arguments as(cf. [3], p. 139, and [1], pp. 175f.) It is my purpose in this note to formulate an alternative restriction on UG which will permit a more natural proof for such arguments, and to prove the consistency of the altered rule.In the notation of [3], “The expression ‘Φμ’ will denote any propositional function in which there is at least one free occurrence of the variable denoted by ‘μ’. The expression ‘Φν’ will denote the result of replacing all free occurrences of μ in Φμ by ν, with the added proviso that when ν is a variable it must occur free in Φν at all places at which μ occurs free in Φμ.” ([3], p. 100.) The statement of EI is relatively unrestricted; beingprovided that ν is a variable which occurs free in no earlier step.” ([3], p. 104.)
On the definition of ‘formal deduction’
Authors: Montague Richard , Henkin Leon 
Published: May 2006

The following remarks apply to many functional calculi, each of which can be variously axiomatized, but for clarity of exposition we shall confine our attention to one particular system Σ. This system is to have the usual primitive symbols and formation rules of the pure first-order functional calculus, and the following formal axiom schemata and formal rules of inference.Axiom schema 1. Any tautologous wff (well-formed formula).Axiom schema 2. (a) A ⊃ B, where A is any wff, a and b are any individual variables, and B arises from A by replacing all free occurrences of a by free occurrences of b.Axiom schema 3. (a)(A ⊃ B)⊃(A⊃ (a)B). where A and B are any wffs, and a is any individual variable not free in A.Rule of Modus Ponens: applies to wffs A and A ⊃ B, and yields B.Rule of Generalization: applies to a wff A and yields (a)A, where a is any individual variable.A formal proof in Σ is a finite column of wffs each of whose lines is a formal axiom or arises from two preceding lines by the Rule of Modus Ponens or arises from a single preceding line by the Rule of Generalization. A formal theorem of Σ is a wff which occurs as the last line of some formal proof.
Investigation of the equivalence of the axiom of choice and Zorn's lemma from the viewpoint of the hierarchy of types
Authors: Büchi J. Richard 
Published: May 2006

It is a well known fact that Zermelo's Axiom of Choice and Zorn's Lemma are equivalent logical assumptions. However, an investigation from the viewpoint of the hierarchy of types reveals a complication in the nature of this equivalence. In a type-theoretical formalism both postulates enter as spectra (ZAα) and (ZLα) of formulas, where ZAα is Zermelo's Axiom and ZLα is Zorn's Lemma stated for variables of a fixed type α. The complication has its origin in the fact that, although the formula ZAα implies ZLα, in order to deduce ZAα it seems to be necessary to assert Zorn's Lemma ZLβ for a type β which is higher than α. In other words, we don't know a proof assuring the equivalence of the two formulas ZAα and ZLα. Therefore the equivalence of Zermelo's Axiom and Zorn's Lemma has to be understood in the sense that the assertion of the formulas ZAα for all types α implies every one of the formulas ZLβ and conversely the assertion of the spectrum of formulas (ZLα) implies every one of the formulas ZAβ.In § 3 we shall indicate a type β which makes the deduction of ZAα from ZLβ possible. For this purpose a proof by G. Birkhoff [3] is translated into type-theoretical language.In § 2 it is shown that ZAα implies ZLα. In this proof no use is made of the notion of well-ordering. Specifically, we do not first deduce the Well-Ordering Theorem as it is usually done in proving Zorn's Lemma from Zermelo's Axiom. However, the method is suggested by Zermelo's second proof of the Well-Ordering Theorem [2].
On the interpretation of intuitionistic number theory
Authors: Kleene S. C. 
Published: May 2006

The purpose of this article is to introduce the notion of “recursive realizability.”Let P be some property of natural numbers. Consider the existential statement, “There exists a number n having the property P.” To explain the meaning which this has for a constructivist or intuitionist, it has been described as a partial judgement, or incomplete communication of a more specific statement which says that a certain given number n, or the number n obtainable by a certain given method, has the property P. The meaning of the existential statement thus resides in a reference to certain information, which it implies could be stated in detail, though the trouble is not taken to do so. Perhaps the detail is suppressed in order to convey a general view of some fact.The information to which reference is made should be thought of as possibly comprising other items besides the value of n or method for obtaining it, namely such items as may be necessary to complete the communication that that n has the property P.
Correction to A note on the Entscheidungsproblem
Authors: Church Alonzo 
Published: May 2006

In A note on the Entscheidungsproblem the author gave a proof of the unsolvability of the general case of the Entscheidungsproblem of the engere Funktionenkalkül. This proof, however, contains an error, in order to correct which it is necessary to modify the “additional axioms” of the system L so that they contain no free variables (either free individual variables or free propositional function variables).The additional axioms of L other than x=y→[F(x)→F(y)] contain no free propositional function variables, and hence it is sufficient to replace each one by an expression obtained from it by quantifying all the individual variables by means of universal quantifiers initially placed—thus, in particular, x = x is replaced by (x)[x=x]. Moreover the axiom x=y→[F(x)→F(y)] may be replaced by the following set of axioms:and similar axioms for each of the functions b1, b2, …, bk.
Identity, variables, and impredicative definitions
Authors: Jaakko K. , Hintikka J. 
Published: May 2006

Recent discussion serves to bring out, amply and convincingly, the utility of observing the ordinary correct use of words and phrases for the purpose of clearing up philosophical problems. In this paper, I shall endeavour to show, by means of an example, that the reverse method may have its interest, too. An attempt will be made to cultivate a minor deviation from the accepted ways of using certain words and phrases in idiomatic English as well as in the formalized “languages” of the logicians. The words and phrases in question are those for the formalization of which a logician employs (free or bound) variables. Cases in point are the words customarily called quantifiers. The deviation I have in mind affects the relation of these words to the notion of identity. The deviation is illustrated by the following sentences:(1a) Any two points of a straight line completely determine that line;(2a) He is John's brother if he has the same parents as John;(3a) Mazzini did more for the emancipation of his country than any living man of his time.These examples may be contrasted with the following closely related sentences:(1b) Any two distinct points of a straight line completely determine that line;(2b) He is John's brother if he has the same parents as John and if he is not John himself;(3b) Mazzini did more for the emancipation of his country than any other living man of his time.
The inconsistency of certain formal logics
Authors: Curry Haskell B. 
Published: May 2006

A proof that certain systems of formal logic are inconsistent, in the sense that every formula expressible in them is provable, was published by Kleene and Rosser under the above title in 1935. For the case where the underlying system satisfies an additional condition—viz. the possession of an operator analogous to Schönfinkel's K—I gave a simpler derivation of this condition in a previous paper. That argument, like the original one of Kleene and Rosser, was a refinement of the Richard paradox. The object of the present paper is to show that, if we use other paradoxes, an inconsistency will result from a very much simpler argument and on much less restrictive hypotheses. The contradiction can no longer be called “the paradox of Kleene and Rosser,” because it is based on an entirely different principle; but, in deference to the work of the original discoverers of the inconsistency, the paper is given the same title as that which their paper bears. The central idea of the new derivation was suggested by some work of R. Carnap.This paper is based on the one above cited, which will be referred to as PKR. However, acquaintance with that paper will be presupposed only through 3.4, i.e., through the statement of the basic hypotheses and conventions for a combinatorially complete system—except that for the second (alternative) method of construction given below the substance of PKR through 9.6 is needed.
Logical truth and logical implication
Authors: Hatcher William S. 
Published: May 2006

In [1], page 85, Quine states: “… ponentials of logically true statements are logically true.” It is perhaps of some interest that this assertion is not completely precise as can be seen from counterexamples. One simple example is the following:Let L be some language in which ‘c’ and ‘b’ are atomic sentential constants. Let ‘c’ be false and ‘b’ true. Suppose that L includes parentheses and the material conditional ‘⊃’ as logical notation, but that ‘b’, at least, counts as extra-logical.
Algebraic semantics for modal logics II
Authors: Lemmon E. J. 
Published: May 2006

This paper is a sequel to [7], and the terminology of [7] is largely presupposed here. In [7], the algebraic methods of McKinsey-Tarski were employed and extended to yield semantic results of a Kripke kind for a class of relatively weak modal logics, the strongest of which was the Feysvon Wright system T. Deontic versions of both T and E2, called T(D) and D2, and even weaker systems, were handled. The main aim of the present paper is to extend these results to stronger systems of modal logic. Thus the Lewis systems S2–S5, the Brouwersche system B of Kripke [4], the systems E3–E5 of [5], and Łukasiewicz's modal logic, as well as certain new systems, are considered.Certain modifications of the method of [7] have proved convenient. Thus in Section I, some further results concerning model structures are proved in order that the relationship between S2 and E2, S3 and E3, can be properly stated; in particular, the notions of a refined and connected model structure play a pervasive role throughout.
Analytic natural deduction
Authors: Smullyan Raymond M. 
Published: May 2006

We consider some natural deduction systems for quantification theory whose only quantificational rules involve elimination of quantifiers. By imposing certain restrictions on the rules, we obtain a system which we term Analytic Natural Deduction; it has the property that the only formulas used in the proof of a given formula X are either subformulas of X, or negations of subformulas of X. By imposing further restrictions, we obtain a canonical procedure which is bound to terminate, if the formula being tested is valid. The procedure (ultimately in the spirit of Herbrand [1]) can be thought of as a partial linearization of the method of semantical tableaux [2], [3]. A further linearization leads to a variant of Gentzen's system which we shall study in a sequel.The completeness theorem for semantical tableaux rests essentially on König's lemma on infinite graphs [4]. Our completeness theorem for natural deduction uses as a counterpart to König's lemma, a lemma on infinite “nest structures”, as they are to be defined. These structures can be looked at as the underlying combinatorial basis of a wide variety of natural deduction systems.In § 1 we study these nest structures in complete abstraction from quantification theory; the results of this section are of a purely combinatorial nature. The applications to quantification theory are given in § 2.
On analytic well-orderings
Authors: Tanaka Hisao 
Published: May 2006

Since about 1955, recursive, (hyper-)arithmetic and well-orderings have been investigated by many authors. Now we shall generally consider analytic well-orderings and compare their representation-capacities for ordinals.Let K be a class of predicates. Then, R is called a Kwell-ordering if R is a binary relation of natural numbers belonging to the class K and satisfies the following conditions:(i) R(x, y) ∧ R(y, x) → x = y;(ii) x, y ∈ D(R) → R(x, y) ∨ R(y, x), where D(R) is the domain of R, that is to say, the set {x ∣ (∃y)[R(x, y) ∨ R(y, x)]};(iii) R(x, y) ∧ R(y, z) → R(x, z);(iv) .
The decision problem for formulas in prenex conjunctive normal form with binary disjunctions
Authors: Krom M. R. 
Published: May 2006

In [8] S. J. Maslov gives a positive solution to the decision problem for satisfiability of formulas of the formin any first-order predicate calculus without identity where h, k, m, n are positive integers, αi, βi are signed atomic formulas (atomic formulas or negations of atomic formulas), and ∧, ∨ are conjunction and disjunction symbols, respectively (cf. [6] for a related solvable class). In this paper we show that the decision problem is unsolvable for formulas that are like those considered by Maslov except that they have prefixes of the form ∀x∃y1 … ∃yk∀z. This settles the decision problems for all prefix classes of formulas for formulas that are in prenex conjunctive normal form in which all disjunctions are binary (have just two terms). In our concluding section we report results on decision problems for related classes of formulas including classes of formulas in languages with identity and we describe some special properties of formulas in which all disjunctions are binary including a property that implies that any proof of our result, that a class of formulas is a reduction class for satisfiability, is necessarily indirect. Our proof is based on an unsolvable combinatorial tag problem.
Postulates for implicational calculi
Authors: Meredith C. A. 
Published: May 2006

I. (Bull's system OIC, defined in [1] as positive implication plus ССССpqqrСССpqrr, can be axiomatised by adding this to a weaker base.)1. СpСqp2. ССpqССqrСpr3. ССССpqqrСССpqrr4. ССССqrСprsССpqs = D225. ССrСpqСССpqСrqСrq = D436. СССССpqССrqСrqsССrСpqs = D257. ССpСqrССpqСpr = D64
Construction of models for algebraically generalized recursive function theory
Authors: Strong H. R. 
Published: May 2006

AbstractThe Uniformly Reflexive Structure was introduced by E. G. Wagner who showed that the theory of such structures generalized much of recursive function theory. In this paper Uniformly Reflexive Structures are constructed as factor algebras of free nonassociative algebras. Wagner's question about the existence of a model with no computable splinter (“successor set”) is answered in the affirmative by the construction of a model whose only computable sets are the finite sets and their complements. Finally, for each countable Boolean algebra R of subsets of a countable set which contains the finite subsets, a model is constructed with R as its family of computable sets.
Strong partition properties for infinite cardinals
Authors: Kleinberg E. M. 
Published: May 2006

The notion of a “partition relation”, as it has been studied in the context of set theory for the past several years, was inspired by the following theorem of F. P. Ramsey [14]:Theorem 0.1. Let n be a positive integer and let {A, B} be a partition of those subsets of the nonnegative integers containing exactly n elements. Then there exists an infinite subset x of the nonnegative integers all of whose n-element subsets are contained in only one of A or B. (Any such set x is said to be “homogeneous” for the partition.)
Remarks on an infinitary language with constructive formulas
Authors: Lopez-Escobar E. G. K. 
Published: May 2006

It is well known that L, the first-order predicate calculus, is unsuitable for characterizing certain mathematical structures. Since some of those structures are quite often considered by mathematicians, extensions of L have been considered which (partially) solve the above problem. Roughly speaking, the extensions of L fall into two main categories:(I) extensions obtained by allowing higher order variables, and(II) extensions obtained by allowing infinitely long formulas.
A proof of zermelo's theorem
Authors: Dévidé Vladimir 
Published: May 2006

We give a short proof of the theorem that, assuming the axiom of choice, every set can be well-ordered. The proof makes direct use of neither induction nor ordinals.Let S be any given set and its power-set. Let be a choice function, i.e. we denote Ζ — {γΖ} by Ζ'.
Turing degrees and many-one degrees of maximal sets
Authors: Lerman Manuel 
Published: May 2006

Martin [4, Theorems 1 and 2] proved that a Turing degree a is the degree of a maximal set if, and only if, a′ = 0″. Lachlan has shown that maximal sets have minimal many-one degrees [2, §1] and that every nonrecursive r.e. Turing degree contains a minimal many-one degree [2, Theorem 4]. Our aim here is to show that any r.e. Turing degree a of a maximal set contains an infinite number of maximal sets whose many-one degrees are pairwise incomparable; hence such Turing degrees contain an infinite number of distinct minimal many-one degrees. This theorem has been proved by Yates [6, Theorem 5] in the case when a = 0′.The need for this theorem first came to our attention as a result of work done by the author [3, Theorem 2.3]. There we looked at the structure / obtained from the recursive functions of one variable under the equivalence relation f ~ g if, and only if, f(x) = g(x) a.e., that is, for all but finitely many x ∈ , where M is a maximal set, and M is its complement. We showed that /1 ≡ /2 if, and only if, 1 =m2, i.e., 1. and 2 have the same many-one degree. However, it might be possible that some Turing degree of a maximal set contains exactly one many-one degree of a maximal set. Theorem 1 was proved to show that this was not the case, and hence that the theory of / is not an invariant of Turing degree.
What is strict implication?
Authors: Hacking Ian 
Published: May 2006

C. I. Lewis intended his systems S1–S5 as contributions to the study of “strict implication”, but in his formulation, strict implication is so thoroughly intertwined with other notions, such as possibility and negation, that it remains a problem, to separate out the properties of strict implication itself. I shall solve this problem for S2–5 and von Wright's M. The results for S3–5 are given below, while the implicative parts of S2 and M, which are rather more complicated, are given in §5.In this presentation, ‘⊃’ stands for strict implication, and missing brackets for ‘⊃’ are restored by associationtothe right. Astrictformula is one of the form A ⊃ B. Axiom schemes are used throughout.
Logical connectives for intuitionistic propositional logic
Authors: McCullough Dean P. 
Published: May 2006

In classical propositional logic it is well known that {7, ⊃ } is a functionally complete set with respect to a two-valued truth function modeling. I.e. all definable logical connectives are definable from 7 and ⊃. Other modelings of classical type propositional logics may have different functionally complete sets; for example, multivalued truth function modelings.This paper examines the question of a functionally complete set of logical connectives for intuitionistic propositional logic with respect to S. Kripke's modeling for intuitionistic logic.
On the derivability of instantiation properties
Authors: Friedman Harvey 
Published: May 2006

AbstractEvery recursively enumerable extension of arithmetic which obeys the disjunction property obeys the numerical existence property [Fr, 1]. The requirement of recursive enumerability is essential. For extensions of intuitionistic second order arithmetic by means of sentences (in its language) with no existential set quantifiers, the numerical existence property implies the set existence property. The restriction on existential set quantifiers is essential. The numerical existence property cannot be eliminated, but in the case of finite extensions of HAS, can be replaced by a weaker form of it. As a consequence, the set existence property for intuitionistic second order arithmetic can be proved within itself.
Experimental logics and Π30 theories
Authors: Hájek Petr 
Published: May 2006

In this paper we are going to consider experimental logics introduced by Jeroslow [4] as models of human reasoning proceeding by trial and error, i.e. admitting changes of axioms in time (some axioms are deleted, some new ones accepted). Jeroslow's notion is based on the idea that events which may cause changes in axioms and rules of reasoning are mechanical. Suppose a finite alphabet Γ to be fixed and let Γ* be the set of words in the alphabet Γ. N denotes the set of natural numbers.0.1. Definition. An experimental logic is a recursive relation H ⊆ N × Γ*; H(t, φ) is read “the expression is accepted at the point of time t”. φ is recurring w.r.t. H (notation: RecH(φ)) if H(t, φ) holds for infinitely many t; is stable w.r.t. H (notation: StblH(φ)) if H(t,φ) holds for all but finitely many t. In symbols:H is convergent if every recurring expression is stable.0.2. We have the following facts: Let X ∈ Γ*. (1) X ∈ iff there is an experimental logic H such that X = {φ; RecH(φ)}- (2) X ∈ iff there is an experimental logic H such that X = {φ; StblH(φ)}. (3) X ∈ iff there is a convergent experimental logic H such that X is the set of all expressions recurring ( = stable) w.r.t. H. (See [4], [3], [7]; cf. also [5].)