| Abstrakt: |
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 Sis 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 M0and Mwith respect to the finite sequence s.(ii) In §2 we will construct from an infinite sequence M0, M1, M2, … of models a new model Si?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 Wbe the fan of all models (see [7, Theorem 2.7]) and let G be a countably infinite sequence of sentences. |
