On formulas of one variable in intuitionistic propositional calculus
- 1 December 1960
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 25 (4), 327-331
- https://doi.org/10.2307/2963526
Abstract
McKinsey and Tarski [3] described Gödel's proof that the number of Brouwerian-algebraic functions is infinite. They gave an example of a sequence of infinitely many distinct Brouwerian-algebraic functions of one argument, which means that there are infinitely many non-equivalent formulas of one variable in the intuitionistic propositional calculus LJ of Gentzen [1]. However they did not completely characterize such formulas. In § 1 of this note, we define a sequence of basic formulas P∞(X), P0(X), P1(X), … and prove the following theorems.Keywords
This publication has 3 references indexed in Scilit:
- Über die Zwischensysteme der AussagenlogikNagoya Mathematical Journal, 1955
- On Closed Elements in Closure AlgebrasAnnals of Mathematics, 1946
- Untersuchungen ber das logische Schlie en. IMathematische Zeitschrift, 1935