First steps in intuitionistic model theory

In this paper we will do some model theory with respect to the models, defined in [7] and, as in [7], we will work again in intuitionistic metamathematics.In this paper we will only consider models M = ‹S, TM›, where S is one fixed spreadlaw for all models M, namely the universal spreadlaw. That we can restrict ourselves to this class of models is a consequence of the completeness proof, which is sketched in [7, §3].The main tools in this paper will be two model-constructions:(i) In §1 we will consider, under a certain condition C(M0, M, s), the construction of a model R(M0, M, s) from two models M0 and M with respect to the finite sequence s.(ii) In §2 we will construct from an infinite sequence M0, M1, M2, … of models a new model Σi∈INMi.Syntactic proofs of the disjunction property and the explicit definability theorem are well known.C. Smorynski [8] gave semantic proofs of these theorems with respect to Kripke models, however using classical metamathematics. In §1 we will give intuitionistically correct, semantic proofs with respect to the models, defined in [7] using Brouwer's continuity principle.Let W be the fan of all models (see [7, Theorem 2.7]) and let Γ be a countably infinite sequence of sentences.