Abstract
We describe an explicit construction of algebraic models for theories with non-standard elements either with classical or constructive logic. The corresponding truthvalue algebra in our construction is a complete algebra of subsets of some concrete decidable set. This way we get a quite finitistic notion of true which reflects a notion of the deducibility of a given theory. It enables us to useconstructive, proof-theoretical methods for theories with non-standard elements. It is especially useful in the case of theories with constructive logic where algorithmic properties are essential.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
S.C. Kleene, Introduction to Metamathematics,D. van Nostrand Co., New York, 1952.
A.G. Dragalin, Mathematical Intuitionism. Introduction to Proof Theory,Translations of AMS,67, 1988.
A. Robinson, Non-Standard Analysis,Studies in Logic and the Foundations of Mathematics, North-Holland, 1966.
M. Davis, Applied Nonstandard Analysis,A Wiley-Interscience Publication, 1977.
A.G. Dragalin, An explicit Boolean-valued model for non-standard arithmetic,Publicationes Mathematicae, Debrecen, 3–4,42, (1993), pp. 369–389.
H. Rasiowa andR. Sikorski, The Mathematics of Metamathematics (second ed.),PWN, Warszawa, 1968.
A.G. Dragalin, A Completeness Theorem for Higher-order Intuitionistic Logic. An Intuitionistic Proof., in: Mathematical Logic and its Applications (ed. Dimiter Skordev, Gödel session),Plenum Press, New York, 1987, pp. 107–124.
A.G. Dragalin, Cut-elimination Theorem for Higher-order Classical Logic. An Intuitionistic Proof., in: Mathematical Logic and its Applications (ed. Dimiter Skordev, Gödel session),Plenum Press, New York, 1987, pp. 243–252.
S.A. Kripke, Semantical Analysis of Intuitionistic Logic I., in: Formal Systems and Recursive Functions (Proc, Eighth Logic Colloq., Oxford, 1963),North-Holland, 1965, pp. 92–130.
A.G. Dragalin, Complete Heyting and Boolean algebras over a partial ordering. Constructive apporoaches,accepted in the Proc. of the Colloq. on Topology, János Bolyai Math. Soc., August 23–27, 1993, Szekszárd, Hungary; also as Technical Report No 93/80, University of Debrecen, Math. Inst., 1993.
A.N. Kolmogoroff andA.G. Dragalin, Introduction to Mathematical Logic.,Moscow University, 1982 (in Russian).
E. Mendelson, Introduction to Mathematical Logic, 3-rd ed.,Wodsworth and Brooks, Calif. 1987.
M. Takahashi, Cut-elimination theorem and Brouwerian-valued models for intuitionistic type theory,Comment. Math. Univ. St. Paul. 19, (1971), pp. 55–72.
A.G. Dragalin, The collapse of the descriptive complexity of truth definitions,Bull. of the Section of Logic,20, (1991), pp. 94–95.
A.G. Dragalin, ‘Completeness and cut-eleimination theorems in classical higher-order logics. Constructive methods’ (in Russian),Izvestiya VUZov, Moskva3, 1993, pp. 3–18.
Author information
Authors and Affiliations
Additional information
The research was supported partly by the Hungarian National Fundation for Scientific Research No. 1654.
Rights and permissions
About this article
Cite this article
Dragalin, A.G. Explicit algebraic models for constructive and classical theories with non-standard elements. Stud Logica 55, 33–61 (1995). https://doi.org/10.1007/BF01053031
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF01053031