Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-25T06:27:03.896Z Has data issue: false hasContentIssue false
  • English
  • Français

Formal systems of constructive mathematics

Published online by Cambridge University Press:  12 March 2014

M. H. Löb
M. H. Löb*
Affiliation:
University of Leeds
Get access Rights & Permissions [Opens in a new window]

Extract

In the present paper we investigate in some detail two systems closely related to those contained in [4]. The system K1 of [4] is simplified by eliminating conjunction and disjunction, giving rise to a system Σ whose primitives are two individuals, concatenation, identity, existential and limited universal quantification. Any relation expressible in Σ may be expressed in the form (Eα1)(β)α1(Eα2)…(Eαn)(γ = δ). A further reduction of primitives leads to a system Σμ, which differs from Σ by containing the operator μ (i.e. “the first string, such that” with respect to a certain ordering) in place of the quantifiers. Reasons are given for restricting Myhill's definition of constructive ideas to those expressible in Σμ.

Acquaintance with [4], [5], [6] is assumed. We deviate from [4] by dropping concatenation-signs and parentheses in chain matrices from the official notation, and, furthermore, by using Greek and German letters as metalinguistic variables standing for chain matrices and chains, respectively, while retaining small Roman letters (excluding a, b) for use as variables of the systems.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 21 , Issue 1 , March 1956 , pp. 63 - 75
Copyright
Copyright © Association for Symbolic Logic 1956

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

BIBLIOGRAPHY

[1]Davis, Martin, Arithmetical problems and recursively enumerable predicates, this Journal, vol. 18 (1953), pp. 33–41.Google Scholar
[2]Fitch, F. P., A basic logic, this Journal, vol. 1 (1936), pp. 105–114.Google Scholar
[3]Kleene, S. C., Recursive predicates and quantifiers, Transactions of the American Mathematical Society, vol. 53 (1943), pp. 41–73.CrossRefGoogle Scholar
[4]Löb, M. H., Concatenation as basis for a complete system of arithmetic, this Journal, vol. 18 (1953), pp. 1–6.Google Scholar
[5]Myhill, John R., A complete theory of natural, rational and real number numbers, this Journal, vol. 15 (1950), pp. 185–196.Google Scholar
[6]Post, E. L., Formal reductions of the general combinatorial decision problem, American journal of mathematics, vol. 65 (1943), pp. 197–215.CrossRefGoogle Scholar