# Triangular Logic of Partial Toposes

Triangular Logic of Partial Toposes We present a new method for proving theorems in the equational theory of partial maps over toposes introduced in the papers [C'089] and , The method is given by a system of rules of formation of proofs. The proofs of f( ) is defined' and the proofs of correctness ‘φ(f( ))' formed by application of the rules of the system are such that they contain a computation of the value f( ), where f is a partial function valued in natural numbers and 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 be also 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. AMS Subject Classification 1995: Primary: 68. Secondary: 18. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Applied Non-Classical Logics Taylor & Francis

# Triangular Logic of Partial Toposes

, Volume 10 (2): 40 – Jan 1, 2000
40 pages

## Triangular Logic of Partial Toposes

Abstract

We present a new method for proving theorems in the equational theory of partial maps over toposes introduced in the papers [C'089] and , The method is given by a system of rules of formation of proofs. The proofs of f( ) is defined' and the proofs of correctness ‘φ(f( ))' formed by application of the rules of the system are such that they contain a computation of the value f( ), where f is a partial function valued in natural numbers and is a vector of natural...  /lp/taylor-francis/triangular-logic-of-partial-toposes-vKqHmj4JsA
Publisher
Taylor & Francis
Copyright Taylor & Francis Group, LLC
ISSN
1958-5780
eISSN
1166-3081
DOI
10.1080/11663081.2000.10510995
Publisher site
See Article on Publisher Site

### Abstract

We present a new method for proving theorems in the equational theory of partial maps over toposes introduced in the papers [C'089] and , The method is given by a system of rules of formation of proofs. The proofs of f( ) is defined' and the proofs of correctness ‘φ(f( ))' formed by application of the rules of the system are such that they contain a computation of the value f( ), where f is a partial function valued in natural numbers and 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 be also 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. AMS Subject Classification 1995: Primary: 68. Secondary: 18.

### Journal

Journal of Applied Non-Classical LogicsTaylor & Francis

Published: Jan 1, 2000