IPC, the intuitionistic predicate calculus, has the property(i) Vc(A c /x) xA.Furthermore, for certain important , IPC has the converse property (ii) xA Vc(A c /x). (i) may be given up in various ways, corresponding to different philosophic intuitions and yielding different systems of intuitionistic free logic. The present paper proves the strong completeness of several of these with respect to Kripke style semantics. It also shows that giving up (i) need not force us to abandon the analogue of (ii).

In the First Antinomy of The Critique of Pure Reason, Kant drew two conclusions from the argument he gives. First, Kant took his argument to show that the referent of the concept of ‘world’ does not exist as a thing in itself. For at B532 he says.