Hostname: page-component-586b7cd67f-t7fkt Total loading time: 0 Render date: 2024-11-25T03:27:22.871Z Has data issue: false hasContentIssue false
  • English
  • Français

First steps in intuitionistic model theory

Published online by Cambridge University Press:  12 March 2014

H. de Swart
H. de Swart*
Affiliation:
Filosofisch Instituut, Erasmuslaan 40, Nijmegen, Netherlands
Get access Rights & Permissions [Opens in a new window]

Extract

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.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 43 , Issue 1 , March 1978 , pp. 3 - 12
Copyright
Copyright © Association for Symbolic Logic 1978

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Kleene, S. C., Disjunction and existence under implication in elementary intuitionistic formalisms, this Journal, vol. 27 (1962), pp. 11–17.Google Scholar
[2]McKinsey, J., Proof of the independence of the primitive symbols of Heyting's calculus of propositions, this Journal, vol. 4 (1939), pp. 155–158.Google Scholar
[3]Segerberg, K., Prepositional logics related to Heyting's and Johansson's, Theoria, vol. 34 (1968), pp. 26–61.CrossRefGoogle Scholar
[4]Prawitz, D., Natural deduction. A proof-theoretical study, Almqvist & Wiksell, Stockholm, 1965.Google Scholar
[5]Smiley, T., The independence of connectives, this Journal, vol. 27 (1962), pp. 426–436.Google Scholar
[6]Scarpellini, B., Some applications of Gentzen's second consistency proof, Mathematische Annalen, vol. 181 (1969), pp. 325–344.CrossRefGoogle Scholar
[7]de Swart, H., An intuitionistically plausible interpretation of intuitionistic logic, this Journal, vol. 42 (1977), pp. 564–578.Google Scholar
[8]Smorynski, C. A., Investigations of intuitionistic formal systems by means of Kripke models, Dissertation, University of Illinois at Chicago Circle, 1973.Google Scholar
[9]Harrop, R., Concerning formulas of the types A → B ∨ C, A → (Ex) B(x) in intuitionistic formal systems, this Journal, vol. 25 (1960), pp. 27–32.Google Scholar
[10]Kleene, S. C. and Vesley, R. E., The Foundations of intuitionistic mathematics, North-Holland, Amsterdam, 1965.Google Scholar