No CrossRef data available.
Article contents
An Investigation on the Logical Structure of Mathematics (IV)0): Compendium for Deductions
Published online by Cambridge University Press: 22 January 2016
Extract
Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.
In § 1 the usage and conventions which are used in the deductions in UL are explained. In §§ 2-4 some metatheorems concerning the deductions are proved. Namely, in § 2 the order of proof constituents in a proof is investigated; in § 3 the applicability of composite proof constituents are proved on the basis of § 2; in §4 the place of the “ordinarily used” principle of extensionality in a proof is specified. In §5 a sufficient condition of the mechanization of mathematics is given in such a manner that the mechanical and non-mechanical parts in solving mathematical problems are separated in accord with the usual way of thinking in mathematics.
- Type
- Research Article
- Information
- Copyright
- Copyright © Editorial Board of Nagoya Mathematical Journal 1958
Footnotes
0)
(Added in proof) This Part (IV) is the continuation of my previous papers: Parts (I) and (II) are forthcoming in E. Artin-H. Hasse’s jubilee volume of the Hamburger Abhandlungen and Part (III) is contained in this same volume. Further continuation will appear elsewhere.
References
1) See theorem 1, §12, Part (II).
2) See §3.
3) See, Equality, Part (III).
4) See, for instance, σ*6, σ*9, Part (III).
5) See the end of the paragraph preceding the conclusion of Introduction in Part (II).
6) See §21, Part (II).
7) The characteriatic properties E1 * 7 and E1 * 9 of ordered pairs are deduced in the Section “Elementary Set,” Part (III). In this section Spf and * Spf are used naturally without taking E1 * 7 and E1 * 9 as premises. The formulas E1 * 7 and E1 * 9 are used as premises in Part (III) in the deduction of the Section “Image of Operator” and the subsequent Sections.
8) Property (a): Any formula under the top sequence is effective. Property (b): Any string of a proof contains no two homologous proof formulas, unless they are both the negation of some defining formulas. For the properties (a), (b), and (d), see §§12, 13, Part (II).
9) See §14, Part (II),
10) By a proper subformula is meant here a subformula in the reduced sense, i.e. a subformula B of A is a proper subformula in the reduced sense, exactly if the reduced degree of B is smaller than that of A. As usual, a subformula is considered in taking its position in a formula into account so that M may contain identical formulas which are at different positions in: G*.
11) See §19, Part (II),
12)
That is, the formulas which are either primitive or a bottom formula of CT (Q, 
) for a member Q of M.
13)
Otherwise, it might happen that a subformula of the form 
at a negative position of would be contained in no member of M so that the proof constituent 
associated to a bottom formula of the carrier Cp
would belong to the tree T constructed before. If so, 
must be brought to the connected part C. But this might be impossible if m dependeds on the eigen variable of a P-constituent which is under 
and over
14)
In order that m can be substituted for x in a formula Fx
, it is necessary and sufficient that m depends on no variable, say y, such that there is an x in Fx
which is under the operator range of 
See the condition of substitution of m for x in U in § 8, Part (I) and foot note 8) there. The variables x1
, …, xn
and y1
, …, yn
are not necessarily the complete systems of variables of F and G, respectively.
15)
We associate the composite proof constituent 
to G, if G is of the form 
16) See §11, Part (I).
17) Although Q is not a proof, it is clear what the elementary transformation of Q means.
You have
Access