Logistic system
Logistic system
The formal construction of a logistic system requires
a list of primitive symbols (these are usually taken as marks but may also be sounds or other things — they must be capable of instances which are, recognizably, the same or different symbols, and capable of utterance in which instances of them arc put forth or arranged in an order one after another);
a determination of a class of formulas, each formula being a finite sequence of primitive symbols, or, more exactly, each formula being capable of instances which are finite sequences of instances of primitive symbols (generalizations allowing two-dimensional arrays of primitive symbols and the like are non-essential);
a determination of the circumstances under which a finite sequence of formulas is a proof of the last formula in the sequence, this last formula being then called a theorem (again we should more exactly speak of proofs as having instances which are finite sequences of instances of formulas);
a determination of the circumstances under which a finite sequence of formulas is a proof of the last formula of the sequence as a consequence of a certain set of formulas (when there is a proof of a formula B as a consequence of the set of formulas A1, A2, . . . , An, we say that the inference from the premisses A1, A2, . . . , An to the conclusion B is a valid inference of the logistic system).
It is not excluded that the class of proofs in the sense of (3) should be empty. But every proof of a formula B as a consequence of an empty set of formulas, in the sense of (4), must also be a proof of B in the sense of (3), and conversely. Moreover, if to the proof of a formula B as a consequence of A1, A2, . . . , An are prefixed in any order proofs of A1, A2, . . . , An, the entire resulting sequence of formulas must be a proof of B; more generally, if to the proof of a formula B as a consequence of A1, A2, . . . , An are prefixed in any order proofs of a subset of A1, A2, . . . , An as consequences of the remainder of A1, A2, . . . , An, the entire resulting sequence must be a proof of B as a consequence of this remainder.
The determination of the circumstances under which a sequence of formulas is a proof, or a proof as a consequence of a set of formulas, is usually made by means of
a list of primitive formulas; and
a list of primitive rules of inference each of which prescribes that under certain circumstances a formula B shall be an immediate consequence of a set of formulas A1, A2, . . . , An.
The list of primitive formulas may be empty — this is not excluded. Or the primitive formulas may be included under the head of primitive rules of inference by allowing the case n=0 in (6). A proof is then defined as a finite sequence of formulas each of which is either a primitive formula or an immediate consequence of preceding formulas by one of the primitive rules of inference. A proof as a consequence of a set of formulas A1, A2, . . . , An is in some cases defined as a finite sequence of formulas each of which is either a primitive formula, or one of A1, A2, . . . , An, or an immediate consequence of preceding formulas by one of the primitive rules of inference; in other cases it may be desirable to impose certain restrictions upon the application of the primitive rules of inference (e.g., in the case of the functional calculus of first order — logic, formal, 3 — that no free variable of A1, A2, . . . , An shall be generalized upon).
A logistic system need not be given any meaning or interpretation, but may be put forward merely as a formal discipline of interest for its own sake; and in this case the words proof, theorem, valid inference, etc., are to be dissociated from their every-day meanings and taken purely as technical terms. Even when an interpretation of the system is intended, it is a requirement of rigor that no use shall be made of the interpretation (as such) in the determination whether a sequence of symbols is a formula, whether a sequence of formulas is a proof, etc.
The kind of an interpretation, or assignment of meaning, which is normally intended for a logistic system is indicated by the technical terminology employed. This is namely such an interpretation that the formulas, some or all of them, mean or express propositions; the theorems express true propositions; and the proofs and valid inferences represent proofs and valid inferences in the ordinary sense. (Formulas which do not mean propositions may be interpreted as names of things other than propositions, or may be interpreted as containing free variables and having only an ambiguous denotation — see variable.) A logistic system may thus be regarded as a device for obtaining — or, rather stating — an objective, external criterion for the validity of proofs and inferences (which are expressible in a given notation).
A logistic system which has an interpretation of the kind in question may be expected, in general, to have more than one such interpretation.
It is usually to be required that a logistic system shall provide an effective criterion for recognizing formulas, proofs, and proofs as a consequence of a set of formulas; i.e., it shall be a matter of direct observation, and of following a fixed set of directions for concrete operations with symbols, to determine whether a given finite sequence of primitive symbols is a formula, or whether a given finite sequence of formulas is a proof, or is a proof as a conseqence of a given set of formulas. If this requirement is not satisfied, it may be necessary — e.g. — given a particular finite sequence of formulas, to seek by some argument adapted to the special case to prove or disprove that it satisfies the conditions to be a proof (in the technical sense); i.e., the criterion for formal recognition of proofs then presupposes, in actual application, that we already know what a valid deduction is (in a sense which is stronger than that merely of the ability to follow concrete directions in a particular case). See further on this point logic, formal, 1.
The requirement of effectiveness does not compel the lists of primitive symbols, primitive formulas, and primitive rules of inference to be finite. It is sufficient if there are effective criteria for recognizing formulas, for recognizing primitive formulas, for recognizing applications of primitive rules of inference, and (if separately needed) for recognizing such restricted applications of the primitive rules of inference as are admitted in proofs as a consequence of a given set of formulas.
With the aid of Gdel’s device of representing sequences of primitive symbols and sequences of formulas by means of numbers, it is possible to give a more exact definition of the notion of effectiveness by making it correspond to that of recursiveness (q. v.) of numerical functions. E.g., a criterion for recognizing primitive formulas is effective if it determines a general recursive monadic function of natural numbers whose value is 0 when the argument is the number of a primitive formula, 1 for any other natural number as argument. The adequacy of this technical definition to represent the intuitive notion of effectiveness as described above is not immediately clear, but is placed beyond any real doubt by developments for details of which the reader is referred to Hilbert-Bernays and Turing (see references below).
The requirement of effectiveness plays an important role in connection with logistic systems, but the necessity of the requirement depends on the purpose in hand and it may for some purposes be abandoned. Various writers have proposed non-effective, or non-constructive, logistic systems; in some of these the requirement of finiteness of length of formulas is also abandoned and certain infinite sequences of primitive symbols are admitted as formulas.
For particular examples of logistic systems (all of which satisfy the requirement of effectiveness) see the article logic, formal, especially 1, 3, 9.
Alonzo Church
R. Carnap,
The Logical Syntax of Language, New York and London, 1937.
H. Scholz,
Was ist ein Kalkl und was hat Frege fr eine pnktliche Beantwortung dieser Frage geleistet?, Semester-Berichte, Mnster i. W., summer 1935, pp. 16-54.
Hilbert and Bernays,
Grundlagen der Mathematik, vol. 2, Berlin, 1939.
A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, ser. 2 vol. 42 (1937), pp. 230-265, and Correction, ibid., ser. 2 vol. 43 (1937), pp. 544-546.
A. M. Turing, Computability and ?-definability, The Journal of Symbolic Logic, vol. 2 (1937), pp. 153-163.