The ${\bf Q}$-consistency of ${\cal F}_{22}$.
Jonathan P. Seldin · Notre Dame Journal of Formal Logic · 1977
In his [CSC],1 Curry proved the consistency of a system, which he there defines and calls 922, and which is closely related to the system 9$λ of [CLg.Il] §15C.2 This is essentially a type-free intuitionistic predicate calculus without conjunction, alternation, or negation but with quantification over propositions and propositional functions. However, Curry's consistency proof is rather weak, since it only proves that every theorem of the system belongs to a class of obs (terms) which are defined to be canonical (called canobs) and since the canobs are those obs which are to be interpreted as propositions this proof leaves open the possibility that every ob which is to be interpreted as a proposition is a theorem of the