with Va3n-Continuity Principle with parameters, Kripke*s Scheme KS ,
Uniformity Principle, Relativized Dependent Choice RDC , and Bar-Induction.
This result goes beyond [Gr2] (appendix A3, where a consistency proof is
suggested w.r.t. higher-order intuitionistic arithmetic): namely, all
principles considered contain parameters, and we allow them to vary over
the whole universe, not only over given types. Moreover, RDC was not con-
sidered in [Kr],[Gr2].
In section 4.2 we present Joyal•s forcing of spoiling the Heine-Borel
theorem, as an example of our general approach given in section 1.1. In
section 4.3. we force 2r to be subcountable, i.e. we generically intro-
duce a surjection from a subset of U onto In section 4.4., we give
a new topological model of ZFI with RDC, KS, and parameterless Va3n-
Continuity, and the Fan Theorem, in which Bar-Induction fails. (Recently,
the author has obtained an independence proof of the Fan Theorem from ZFI
with RDC and parameterless Va3n-Continuity [Sc2]).
Applications of forcing in non-set-theoretic situations (e.g. model-
theoretic Robinson forcing and the closely connected notion of a model
completion, cf. [R], [Kei])are studied in [BScl,2], Applications as [Fe],
[Bl] and the recent application to recursion theory [Ma]) are also
examples of the approach given in 1.1; we will address this in the future.
It seems there is no need to restrict outselves to forcing over models of
set theory (alternatively, looking at classifying topoi); the method given
in 1.1. should work on other levels as well.
The point of view taken here is to make the metatheory as weak as
possible. It turns out again and again that certain constructions naturally
"carry on" assumed additional structure (Axioms of Foundation and Replace-
ment are a case in point - cf. our remarks above on ZF-systems). In
particular, the Law of Excluded Middle makes its appearance rather more
rarely then it would be generally assumed. We always proceed by specifying
data (i.e. hypotheses of the theorem) and then apply a metamathematically
simple construction to such a given structure. We assume Excluded Middle
and Axiom of Choice for (the category of) Sets, but we also specify
crucial mathematical assumptions on which a construction really depends.