Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-11-20T11:46:04.692Z Has data issue: false hasContentIssue false
  • English
  • Français

Formal topologies on the set of first-order formulae

Published online by Cambridge University Press:  12 March 2014

Thierry Coquand ,
Sara Sadocco ,
Giovanni Sambin  and
Jan M. Smith
Thierry Coquand
Affiliation:
Department of Computing Science, Chalmers andUniversity of Göteborg, S- Göteborg, Sweden E-mail: [email protected]
Sara Sadocco
Affiliation:
Dipartimento di Matematica, Universita' di Siena, Via Del Capitano 15, 53100 Siena, Italy E-mail: [email protected]
Giovanni Sambin
Affiliation:
Dipartimento di Matematica Pura e Applicata, Universita' Di Padova, Via Belzoni 7, 35141 Padova, Italy E-mail: [email protected]
Jan M. Smith
Affiliation:
Department of Computing Science, Chalmers and University of Göteborg, S- Göteborg, Sweden E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Extract

The completeness proof for first-order logic by Rasiowa and Sikorski [13] is a simplification of Henkin's proof [7] in that it avoids the addition of infinitely many new individual constants. Instead they show that each consistent set of formulae can be extended to a maximally consistent set, satisfying the following existence property: if it contains (∃x)ϕ it also contains some substitution ϕ(y/x) of a variable y for x. In Feferman's review [5] of [13], an improvement, due to Tarski, is given by which the proof gets a simple algebraic form.

Sambin [16] used the same method in the setting of formal topology [15], thereby obtaining a constructive completeness proof. This proof is elementary and can be seen as a constructive and predicative version of the one in Feferman's review. It is a typical, and simple, example where the use of formal topology gives constructive sense to the existence of a generic object, satisfying some forcing conditions; in this case an ultrafilter satisfying the existence property.

In order to get a formal topology on the set of first-order formulae, Sambin used the Dedekind-MacNeille completion to define a covering relation ⊲DM. This method, by which an arbitrary poset can be extended to a complete poset, was introduced by MacNeille [9] and is a generalization of the construction of real numbers from rationals by Dedekind cuts. It is also possible to define an inductive cover, ⊲I, on the set of formulae, which can also be used to give canonical models, see Coquand and Smith [3].

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 65 , Issue 3 , September 2000 , pp. 1183 - 1192
Copyright
Copyright © Association for Symbolic Logic 2000

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]Bishop, E., Foundations of constructive analysis, McGraw-Hill, New York, 1967.Google Scholar
[2]Cederquist, J., A pointfree approach to constructive analysis in type theory, Ph.d. thesis, Chalmers University of Technology and University of Göteborg, Sweden, 1997.Google Scholar
[3]Coquand, T. and Smith, J. M., An application of constructive completeness, Proceedings of the Workshop TYPES '95, Torino, Italy, June 1995 (Berardi, and Coppo, , editors), Lecture Notes in Computer Science, no. 1158, Springer-Verlag, 1996, pp. 76–84.Google Scholar
[4]Dragalin, A. G., An explicit Boolean-valued model for non-standard arithmetic, Publicationes Mathematicae Drebecen, vol. 42 (1993), pp. 369–389.Google Scholar
[5]Feferman, S., Review of “A proof of the completeness theorem of Gödel” by H. Rasiowa and R. Sikorski, this Journal, vol. 17 (1952), no. 1, p. 72.Google Scholar
[6]Fourman, M. P. and Grayson, R. J., Formal Spaces, Brouwer Centenary Symposium (Troelstra, A. S. and van Dalen, D., editors), North-Holland, 1982, pp. 107–122.Google Scholar
[7]Henkin, L., The completeness of first-order functional calculus, this Journal, vol. 14 (1949), pp. 159–166.Google Scholar
[8]Johnstone, P. T., Open locales and exponentiation, Mathematical Applications of Category Theory, A.M.S. Contemporary Mathematical series, vol. 30, 1984.CrossRefGoogle Scholar
[9]MacNeille, H. M., Partially ordered sets, Transactions of the American Mathematical Society, vol. 42 (1937), pp. 416–460.CrossRefGoogle Scholar
[10]Moerdijk, I. and Palmgren, E., Minimal models of Heyting arithmetic, this Journal, vol. 62 (1997), no. 4, pp. 1448–1460.Google Scholar
[11]Nordström, B., Petersson, K., and Smith, J. M., Programming in Martin-Löf's type theory. an introduction., Oxford University Press, 1990.Google Scholar
[12]Persson, H., Constructive completeness of intuitionistic predicate logic: A formalisation in type theory, Licentiate Thesis, Chalmers University of Technology and University of Göteborg, Sweden, November 1996.Google Scholar
[13]Rasiowa, H. and Sikorski, R., A proof of the completeness theorem of Gödel, Fundamenta Mathematicae, vol. 37 (1950), pp. 193–200.CrossRefGoogle Scholar
[14]Sadocco, S., Topologie formali sull'insieme delle formule, Tesi di laurea, University of Padova, February 1996.Google Scholar
[15]Sambin, G., Intuitionistic Formal Spaces — A First Communication, Mathematical logic and its applications (Skordev, D., editor), Plenum, 1987, pp. 187–204.Google Scholar
[16]Sambin, G., Pretopologies and completeness proofs, this Journal, vol. 60 (1995), pp. 861–878.Google Scholar
[17]Sambin, G. and Valentini, S., Building up a toolbox for Martin-Löf's type theory: subset theory, Twenty-five years of constructive type theory (Sambin, Giovanni and Smith, Jan M., editors), Oxford University Press, 1998, pp. 221–244.CrossRefGoogle Scholar