×

Triangular logic of partial toposes. (English) Zbl 1033.03037

Summary: We present a new method for proving theorems in the equational theory of partial maps over toposes introduced by the author [ The logic of categories of partial functions and its applications. Diss. Math. 241 (1986; Zbl 0617.03041)]{} and the author and P.-L. Curien [ Inf. Comput. 80, 50–95 (1989; Zbl 0674.18001)]{}. The method is given by a system of rules of formation of proofs. The proofs of ‘\(f(\vec n)\) is defined’ and the proofs of correctness ‘\(\varphi(f(\vec n))\)’ formed by application of the rules of the system are such that they contain a computation of the value \(f(\vec n)\), where \(f\) is a partial function with values in the natural numbers and \(\vec n\) is a vector of natural numbers. We show that the system is complete, i.e., if an equation holds in every model then it has a proof formed by application of the rules of the system. The system is equipped with a method of visual presentation of proofs by nested commutative triangles, i.e. commutative triangles which contain in their interiors other commutative triangles which may also be nested. To provide formal foundations for the method of visual presentation of proofs, we give a mathematical description of nested commutative triangles in terms of directed graphs and graph homomorphisms.

MSC:

03G30 Categorical logic, topoi
03B70 Logic in computer science
18B25 Topoi
03C05 Equational classes, universal algebra in model theory
05C20 Directed graphs (digraphs), tournaments
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Curien, P.L. and Obtulowicz, A. 1989.Partiality, Cartesian Closedness, and Toposes50–95. Information and Computation, Vol. 80, No. 1
[2] Ehrig, H. and Kreowski, H.J. 1979.Pushout-Properties: An Analysis of Gluing Constructions for Graphs135–149. Math. Nachr. 91 · Zbl 0431.68069
[3] Lambek J., Introduction to Higher Order Categorical Logic, Cambridge (1986) · Zbl 0596.03002
[4] Mac Lane S., Categories for the Working Mathematician · Zbl 0232.18001 · doi:10.1007/978-1-4757-4721-8
[5] Makkai, M. 1997.Generalized sketches as a framework for completeness theorem. Part I49–79. Journal of Pure and Applied Algebra 115 · Zbl 0871.03045
[6] Obtulowicz A., The logic of categories of partial functions and its applications · Zbl 0367.18001
[7] Obtulowicz, A. 1987.Algebra of Constructions I. The Word Problem for Partial Algebras129–173. Information and Computation 73
[8] Troelstra A. S., Mathematical Investigation of Intuistic Arithmetic and Analysis, Lecture Notes in Mathematics 344 (1973)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.