INTRODUCTION

IX

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.