We present a dual tableau system, RLK, which is itself a deterministic decision procedure verifying validity of K-formulas. The system is constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. Furthermore, we describe an implementation of the system in Prolog, and we show some of its advantages.

This paper introduces Basic Intuitionistic Set Theory BIST, and investigates it as a first-order set theory extending the internal logic of elementary toposes. Given an elementary topos, together with the extra structure of a directed structural system of inclusions on the topos, a forcing-style interpretation of the language of first-order set theory in the topos is given, which conservatively extends the internal logic of the topos. This forcing interpretation applies to an arbitrary elementary topos, since any such is equivalent to (...) one carrying a dssi. We prove that the set theory BIST+Coll is sound and complete relative to forcing interpretations in toposes with natural numbers object . Furthermore, in the case that the structural system of inclusions is superdirected, the full Separation schema is modelled. We show that all cocomplete and realizability toposes can be endowed with such superdirected systems of inclusions.A large part of the paper is devoted to an alternative notion of category-theoretic model for BIST, which, following the general approach of Joyal and Moerdijkʼs Algebraic Set Theory, axiomatizes the structure possessed by categories of classes compatible with BIST. We prove soundness and completeness results for BIST relative to the class-category semantics. Furthermore, BIST+Coll is complete relative to the restricted collection of categories of classes given by categories of ideals over elementary toposes with nno and dssi. It is via this result that the completeness of the original forcing interpretation is obtained, since the internal logic of categories of ideals coincides with the forcing interpretation. (shrink)

In 1941, Tarski published an abstract, finitely axiomatized version of the theory of binary relations, called the theory of relation algebras, He asked whether every model of his abstract theory could be represented as a concrete algebra of binary relations. He and Jonsson obtained some initial, positive results for special classes of abstract relation algebras. But Lyndon showed, in 1950, that in general the answer to Tarski's question is negative. Monk proved later that the answer remains negative even if one (...) adjoins finitely many new axioms to Tarski's system. In this paper we describe a far-reaching generalization of the positive results of Jonsson and Tarski, as well as of some later, related results of Maddux. We construct a class of concrete models of Tarski's axioms-called coset relation algebras-that are very close in spirit to algebras of binary relations, but are built using systems of groups and cosets instead of elements of a base set. The models include all algebras of binary relations, and many non-representable relation algebras as well, We prove that every atomic relation algebra satisfying a certain measurability condition-a condition generalizing the conditions imposed by Jonsson and Tarski-is essentially isomorphic to a coset relation algebra. The theorem raises the possibility of providing a positive solution to Tarski's problem by using coset relation algebras instead of the standard algebras of binary relations. (shrink)

A connection between Aristotle's syllogistic and the calculus of relations is investigated. Aristotle's and Gergonne's syllogistics are considered as some algebraic structures. It is proved that Gergonne's syllogistic is isomorphic to closed elements algebra of a proper approximation relation algebra. This isomorphism permits to evaluate Gergonne's syllogisms and also Aristotle's syllogisms, laws of conversion and relations in the "square of oppositions" by means of regular computations with Boolean matrices.

ABSTRACT In this paper it is shown that a broad class of propositional logics can be interpreted in an equational logic based on fork algebras. This interpetability enables us to develop a fork-algebraic formalization of these logics and, as a consequence, to simulate non-classical means of reasoning with equational theories algebras.

Alfred Tarski’s influence on computer science was indirect but significant in a number of directions and was in certain respects fundamental. Here surveyed is Tarski’s work on the decision procedure for algebra and geometry, the method of elimination of quantifiers, the semantics of formal languages, model-theoretic preservation theorems, and algebraic logic; various connections of each with computer science are taken up.

The standard model for mereotopological structures are Boolean subalgebras of the complete Boolean algebra of regular closed subsets of a nonempty connected regular T 0 topological space with an additional "contact relation" C defined by xCy x ØA (possibly) more general class of models is provided by the Region Connection Calculus (RCC) of Randell et al. We show that the basic operations of the relational calculus on a "contact relation" generate at least 25 relations in any model of the RCC, (...) and hence, in any standard model of mereotopology. It follows that the expressiveness of the RCC in relational logic is much greater than the original 8 RCC base relations might suggest. We also interpret these 25 relations in the the standard model of the collection of regular open sets in the two-dimensional Euclidean plane. (shrink)

Contact relations have been studied in the context of qualitative geometry and physics since the early 1920s, and have recently received attention in qualitative spatial reasoning. In this paper, we present a sound and complete proof system in the style of Rasiowa and Sikorski (1963) for relation algebras generated by a contact relation.

Unifiability of terms (and formulas) and structural completeness in the variety of relation algebras RA and in the products of modal logic S5 is investigated. Nonunifiable terms (formulas) which are satisfiable in varieties (in logics) are exhibited. Consequently, RA and products of S5 as well as representable diagonal-free n-dimensional cylindric algebras, RDfn, are almost structurally complete but not structurally complete. In case of S5n a basis for admissible rules and the form of all passive rules are provided.

One of the most significant discoveries of early twentieth century mathematical logic was a workable definition of ‘ordered pair’ totally within set theory. Norbert Wiener, and independently Casimir Kuratowski, are usually credited with this discovery. A definition of ‘ordered pair’ held the key to the precise formulation of the notions of ‘relation’ and ‘function’ — both of which are probably indispensable for an understanding of the foundations of mathematics. The set-theoretic definition of ‘ordered pair’ thus turned out to be a (...) key victory for logicism, providing one admits set theory is logic. The definition also was instrumental in achieving the appearance of ontological economy — since it seemed only sets were needed — although this feature was emphasized only later. (shrink)

Our purpose in this paper is to delineate an ontology for quantum mechanics that results adequate to the formalism of the theory. We will restrict our aim to the search of an ontology that expresses the conceptual content of the recently proposed modal-Hamiltonian interpretation, according to which the domain referred to by non-relativistic quantum mechanics is an ontology of properties. The usual strategy in the literature has been to focus on only one of the interpretive problems of the theory and (...) to design an interpretation to solve it, leaving aside the remaining difficulties. On the contrary, our aim in the present work is to formulate a “global” solution, according to which different problems can be adequately tackled in terms of a single ontology populated of properties, in which systems are bundles of properties. In particular, we will conceive indistinguishability between bundles as a relation derived from indistinguishability between properties, and we will show that states, when operating on combinations of indistinguishable bundles, act as if they were symmetric with no need of a symmetrization postulate. (shrink)

In this paper, we obtain axiom systems, bases of identities and quasi-identities for classes of algebras of binary relations with a conjunctive operation, i.e., an operation that can be defined by a logical formula containing only conjunctions. The result of applying such an operation to two binary relations is the Cartesian product of their reflexive projections. Our consideration of these classes leads to the concept of quasi-semilattices as a natural generalization of the notion of semilattices.

Relevance logics are known to be sound and complete for relational semantics with a ternary accessibility relation. This paper investigates the problem of adequacy with respect to special kinds of dynamic semantics (i.e., proper relation algebras and relevant families of relations). We prove several soundness results here. We also prove the completeness of a certain positive fragment of R as well as of the first-degree fragment of relevance logics. These results show that some core ideas are shared between relevance logics (...) and relation algebras. Some details of certain incompleteness results, however, pinpoint where relevance logics and relation algebras diverge. To carry out these semantic investigations, we define a new tableaux formalization and new sequent calculi (with the single cut rule admissible) for various relevance logics. (shrink)

It is shown that Tarski’s set of ten axioms for the calculus of relations is independent in the sense that no axiom can be derived from the remaining axioms. It is also shown that by modifying one of Tarski’s axioms slightly, and in fact by replacing the right-hand distributive law for relative multiplication with its left-hand version, we arrive at an equivalent set of axioms which is redundant in the sense that one of the axioms, namely the second involution law, (...) is derivable from the other axioms. The set of remaining axioms is independent. Finally, it is shown that if both the left-hand and right-hand distributive laws for relative multiplication are included in the set of axioms, then two of Tarski’s other axioms become redundant, namely the second involution law and the distributive law for converse. The set of remaining axioms is independent and equivalent to Tarski’s axiom system. (shrink)

A series of nonrepresentable relation algebras is constructed from groups. We use them to prove that there are continuum many subvarieties between the variety of representable relation algebras and the variety of coset relation algebras. We present our main construction in terms of polygroupoids.

Nathan Houser, Don D. Roberts and James Van Evra (eds), Studies in the Logic of Charles Sanders Peirce, In:Bloomington and Indianapolis, Indiana University Press, 1997, xiii + 653 pp. £41.95. ISBN 0-253-33020-3.