On the extension of intuitionistic propositional logic with Kreisel-Putnam's and Scott's schemes

LetSKP be the intermediate prepositional logic obtained by adding toI (intuitionistic p.l.) the axiom schemes:S = ((? ?α→α)→α∨ ?α)→ ?α∨ ??α (Scott), andKP = (?α→β∨γ)→(?α→β)∨(?α→γ) (Kreisel-Putnam). Using Kripke's semantics, we prove:

1. SKP has the finite model property;
2. SKP has the disjunction property.

In the last section of the paper we give some results about Scott's logic S = I+S.