Search

In [3] a definition of negation was presented for the system K' of extended basic logic [1], but it has since been shown by Peter Päppinghaus (personal communication) that this definition fails to give rise to the law of double negation as I claimed it did. The purpose of this note is to revise this defective definition in such a way that it clearly does give rise to the law of double negation, as well as to the other negation rules of K'.Although Päppinghaus's original letter to me was dated September 19, 1972, the matter has remained unresolved all this time. Only recently have I seen that there is a simple way to correct the definition. I am of course very grateful to Päppinghaus for pointing out my error in claiming to be able to derive the rule of double negation from the original form of the definition.The corrected definition will, as before, use fixed-point operators to give the effect of the required kind of transfinite induction, but this time a double transfinite induction will be used, somewhat like the double transfinite induction used in [5] to define simultaneously the theorems and antitheorems of system CG.

It will be shown that system Qof [1], with minor corrections, is free from contradiction and can be strengthened in various ways without destroying its consistency.By the system C*Awill be meant the system that results in place of CAif rule 3.4.10 is omitted in [2] from the rules 3.4 defining PAand RAfor an arbitrary class Aof equations. We let P*Abe the theorems of C*Aand R*Abe the antitheorems of C*A, just as PAand RAare respectively the theorems and antitheorems of CAin [2]. Similarly G* is the class that is defined exactly like the class Gin 4.18 of [2] except that systems of the form C*Areplace those of the form CA. The terminology and conventions of [2] will be assumed in what follows.Using the methods that were used to show in 5.9 of [2] that CGis free from contradiction, it is easy to show that C*Ais free from contradiction for every class Aof equations. (The fact that rule 3.4.10 is omitted causes the proof of consistency to work even for cases where Ais not systematically closed in the sense of 4.11 of [2].)Just as it was shown in 4.19 of [2] that Gis systematically closed (in the sense of 4.11 of [2]), so also it clearly can be shown that G* is systematically closed. This means, in effect, that the rule of substitution of equals for equals holds in the system C*G*.

In a previous paper [9] a demonstrably consistent type-free system of combinatory logic C? was presented. This system contained a moderately strong exten-sionality principle, the usual equations of combinatory logic, Boolean propositional connectives, unrestricted quantifiers, an unrestricted abstraction principle (“comprehension axiom”), and a limited principle of excluded middle. It also contained elementary arithmetic in its entirety, avoiding arithmetical Gödel incompleteness [14] by being ?-complete. C? probably can be shown to contain certain important parts of mathematical analysis, such as the theory of continuous functions, which are contained by the somewhat similar (but nonextensional) system K' [6], [7]. A stronger system CG, having these same properties and more, will be formulated in the present paper. Elsewhere [13] it will be shown that the system Qof my book, Elements of combinatory logic(Yale University Press, New Haven and London, 1974), referred to below as ECL, is essentially a subsystem of CG, so that the consistency of CG guarantees that of Q.CGwill be stronger than both C? and Qin having an operator ‘?’ (inverted Greek iota) which denotes the inverse of equality in the sense that ‘?(= a) = a’ is a theorem of the system. Thus ‘?’ denotes a function or operator which operates on a unit class to give the only member of that class. (Here ‘=a’ denotes the unit class whose only member is denoted by ‘a’.) If uninverted Greek iota, ‘?’, is used as an abbreviation for ‘=’, the above equation could be written as ‘?(?a) = a’. Here ‘?a’ is analogous to Bertrand Russell's well-known notation ‘?a’, denoting a unit class. This same operator ‘?’ makes it possible to transform one-many or many-one relations into the corresponding functions or operators, a kind of transformation not usually available in systems of combinatory logic [1], [2]. It also provides a method for restricting functions by restricting the corresponding relations.

In this paper it will be shown that the fundamental modal functions (“… is necessary,” “… is possible,” etc.) may be represented in the ordinary two-valued logic of propositions, relatively to a subset Sof the set Kof all propositions of the logic. The only restriction on Sis that no member of Scan occur in any other member of S. The representation concerns the set SKconsisting of all members of Kin which occur members of S. Every member of SKmay be regarded as a truth-function of the members of S. If Sconsists of only one member, P, and if f(P)and g(P)are any members of SK, then we define |f(P)| as (f(P)·f(~P)). The proposition “f(P)is S-necessary” may then be expressed by |f(P)· Furthermore we may express “f(P)is S-impossible” by |~f(P)|, abbreviated to f(P)*; we may express “f(P)is S-possible” by abbreviated to f(P); and we may express “f(P) S-strictly implies g(P)” by (f(P)·~g(P))*, abbreviated to f(P)?g(P). Thus is obtained a novel analysis of modality, contrasting, on the one hand, with Carnap's syntactic theory of modality, and, on the other hand, with Lewis's view of modal concepts as underivable from other logical concepts. We would maintain that modal concepts are not absolute, but always relative to some S, generally unspecified.In the formal exposition which follows, we shall assume tacitly but not explicitly the important distinction between the symbols we are discussing and symbols denoting or designating the former.

The system of formal logic to be presented in this paper has the following main properties:(1). The Mengenlehre paradoxes do not arise in it.(2). It seems to be free from other contradictions.(3). It does not resort to a theory of types.(4). It uses negation and material implication and does not weaken the principle of excluded middle.(5). It contains no analogue to the Curry Woperator; consequently, given a propositional function ?, a propositional function ? cannot always be found such that, for all x, ?(x, x) and ?(x) are equivalent propositions.(6). It employs a universal quantifier, G, such that (x)f(x), (x)f(x, x), (x)f(x, x, x), …, would be respectively expressed thus, G(f, f), G(f, f, f), G(f, f, f, f), ….(7). It employs Schönfinkel's functional notation, so that f(x1, x2, …, xn) will be written as (( … ((fx1)x2) …)xn) and abbreviated to (fx1x2… xn) and, when no ambiguity results, to fx1x2…xn.(8). A theory of integers and real numbers cannot, apparently, be deduced from it.(9). A form of the axiom of choice is provable in it.

When the axioms of infinity and choice are added to the system of logic of the second edition of Whitehead and Russell's Principia mathematica, and when, as in the second edition, the axiom of reducibility is omitted (so that the ramified nature of Russell's theory of types, especially his distinction between “orders,” is not in effect obliterated), the resulting system will hereafter be referred to as “the ramified Principia.” It will be shown that a certain system S, slightly stronger than the ramified Principia, is consistent, so that the ramified Principiaitself is consistent. From Gödel's theorem it will then follow that the sort of mathematical induction employed in the consistency proof of Scannot be adequately handled within Sor within the ramified Principia.The method of proving the consistency of Swill be roughly as follows: A consistent non-constructive system S' will be defined by means of induction with respect to a serial well-ordering of all the propositions of S. It will then be shown that every true proposition of Sis a true proposition of S', so that Smust also be consistent.1. Preliminary conventions.1.1. Definition. By a “symbol” is to be understood any typographical expression which does not consist of a horizontal collinear sequence of expressions. Expressions formed by adding indices to either of the two upper or two lower corners of a symbol will also be considered symbols.

1.1. The aim of this paper is the construction of a demonstrably consistent system of set theory that (1) contains roughly the same amount of mathematics as the writer's system K'[3], including a theory of continuous functions of real numbers, and (2) provides a way for expressing in the object language various propositions which, in the case of K',could be expressed only in the metalanguage, for example, general propositions about all real numbers. It was not originally intended that the desired system should be a modal logic, but the modal character of the system appears to be a natural outgrowth of the way it is constructed. A detailed treatment of the natural, rational, and real numbers is left for a subsequent paper.

1.1 The system K* of basic logic, as presented in a previous paper, will be shown to be formalizable in an alternative way according to which the rule [E],is replaced by the rule [F],1.2. General recursive functions will be shown to be definable in K* in a way that retains functional notation, so that the equation,will be formalized in K* by the formula,where ‘f’, ‘p1’, … ‘pn’ respectively denote f, x1, …, xn, and where ‘?’ plays the role of numerical equality. Partial recursive functions may be handled in a similar way. The rule [E] is not required for dealing with primitive recursive functions by this method.1.3. An operator ‘G’ will be defined such that ‘[Ga? p]’ is a theorem of K* if and only if ‘p’ denotes the Gödel number of ‘a’.1.4. In reformulating K* we assume ‘o0’, ‘o1,’ ‘o2’, …, have been so chosen that we can determine effectively whether or not a given U-expression is the mth member of the above series. The revised rules for K* are then as follows. (Double-arrow forms of these rules are derivable, except in the case of rule [V].)

A previous paper proposed a finitary system of logic which was surmised to be basicin the sense that every finitary system of logic could be defined within it. In the present paper this anticipated result, or rather its syntactical counterpart, is definitely established as Theorem VI. The calculus Kis a formalization of the basic logic. Its main features were described in the previous paper, acquaintance with which is presupposed here. Attention is called to the fact that from now on the class Yof atomic U-expressions will be assumed to be finite instead of infinite. This is a relatively minor change and does not affect the previously established results. The account of the nature of calculi, as given in the other paper, is to be made more precise by stating that a calculus is any class of expressions having as a Gödel representation a recursively enumerable class of integers. A system of logic is regarded as being finitaryif it is capable of formalization by means of an appropriate calculus.

A logical calculus will be presented which not only is a formulation of a “basic logic” in the sense of the writer's previous papers, but which has the additional property that no weaker calculus can be a formulation of a basic logic. A sort of minimum logical calculus is thus attained, which has nothing superfluous about it for achieving the purpose for which it is designed.In the case of some logical calculi the question can arise as to whether certain of the postulates are really logically valid and necessary. Sometimes a test is available, such as the truth-table test, enabling us to distinguish between logically valid sentences and others, but often no such test is available, especially where quantifiers are involved. Is or is not the axiom of infinity, for example, to be regarded as logically valid? Or is the principle of double negation really acceptable, even though it satisfies the truth-table test?

A logical calculus ?was defined in a previous paper and then shown in a subsequent paper to contain within itself a representation of every constructively definable subclass of expressions of a certain infinite class Uof expressions, where ?itself is one such subclass. (The former paper will be referred to as BL and the latter paper as RC.) The calculus ?was called a “basic calculus” and its theorems were thought of as expressing the asserted propositions of a “basic logic,” that is, of a logic within which is definable every constructively definable system of logic and indeed every constructively definable class or relation. The notion of constructive definability was essentially equated with the notion of recursive enumerability.

13.1. If ‘[p f a]’ is in K', we will say that ‘p’ is a value of ‘f’ at ‘a’.13.2. If ‘a’ and ‘b’ are rational U-reals and if ‘b’ is not less than ‘a’, then ‘{a, b}’ will be called a rational U-interval.13.3. If ‘f’ has a value at ‘d’, if ‘d’ is within a U-interval ‘{c, e}’, and if all values of ‘f’ at U-reals with ‘{c, e}’ are within the U-interval ‘{r, t}’, then we will say that ‘{c, e}’ restricts ‘f’ to ‘{r, t}’ at ‘d’, and that ‘{c, e}’ is an ‘f’-restrictive correlate of ‘d’ with respect to ‘{r, t}’.13.4. If ‘d’ is within ‘{a, b}’, we will say that ‘{a, b}’ “contains” ‘d’.13.5. If ‘f’ has a value at ‘d’ and if corresponding to every U-interval ‘{r, t}’ that contains a value of ‘f’ at ‘d’ there is an ‘f’-restrictive correlate of ‘d’ with respect to ‘{r, t}’, then ‘f’ will be said to be “continuous” at ‘d’. Without loss of generality the ‘f’-restrictive correlate can be required to be a rational U-interval.13.6. If ‘f’ is continuous at every U-real in ‘{a, b}’, we will say that ‘f’ is continuous in ‘{a, b}’.13.7. Theorem. If ‘k’ is a positive U-real and ‘f’ is continuous in a U-interval ‘{a, b}’, then ‘{a, b}’ is covered by the class S of rational U-intervals that are ‘f’-restrictive correlates of rational U-reals in ‘{a, b}’ with respect to those rational U-intervals ‘{r, t)’ that contain values of ‘f’ at rational U-reals in ‘{a, b}’ and that are such that’|t - r|‘ is equal to ‘k’ (in the sense of 10.10).

The purpose of this paper is to provide a partial logical analysis of a few concepts that may be classified as value concepts or as concepts that are closely related to value concepts. Among the concepts that will be considered are striving for, doing, believing, knowing, desiring, ability to do, obligation to do, and value for. Familiarity will be assumed with the concepts of logical necessity, logical possibility, and strict implication as formalized in standard systems of modal logic (such as S4), and with the concepts of obligation and permission as formalized in systems of deontic logic. It will also be assumed that quantifiers over propositions have been included in extensions of these systems.

The system of combinatory logic to be presented in this paper will be called C?. It may be compared to various systems of combinatory logic constructed by Schonfinkel [11], Curry [1], Rosser [10], and Curry and Feys [2], and to the author's systems K' [3] and S [5], and to extensional modifications of K' [6], [7], [8], [9]. The present system falls within this latter category of extensional or semi-extensional systems, but it is more perspicuous than the others, and the proof of its consistency is more direct. It contains the theory of combinators in full strength. It also contains operators for disjunction, conjunction, negation, existence (that is, non-emptiness), and universality. A considerable part of classical mathematical analysis can be shown to be derivable in C?, just as in K' [4], but with the added advantage of the availability of a limited extensionality principle.

The system K' of “extended basic logic” lacks a principle of extensionality. In this paper a system KE' will be presented which is like K' in many respects but which does possess a fairly strong principle of extensionality by way of rule 6.37 below. It will be shown that KE' is free from contradiction. KE' is especially well suited for formalizing the theory of numbers presented in my paper, On natural numbers, integers, and rationals. The methods used there can be applied even more directly here because of the freedom of KE' from type restrictions, but the details of such a derivation of a portion of mathematics will not be presented in this paper. It is evident, moreover, that KE' contains at least as much of mathematical analysis as does K', and perhaps considerably more. The method of carrying out proofs in KE' is closely similar to that used in my book Symbolic logic, and could be expressed in similar notation.

Let “the hypothesis of similarity” be the hypothesis that all infinite classes are similar (have the same power or cardinal number). It will be shown that the system of logic of Whitehead and Russell's Principia mathematica(without the axiom of reducibility) is consistent when to its axioms are added all the following:(1). The hypothesis of similarity.(2). The axiom of infinity.(3). The axiom of choice.(4). The contradictory of the axiom of reducibility.If (2) – (4) but not (1) are employed in Principia, it must therefore be the case that Cantor's theorem is not deducible, since it contradicts (1). If (2) and (3) but not (1) and (4) are employed, then a proof of Cantor's theorem must require the use of some sort of reducibility principle.The first step in the required consistency proof is to modify in certain respects the system Sof a previous paper. Immediately after definition 3.5 the following definition is to be added:3.5.1. If ais of the form (b,c), where xis an S-variable and where band care S-constants neither of which is of higher order than that of x, then ais an S-proposition.

The purpose of this paper is to suggest two alternatives to Quine's definition of closure. These new definitions have two advantages over Quine's definition, and they probably are the simplest definitions having bothadvantages. The two advantages are:(1). Principle *101 becomes superfluous and may be dropped from Quine's set of principles for quantification. (In the case of my second definition, however, the dropping of *101 must be balanced by a slight change in *104.)(2). Closure is made independent of the alphabetical order of variables.The second of these advantages turns on the fact that the “alphabetical order” possessed by variables in virtue of their respective positions in the alphabet (or arbitrarily assigned to them) is a mere convention and not of genuine logical significance. It seems therefore desirable to consider some alternatives to Quine's definition of closure, since according to his definition the closure of a given formula will be one statement or another, depending upon whether or not one letter of the alphabet is alphabetically prior to a certain other letter. It is interesting that the removal of this minor artificiality also enables us to dispense with *101.According to Quine, the closure of a formula containing nfree variables is obtained by prefixing to it in alphabetical order the nuniversal quantifiers formed from these variables by enclosing each in a pair of parentheses. (If n= 0 the formula is its own closure and is a “statement” rather than a “matrix.”) Thus the statement ‘(x)(y)(z)(x?y? y?z)’ would be the closure of ‘x?y? y?z’, but ‘(z)(x)(y)(x?y? y?z)’ would not be its closure. Now there is no reason why ‘(z)(x)(y)(x?y? y?z)’ or (y)(z)(x)(x?y? y?z) and so on, could not just as well be regarded as “the” closure of ‘(x?y? y?z’ as ‘(x)(y)(z)(x?y? y?z)’. I therefore propose to allow to each formula not merely oneclosure, but as many closures as can be obtained by permuting in various ways the nprefixed universal quantifiers. In this way alphabetical order becomes irrelevant and no preference is given to one order of prefixed quantifiers in contrast to other orders which seem equally good. This constitutes my first redefinition of closure.

This paper is concerned with finding a fairly simple system of logic which is “basic” in the sense that every system of logic is definable in it. If a “system”is regarded as being a class of propositions, rather than a class of sentences, then every class of propositions which is a system should be definable in the basic logic. The system of logic proposed in this paper will not be proved to be a basic logic, but strong evidence that it is basic will be given at the end of the paper. Evidence will also be given that the class of propositions which are not provable in the system is not definable in any system of logic. It will be established that the decision problem is unsolvable for the system. Notable characteristics of the system are its lack of negation and universal quantification, and its similarity to systems proposed by Church, Curry, and Rosser.By a “system” will be meant a class of propositions the membership of which can be specified by ordinary recursive methods, so that if the membership of a given proposition in the class can be established at all, such membership can be established in a finite number of steps. (This is not the same as demanding that a criterion must exist for determining, in a finite number of steps, whether or not some given proposition is a member of the class. Such a demand would require a solution of the decision problem for every system.)

A demonstrably consistent theory of real numbers has been outlined by the writer in An extension of basic logic1(hereafter referred to as EBL). This theory deals with non-negative real numbers, but it could be easily modified to deal with negative real numbers also. It was shown that the theory was adequate for proving a form of the fundamental theorem on least upper bounds and greatest lower bounds. More precisely, the following results were obtained in the terminology of EBL: If ? is a class of U-reals and is completely represented in ?' and if some U-real is an upper bound of ?, then there is a U-real which is a least upper bound of ?. If Dis a class of (U-reals and is completely represented in ?', then there is a U-real which is a greatest lower bound of D.

A theory of natural numbers will be outlined in what follows. This theory will also be extended to give an account of positive and negative integers and positive and negative rational numbers. The system of logic used will be that of Whitehead and Russell's Principia mathematicawith the simple theory of types. It will be assumed that the reader is familiar with the more elementary properties of relations and with such notions as the relative product of two relations, the square of a relation, the cube of a relation, and the various other whole-number powers of relations.The guiding principle of this theory is that the natural number zero is to be regarded as the relation of the zevothpower of a relation ?to ?itself, and the natural number 1 is to be regarded as the relation of the first power of a relation ?to ?itself, and the natural number 2 is to be regarded as the relation of the square of a relation ?to ?itself, and so on.

1.1. In two previous papers a consistent theory of real numbers has been outlined by the author, using a system K'. This latter system is an extension of a system K, which is “basic” in the sense that every finitary (recursively enumerable) subclass of its well-formed expressions is in a certain sense represented in it. The system Ldescribed below is a further extension of K. The system K' lacks two important features possessed by L: a symbol for a special kind of implication (or “conditionality”) and a symbol for the modal concept “necessity.” The presence of the implication symbol, and the additional assumptions that go with it, make available in Lvarious kinds of restricted universal quantification not available in K', for example, universal quantification restricted to the real numbers of the author's theory of real numbers.1.2. If ‘~[a & ~a]’ is a theorem of L, then the proposition expressed by ‘a’ may be said to L-satisfy the principle of excluded middle. I t is always the case that ‘a’ L-satisfies the principle of excluded middle (or rather that the proposition expressed by ‘a’ does so) if and only if ‘a’ or ‘~a’ is a theorem of L. An example of a proposition that does not L-satisfy the principle of excluded middle is that expressed by ‘’, namely the proposition that asserts that the class of classes that are not members of themselves is a member of itself.

This paper continues the exposition of a demonstrably consistent foundation for mathematics begun in An extension of basic logic(hereafter referred to as EBL) and in The Heine-Borel theorem in extended basic logic(hereafter referred to as HB). Still earlier papers related to these are A basic logic(referred to as BL) and Representations of calculi(referred to as RC). The main conventions and results of all the above papers will be presupposed in what follows. The numbering of sections and paragraphs will be a continuation of that of EBL and HB.

The program of “basic logic” can be summarized as follows:I. To treat every syntactical system as a subclass of a certain fixed infinite classUof“U-expressions.” This can always be done by modifying in trivial ways the notation of each syntactical system which is not already such a subclass. As a result all syntactical systems become comparable with each other in the sense that they are merely different subclasses of a single class of expressions. The class Ucan be chosen in such a way as to be inductively definable thus in terms of a fixed symbol ‘s’: (1) The symbol ‘s’ is a U-expression. (2) The result of placing two U-expressions (or two occurrences of the same U-expression) next to each other, and enclosing this total expression within a pair of parentheses, is a U-expression.II. To formulate a particular syntactical systemKwithin which every syntactical system(and indeedKitself) is “represented.”Such a system is here said to be a “basic system,” and an appropriate interpretation of it is said to be a “basic logic.” Within such a logic every finitary logic is definable, as well as the basic logic itself. Such a logic should be of fundamental importance, especially if it is so constructed as to be the weakest such logic and so contain no theorems that are not essential to its being basic.With the above considerations in view, the system Khas been defined in such a way that it is a subclass of Uand is a basic syntactical system. A simpler definition of Kwill be given than heretofore in previous papers, and the minimum character of Kwill be made more clear.

In a previous paper it was shown that the system Kof basic logic could be formulated in a simpler way owing to the fact that the proper ancestral could be defined in terms of the other concepts of that system. In the present paper analogous but more far-reaching results will be obtained for the system K' of extended basic logic. In particular we will show that negation and the dual of the proper ancestral, as well as the proper ancestral itself, are definable in terms of the other concepts of K'. Hence, in order to define K', we need to add only a single non-finitary rule to the rules used to define K. This rule was already among the rules originally used to define K'. It asserts that ‘Aa’ is in K' if (and only if) every ‘b’ is such that ‘ab’ is in K'.We will also show that a large class of non-finitary classes and relations are represented in K', among which is K' itself, just as all finitary syntactical classes and all finitary two- and three-place syntactical relations are represented in K, one of which is the finitary syntactical class Kitself. The point is that K' is adequate to handle the sort of transfinite induction that is essential in formulating K', just as Kis adequate to handle the ordinary finitary mathematical induction required in defining K'.