Intuitionistic typical ambiguity (Q757362)

This paper is about typical ambiguity as defined for Russell's Simple Type Theory (TT) by \textit{E. Specker} [Logic, Methodology and Philosophy of Science, Proc. 1960 Int. Congr. 116-124 (1962; Zbl 0156.021)]. It proves, in a model theoretical way, an intuitionistic version of Specker's results, including the equi-consistency of \(TT^*\) and NF, where \(TT^*\) is obtained by adding ``ambiguity axioms'' to an intuitionistic version of TT, and NF is an intuitionistic version of Quine's ``New Foundations''. The paper includes some results in Kripke model theory (a.o. a saturation theorem). Finally, two classically equivalent formulations of the ambiguity axiom schema are proved not to be intuitionistically equivalent.