Hostname: page-component-cd9895bd7-jn8rn Total loading time: 0 Render date: 2024-12-24T19:43:12.170Z Has data issue: false hasContentIssue false
  • English
  • Français

Pretopologies and completeness proofs

Published online by Cambridge University Press:  12 March 2014

Giovanni Sambin
Giovanni Sambin*
Affiliation:
Dipartimento di Matematica Pura ed Applicata, Università degli Studi di Padova, 35131 Padova, Italy, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Extract

Pretopologies were introduced in [S], and there shown to give a complete semantics for a propositional sequent calculus BL, here called basic linear logic, as well as for its extensions by structural rules, ex falso quodlibet or double negation. Immediately after Logic Colloquium '88, a conversation with Per Martin-Löf helped me to see how the pretopology semantics should be extended to predicate logic; the result now is a simple and fully constructive completeness proof for first order BL and virtually all its extensions, including the usual, or structured, intuitionistic and classical logic. Such a proof clearly illustrates the fact that stronger set-theoretic principles and classical metalogic are necessary only when completeness is sought with respect to a special class of models, such as the usual two-valued models.

To make the paper self-contained, I briefly review in §1 the definition of pretopologies; §2 deals with syntax and §3 with semantics. The completeness proof in §4, though similar in structure, is sensibly simpler than that in [S], and this is why it is given in detail. In §5 it is shown how little is needed to obtain completeness for extensions of BL in the same language. Finally, in §6 connections with proofs with respect to more traditional semantics are briefly investigated, and some open problems are put forward.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 60 , Issue 3 , September 1995 , pp. 861 - 878
Copyright
Copyright © Association for Symbolic Logic 1995

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

[A]Abrusci, V. M., A sequent calculus for intuitionistic linear propositional logic, Mathematical logic (Petkov, P. P., editor), Plenum Press, New York, 1990, pp. 223–242.CrossRefGoogle Scholar
[BS]Battilotti, G. and Sambin, G., Pretopologies and a uniform presentation of sup-lattices, quantales and frames (to appear).Google Scholar
[G]Girard, J.-Y., Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102.CrossRefGoogle Scholar
[GL]Girard, J.-Y. and Lafont, Y., Linear logic and lazy computation, TAPSOFT '87, Lecture Notes in Computer Science, vol. 250, Springer-Verlag, Berlin, 1987, pp. 52–66.CrossRefGoogle Scholar
[KW]Ketonen, J. and Weyrauch, R., A decidable fragment of predicate calculus, Theoretical Computer Science, vol. 32 (1984), pp. 293–307.CrossRefGoogle Scholar
[ITT]Martin-Löf, P., Intuitionistic type theory, Bibliopolis, Naples, 1984.Google Scholar
[O1]Ono, H., Algebraic aspects of logics without structural rules, Proceedings of the international conference on algebra dedicated to the memory of A. I. Mal′cev, Contemporary Mathematics, vol. 131, part 3, American Mathematical Society, Providence, Rhode Island, 1992, pp. 601–621.Google Scholar
[O2]Ono, H., Semantics for substructural logics, Substructural logics (Došen, K. and Schroeder-Heister, P., editors), Oxford University Press, Oxford, 1993, pp. 259–291.CrossRefGoogle Scholar
[OK]Ono, H. and Komori, Y., Logics without the contraction rule, this Journal, vol. 50 (1985), pp. 169–201.Google Scholar
[R]Rosenthal, K., Quantales and their applications, Pitman Research Notes in Mathematics, vol. 234, Longman Scientific & Technical, Harlow, and Wiley, New York, 1990.Google Scholar
[IFS]Sambin, G., Intuitionistic formal spaces—a first communication, Mathematical logic and its applications (Skordev, D., editor), Plenum Press, New York, 1987, pp. 187–204.CrossRefGoogle Scholar
[S]Sambin, G., Intuitionistic formal spaces and their neighbourhood, Logic Colloquium '88 (Ferro, R.et al, editors), North-Holland, Amsterdam, 1989, pp. 261–285.Google Scholar
[S2]Sambin, G., The semantics of pretopologies, Substructural logics (Došen, K. and Schroeder-Heister, P., editors), Oxford University Press, Oxford, 1993, pp. 293–307.CrossRefGoogle Scholar
[T]Troelstra, A. S., Lectures on linear logic, CSLI Lecture Notes, no. 29, Center for the Study of Language and Information, Stanford University, Stanford, California, 1992.Google Scholar
[TvD]Troelstra, A. S. and van Dalen, D., Constructivism in mathematics: an introduction, North-Holland, Amsterdam, 1988.Google Scholar