Propositional calculus and realizability
Gene F. Rose · Transactions of the American Mathematical Society · 1953
A familiarity with the fundamental results pertaining to this concept is presupposed.For this purpose, the reader is referred to the above paper or to [17, §82].The conjecture which is disposed of in this paper was proposed by Kleene in correspondence in November 1941, and was the only one of an early group of conjectures about realizability which was not settled by 1945.It was discussed by him in a paper before the Princeton Bicentennial Conference on the Problems of Mathematics in December 1946 (unpublished).The author took up the investigation in 1947, following a suggestion by Kleene that Jaskowski's matric treatment of the Heyting propositional calculus [lO] might provide a basis for attacking that part of the problem which concerns the propositional calculus.The solution by a counterexample, presented here, was obtained in February 1951.The material in this paper is included in JaSkowski's truth-tables and realizability, a thesis submitted in partial fulfilment of the requirements for the degree of Doctor of Philosophy at the University of Wisconsin and accepted in February 1952.In the thesis, the proofs of the following lemmas and theorems are given in greater detail: 3.2, 4.5, 4.6, 4.7, 4.8, 5.1, 5.2, 5.3, 5.4, 6.1, 7.1, 7.2.(2) Cf.Nelson [23, Theorem l] or Kleene [17, §82, Theorem 62(a)].(3) Cf. [8; 9; 2].(4) Cf. [13, §10].Other demonstrations were given later: cf.[14; 17, §80; 22].(6) For the classical predicate calculus, there is the well known completeness theorem of Gödel [4].For the intuitionistic predicate calculus, on the other hand, no completeness theorem was known until 1949, when one not closely connected with the logical interpretation was found by Henkin [7] as a kind of converse of a result of Mostowski [22].