A remark on free choice sequences and the topological completeness proofs

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.