{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T06:51:35Z","timestamp":1649141495023},"reference-count":10,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":13160,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1978,3]]},"abstract":"<jats:p>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.<\/jats:p><jats:p>In this paper we will only consider models <jats:italic>M<\/jats:italic> = \u2039<jats:italic>S<\/jats:italic>, <jats:italic>T<jats:sub>M<\/jats:sub><\/jats:italic>\u203a, where <jats:italic>S<\/jats:italic> is one fixed spreadlaw for all models <jats:italic>M<\/jats:italic>, 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, \u00a73].<\/jats:p><jats:p>The main tools in this paper will be two model-constructions:<\/jats:p><jats:p>(i) In \u00a71 we will consider, under a certain condition <jats:italic>C<\/jats:italic>(<jats:italic>M<\/jats:italic><jats:sub>0<\/jats:sub>, <jats:italic>M, s<\/jats:italic>), the construction of a model <jats:italic>R<\/jats:italic>(<jats:italic>M<\/jats:italic><jats:sub>0<\/jats:sub>, <jats:italic>M, s<\/jats:italic>) from two models <jats:italic>M<\/jats:italic><jats:sub>0<\/jats:sub> and <jats:italic>M<\/jats:italic> with respect to the finite sequence <jats:italic>s<\/jats:italic>.<\/jats:p><jats:p>(ii) In \u00a72 we will construct from an infinite sequence <jats:italic>M<\/jats:italic><jats:sub>0<\/jats:sub>, <jats:italic>M<\/jats:italic><jats:sub>1<\/jats:sub>, <jats:italic>M<\/jats:italic><jats:sub>2<\/jats:sub>, \u2026 of models a new model \u03a3<jats:sub><jats:italic>i<\/jats:italic>\u2208<jats:italic>IN<\/jats:italic><\/jats:sub><jats:italic>M<jats:sub>i<\/jats:sub><\/jats:italic>.<\/jats:p><jats:p>Syntactic proofs of the disjunction property and the explicit definability theorem are well known.<\/jats:p><jats:p>C. Smorynski [8] gave semantic proofs of these theorems with respect to Kripke models, however using classical metamathematics. In \u00a71 we will give intuitionistically correct, semantic proofs with respect to the models, defined in [7] using Brouwer's continuity principle.<\/jats:p><jats:p>Let <jats:italic>W<\/jats:italic> be the fan of all models (see [7, Theorem 2.7]) and let \u0393 be a countably infinite sequence of sentences.<\/jats:p>","DOI":"10.2307\/2271944","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:46:34Z","timestamp":1146951994000},"page":"3-12","source":"Crossref","is-referenced-by-count":3,"title":["First steps in intuitionistic model theory"],"prefix":"10.1017","volume":"43","author":[{"given":"H.","family":"de Swart","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200049847_ref001","first-page":"11","volume":"27","author":"Kleene","year":"1962","journal-title":"Disjunction and existence under implication in elementary intuitionistic formalisms"},{"key":"S0022481200049847_ref008","unstructured":"Smorynski C. A. , Investigations of intuitionistic formal systems by means of Kripke models, Dissertation, University of Illinois at Chicago Circle, 1973."},{"key":"S0022481200049847_ref009","first-page":"27","volume":"25","author":"Harrop","year":"1960","journal-title":"Concerning formulas of the types A \u2192 B \u2228 C, A \u2192 (Ex) B(x) in intuitionistic formal systems"},{"key":"S0022481200049847_ref005","first-page":"426","volume":"27","author":"Smiley","year":"1962","journal-title":"The independence of connectives"},{"key":"S0022481200049847_ref004","volume-title":"Natural deduction. A proof-theoretical study","author":"Prawitz","year":"1965"},{"key":"S0022481200049847_ref002","first-page":"155","volume":"4","author":"McKinsey","year":"1939","journal-title":"Proof of the independence of the primitive symbols of Heyting's calculus of propositions"},{"key":"S0022481200049847_ref003","doi-asserted-by":"publisher","DOI":"10.1111\/j.1755-2567.1968.tb00337.x"},{"key":"S0022481200049847_ref010","volume-title":"The Foundations of intuitionistic mathematics","author":"Kleene","year":"1965"},{"key":"S0022481200049847_ref007","first-page":"564","volume":"42","author":"de Swart","year":"1977","journal-title":"An intuitionistically plausible interpretation of intuitionistic logic"},{"key":"S0022481200049847_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BF01350671"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200049847","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T20:19:37Z","timestamp":1558988377000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200049847\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1978,3]]},"references-count":10,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1978,3]]}},"alternative-id":["S0022481200049847"],"URL":"https:\/\/doi.org\/10.2307\/2271944","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1978,3]]}}}