Hostname: page-component-586b7cd67f-t7fkt Total loading time: 0 Render date: 2024-11-24T23:34:18.883Z Has data issue: false hasContentIssue false
  • English
  • Français

A remark on free choice sequences and the topological completeness proofs

Published online by Cambridge University Press:  12 March 2014

G. Kreisel
G. Kreisel*
Affiliation:
The University, Reading, England
Get access Rights & Permissions [Opens in a new window]

Extract

Below are collected some simple results on the theory of free choice sequences [4] or infinitely proceeding sequences (ips) as they are called in [5]. These results are not sufficient to settle the completeness problems for Heyting's predicate calculus [4], as formulated in [12], neither in the strong nor in the weak sense. They are published because they lead to intuitionistically valid versions of completeness proofs which have appeared in the literature, particularly [16], [17], [18], and, with certain reservations, [1].

The problems considered below (except in §8) differ from those of [12] in the following respect: In [12] we were mainly concerned with formulae of Heyting's predicate calculus which were not even classically provable, and showed that the calculus was complete with respect to certain classes of these formulae. The novel feature was that we established this completeness by means of intuitionistically valid methods, in fact methods which can be formalized in Heyting's arithmetic. Here we are primarily concerned with formulae which are classically, but not intuitionistically, provable. As pointed out in [12], the nature of the completeness problem for such formulae is totally different: the class of predicates which provides the required counterexamples must come from a system (with an intuitionistically acceptable interpretation) which, unlike Heyting's arithmetic, is not a subsystem of the corresponding classical system. An example of such a system is an extension FC, given below, of Heyting's formalization of the theory of free choices.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 23 , Issue 4 , December 1958 , pp. 369 - 388
Copyright
Copyright © Association for Symbolic Logic 1958

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

REFERENCES

[1]Beth, E. W., Semantic construction of intuitionistic logic, Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, Afd. Letterkunde, n.s. vol. 19 no. 11 (1956), pp. 357–388.Google Scholar
[2]Gödel, K., Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines mathetnatischen Kolloquiums, Heft 4 (1932), pp. 34–38.Google Scholar
[3]Heyting, A., Die formalen Regeln der intuitionistischen Logik, Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-Mathematische Klasse (1930), pp. 42–56.Google Scholar
[4]Heyting, A., Die formalen Regeln der intuitionistischen Mathematik, Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-Mathematische Klasse (1930), pp. 57–71, pp. 158–169.Google Scholar
[5]Heyting, A., Intuitionism, An introduction, Amsterdam (North Holland Pub. Co.), 1956, viii + 133 pp.Google Scholar
[6]Hilbert, D. and Bernays, P., Grundlagen der Mathematik, vol. 2, Berlin (Springer), 1939, xii + 498 pp.Google Scholar
[7]Kleene, S. C., A symmetric form of Gödel's theorem, Indagationes mathematicae, vol. 12 (1950), pp. 244–246.Google Scholar
[8]Kleene, S. C., Realizability, Summaries of talks presented at the Summer Institute of Symbolic in 1957 at Cornell University (mimeographed), 1957, pp. 100–104; also in Constructivity in mathematics, Amsterdam (North Holland Pub. Co.).Google Scholar
[9]Kreisel, G., Note on arithmetic models for consistent formulae of the predicate calculus, Fundamenta mathematicae, vol. 37 (1950), pp. 265–285.CrossRefGoogle Scholar
[10]Kreisel, G., Note on arithmetic models for consistent formulae of the predicate calculus II, Proceedings of XIth International Congress of Philosophy, vol. 14 (1953), pp. 39–49.Google Scholar
[11]Kreisel, G., Gödel's interpretation of Heyting's arithmetic, Summaries of talks presented at the Summer Institute of Symbolic Logic in 1957 at Cornell University (mimeographed), 1957, pp. 125–132; also in Constructivity in mathematics, Amsterdam (North Holland Pub. Co.).Google Scholar
[12]Kreisel, G., Elementary completeness properties of intuitionistic logic with a note on negations of prenex formulae, this Journal, vol. 23, pp. 317–330.Google Scholar
[13]Mostowski, A., On a system of axioms which has no recursively enumerable arithmetic model, Fundamenta mathematicae, vol. 40 (1953), pp. 58–61.CrossRefGoogle Scholar
[14]Mostowski, A., A formula with no recursively enumerable model, Fundamenta mathematicae, vol. 42 (1955), pp. 125–140.CrossRefGoogle Scholar
[15]Putnam, H., Arithmetic models for consistent formulae of quantification theory, this Journal, vol. 22 (1957), pp. 110–111.Google Scholar
[16]Rasiowa, H. and Sikorski, R., On existential theorems in non-classical functional calculi, Fundamenta mathematicae, vol. 41 (1954), pp. 87–91.Google Scholar
[17]Scott, Dana, Completeness proofs for the intuitionistic sentential calculus, Summaries of talks presented at the Summer Institute of Symbolic Logic in 1957 at Cornell University, mimeographed, 1957, pp. 231–241.Google Scholar
[18]Tarski, A., Der Aussagenkalkül und die Topologie, Fundamenta mathematicae, vol 31 (1938), pp. 103–134.CrossRefGoogle Scholar