In:
Journal of Symbolic Logic, Cambridge University Press (CUP), Vol. 2, No. 3 ( 1937-09), p. 113-119
Abstract:
1. The notion of derivability. Italic capitals, with or without subscripts, will be used as variables. They are to take as values some manner of elements which may for the present be left undetermined. Now let us consider abstractly the notion of the derivability of an element X from one or more specified elements by a series of steps of a specified kind. This involves reference to two conditions upon elements. One of these conditions, expressible by some statement form containing a single free variable, determines the elements from which X is said to be derivable. The other condition, expressed say by a statement form containing k + 1 free variables, determines the kind of steps by which the derivation is to proceed; it is the condition which any elements Z 1 , … Z k , Y must fulfill if progress from Z i , …, Z k to Y is to constitute a step of derivation in the intended sense. Supposing “ f(Y) ” supplanted by the first of these statement forms, whatever it may be, and “ g(Z 1 , …, Z k , Y) ” supplanted by the other, let us adopt the form of notation to express derivability of X in the suggested sense. The meaning of (1) can be formulated more accurately as follows: (i) There are elements Y 1 to Y m (for some m ) such that Y m = X and, for each i≦m , either f ( Y i ) or else there are numbers j 1 to Y m , each less than i , for which g ( Y j 1 , …, Y jk , Y i ). (Variable subscripts are to be understood, here and throughout the paper, as referring only to positive integers.) The notion (1) is illustrated in the ancestral R * of a relation R; 1 for, Another illustration is afforded by metamathematics. Suppose our elements are the expressions used in some formal system; suppose we have defined “ Post(Y) ”, meaning that Y is a postulate of that system; and suppose we have defined “ Inf ( Z I , …, Z k , Y )” (for some fixed k large enough for all purposes of the system in question), meaning that Y proceeds from Z 1 , …, Z k by one application of one or another of the rules of inference of the system. Then would mean that X is a theorem of the system.
Type of Medium:
Online Resource
ISSN:
0022-4812
,
1943-5886
Language:
English
Publisher:
Cambridge University Press (CUP)
Publication Date:
1937
detail.hit.zdb_id:
2010607-5
SSG:
5,1
SSG:
17,1
Bookmarklink
