Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-09T22:46:22.741Z Has data issue: false hasContentIssue false
  • English
  • Français

A basic logic

Published online by Cambridge University Press:  12 March 2014

Frederic B. Fitch
Frederic B. Fitch*
Affiliation:
Yale University
Get access Rights & Permissions [Opens in a new window]

Extract

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.)

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 7 , Issue 3 , September 1942 , pp. 105 - 114
Copyright
Copyright © Association for Symbolic Logic 1942

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

1 The present paper gives in more detailed form, and with some important improvements, the results reported in a paper entitled Toward a basic logic, read on Dec. 28, 1940, at Philadelphia at a joint meeting of the Association for Symbolic Logic and the A.A.A.S. Much of the general discussion included in the Philadelphia paper, however, has been omitted here. For a summary of the latter paper, see this Journal, vol. 6 (1941), p. 39. The present paper has benefited from the helpful comments made by the referee on a previous draft of it. The author's indebtedness to the writings of Curry, Church, Rosser, Quine, Carnap, Tarski, and other workers in this field, should be obvious.

2 For references to some of Curry's and Rosser's main papers on combinatory logic see Curry, H. B., A revision of the fundamental rules of combinatory logic, this Journal, vol. 6 (1941), pp. 41–53Google Scholar, also an article by Curry that immediately follows the latter. The present system is also very similar to systems that have been proposed by Alonzo Church. See, for example, the system described on pp. 65 and 66 of his book, The calculi of lambda-conversion, Annals of Mathematics studies no. 6, Princeton University Press, Princeton, 1941.

3 These sentences are to be thought of as already “interpreted,” that is, as already understood as regards their meanings. In syntactical investigations a calculus is usually treated in abstraction from the meanings of its sentences.

4 An alternative (and in some respects preferable) method would be to define the class of K-sentences not as U itself but as a proper subclass of the class U. This could be done by a recursive definition somewhat as follows: Expressions of the form ‘(=ƒa)’ are K-sentences so is ‘(εaƒ); if (ƒ(ga)’ is a K-sentence so is ‘(oƒga)’; and so on (paralleling the rules in 3.1). Then it could be said that if ‘(ƒa)’ is a K-sentence, ‘(ƒa)’ expresses the proposition that a is a member of ƒ. Similarly it could be said that if ‘(gab)’ is a K-sentence, ‘(gab)’ expresses the proposition that a bears the dyadic relation g to b.

5 We may refer to ‘(ab)’ as the “combination” of ‘a’ with ‘b’, and to (ab) as the “application” of a to b.

6 The interpretation of these symbols should be clear from the use made of them. Briefly, however, the interpretation is as follows: ‘=’ means identity, ‘ε’ means class membership. ‘o’ means the triadic relation of ƒ to g to a such that the application of g to a is a member of ƒ. ‘έ’ means the triadic relation of a to ƒ to b such that g bears to b the dyadic relation ƒ, ‘ό’ means the tetradic relation of ƒ to g to a to b such that the application of g to a bears to b the dyadic relation ƒ. ‘W’ means the dyadic relation of ƒ to a such that a bears to itself the dyadic relation ƒ. ‘&’ means prepositional conjunction. ‘V’ means propositional alternation. ‘E’ means the class of existent (non-empty) classes. ‘*’ means the triadic relation of ƒ to a to b such that a bears to b the proper ancestral of the dyadic relation ƒ. Observe that ‘o’ and ‘ό’ are analogous to Curry's ‘B’, while ‘ε’ and ‘έ’ are analogous to Curry's ‘(CI)’, which is Rosser's ‘T’ Finally ‘W’ and ‘E’ are respectively analogous to Curry's ‘W’ and ‘Σ’.

7 It is to be understood that U-expressions used as variables are to be so chosen in each case that they occur nowhere except where indicated by the context.

8 A “U-calculus” is a calculus which is a subclass of U.

9 See Rosser, Barkley, An informal exposition of proofs of Gödel's theorems and Church's theorem, this Journal, vol. 4 (1939), pp. 53–60.Google Scholar

10 Supposing, of course, that U has been assigned an adequate supply of interpreted symbols.

11 Observe the important part played by ‘W’ in the following discussion. Cp. the author's paper, A system of formal logic without an analogue to the Curry W-operator, this Journal, vol. 1 (1936), pp. 92–100. In that paper the Russell paradox is avoided by omitting the W-operator, in this paper by omitting negation.