We present relational proof systems for the four groups of theories of spatial reasoning: contact relation algebras, Boolean algebras with a contact relation, lattice-based spatial theories, spatial theories based on a proximity relation.

The period from 1900 to 1935 was particularly fruitful and important for the development of logic and logical metatheory. This survey is organized along eight "itineraries" concentrating on historically and conceptually linked strands in this development. Itinerary I deals with the evolution of conceptions of axiomatics. Itinerary II centers on the logical work of Bertrand Russell. Itinerary III presents the development of set theory from Zermelo onward. Itinerary IV discusses the contributions of the algebra of logic tradition, in particular, Löwenheim (...) and Skolem. Itinerary V surveys the work in logic connected to the Hilbert school, and itinerary V deals specifically with consistency proofs and metamathematics, including the incompleteness theorems. Itinerary VII traces the development of intuitionistic and many-valued logics. Itinerary VIII surveys the development of semantical notions from the early work on axiomatics up to Tarski's work on truth. (shrink)

We consider the problem of finding and classifying representations in algebraic logic. This is approached by letting two players build a representation using a game. Homogeneous and universal representations are characterized according to the outcome of certain games. The Lyndon conditions defining representable relation algebras (for the finite case) and a similar schema for cylindric algebras are derived. Finite relation algebras with homogeneous representations are characterized by first order formulas. Equivalence games are defined, and are used to establish whether an (...) algebra is ω-categorical. We have a simple proof that the perfect extension of a representable relation algebra is completely representable. An important open problem from algebraic logic is addressed by devising another two-player game, and using it to derive equational axiomatisations for the classes of all representable relation algebras and representable cylindric algebras. Other instances of this approach are looked at, and include the step by step method. (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.

We characterise the class S Ra CA n of subalgebras of relation algebra reducts of n -dimensional cylindric algebras by the notion of a ‘hyperbasis’, analogous to the cylindric basis of Maddux, and by representations. We outline a game–theoretic approximation to the existence of a representation, and how to use it to obtain a recursive axiomatisation of S Ra CA n.

We describe a relational framework that uniformly supports formalization and automated reasoning in varied propositional modal logics. The proof system we propose is a relational variant of the classical Rasiowa-Sikorski proof system. We introduce a compact graph-based representation of formulae and proofs supporting an efficient implementation of the basic inference engine, as well as of a number of refinements. Completeness and soundness results are shown and a Prolog implementation is described.

A prized property of theories of all kinds is that of generality, of applicability or least relevance to a wide range of circumstances and situations. The purpose of this article is to present a pair of distinctions that suggest that three kinds of generality are to be found in mathematics and logics, not only at some particular period but especially in developments that take place over time: ‘omnipresent’ and ‘multipresent’ theories, and ‘ubiquitous’ notions that form dependent parts, or moments, of (...) theories. The category of ‘facets’ is also introduced, primarily to assess the roles of diagrams and notations in these two disciplines. Various consequences are explored, starting with means of developing applied mathematics, and then reconsidering several established ways of elaborating or appraising theories, such as analogising, revolutions, abstraction, unification, reduction and axiomatisation. The influence of theories already in place upon theory-building is emphasised. The roles in both mathematics and logics of set theory, abstract algebras, metamathematics, and model theory are assessed, along with the different relationships between the two disciplines adopted in algebraic logic and in mathematical logic. Finally, the issue of monism versus pluralism in these two disciplines is rehearsed, and some suggestions are made about the special character of mathematical and logical knowledge, and also the differences between them. Since the article is basically an exercise in historiography, historical examples and case studies are described or noted throughout. (shrink)

Over the last twenty years, in all of these neighbouring fields, modal systems have been developed that we call multi-dimensional. (Our definition of multi ...

In Computer Science stepwise refinement of algebraic specifications is a well-known formal methodology for rigorous program development. This paper illustrates how techniques from Algebraic Logic, in particular that of interpretation, understood as a multifunction that preserves and reflects logical consequence, capture a number of relevant transformations in the context of software design, reuse, and adaptation, difficult to deal with in classical approaches. Examples include data encapsulation and the decomposition of operations into atomic transactions. But if interpretations open such a new (...) research avenue in program refinement, (conceptual) tools are needed to reason about them. In this line, the paper’s main contribution is a study of the correspondence between logical interpretations and morphisms of a particular kind of coalgebras. This opens way to the use of coalgebraic constructions, such as simulation and bisimulation, in the study of interpretations between (abstract) logics. (shrink)

This contribution is an essay of formal philosophy—and more specifically of formal ontology and formal epistemology—applied, respectively, to the philosophy of nature and to the philosophy of sciences, interpreted the former as the ontology and the latter as the epistemology of the modern mathematical, natural, and artificial sciences, the theoretical computer science included. I present the formal philosophy in the framework of the category theory (CT) as an axiomatic metalanguage—in many senses “wider” than set theory (ST)—of mathematics and logic, both (...) of the “extensional” logics of the pure and applied mathematical sciences (=mathematical logic), and the “intensional” modal logics of the philosophical disciplines (=philosophical logic). It is particularly significant in this categorical framework the possibility of extending the operator algebra formalism from (quantum and classical) physics to logic, via the so-called “Boolean algebras with operators” (BAOs), with this extension being the core of our formal ontology. In this context, I discuss the relevance of the algebraic Hopf coproduct and colimit operations, and then of the category of coalgebras in the computations over lattices of quantum numbers in the quantum field theory (QFT), interpreted as the fundamental physics. This coalgebraic formalism is particularly relevant for modeling the notion of the “quantum vacuum foliation” in QFT of dissipative systems, as a foundation of the notion of “complexity” in physics, and “memory” in biological and neural systems, using the powerful “colimit” operators. Finally, I suggest that in the CT logic, the relational semantics of BAOs, applied to the modal coalgebraic relational logic of the “possible worlds” in Kripke’s model theory, is the proper logic of the formal ontology and epistemology of the natural realism, as a formalized philosophy of nature and sciences. (shrink)

We prove, for each 4⩽ n ω , that S Ra CA n+1 cannot be defined, using only finitely many first-order axioms, relative to S Ra CA n . The construction also shows that for 5⩽n S Ra CA n is not finitely axiomatisable over RA n , and that for 3⩽m S Nr m CA n+1 is not finitely axiomatisable over S Nr m CA n . In consequence, for a certain standard n -variable first-order proof system ⊢ m (...) , n of m -variable formulas, there is no finite set of m -variable schemata whose m -variable instances, when added to ⊢ m , n as axioms, yield ⊢ m , n +1. (shrink)

Sound and complete semantics for classical propositional logic can be obtained by interpreting sentences as sets. Replacing sets with commuting dense binary relations produces an interpretation that turns out to be sound but not complete for R. Adding transitivity yields sound and complete semantics for RM, because all normal Sugihara matrices are representable as algebras of binary relations.

We study algebras whose elements are relations, and the operations are natural “manipulations” of relations. This area goes back to 140 years ago to works of De Morgan, Peirce, Schröder . Well known examples of algebras of relations are the varieties RCAn of cylindric algebras of n-ary relations, RPEAn of polyadic equality algebras of n-ary relations, and RRA of binary relations with composition. We prove that any axiomatization, say E, of RCAn has to be very complex in the following sense: (...) for every natural number k there is an equation in E containing more than k distinct variables and all the operation symbols, if 2 < n < ω. Completely analogous statement holds for the case n ω. This improves Monk's famous non-finitizability theorem for which we give here a simple proof. We prove analogous nonfinitizability properties of the larger varieties SNrnCAn + k. We prove that the complementation-free subreducts of RCAn do not form a variety. We also investigate the reason for the above “non-finite axiomatizability” behaviour of RCAn. We look at all the possible reducts of RCAn and investigate which are finitely axiomatizable. We obtain several positive results in this direction. Finally, we summarize the results and remaining questions in a figure. We carry through the same programme for RPEAn and for RRA. By looking into the reducts we also investigate what other kinds of natural algebras of relations are possible with more positive behaviour than that of the well known ones. Our investigations have direct consequences for the logical properties of the n-variable fragment Ln of first order logic. The reason for this is that RCAn and RPEAn are the natural algebraic counterparts of Ln while the varieties SNrnCAn + k are in connection with the proof theory of Ln. This paper appears in two parts. The first part contains the non-finite axiomatizability results. The present second part contains finite axiomatizations of some fragments together with a figure summarizing the finite and non-finite axiomatizability results in this area and the problems left open. (shrink)

ABSTRACT Propositional dynamic logic with converse and test, is enriched with complement, intersection and relational operations of weakest prespecification and weakest postspecification. Relational deduction system for the logic is given based on its interpretation in the relational calculus. Relational interpretation of the operators ?repeat? and ?loop? is given.

Using a variation of the rainbow construction and various pebble and colouring games, we prove that RRA, the class of all representable relation algebras, cannot be axiomatised by any first-order relation algebra theory of bounded quantifier depth. We also prove that the class At(RRA) of atom structures of representable, atomic relation algebras cannot be defined by any set of sentences in the language of RA atom structures that uses only a finite number of variables.

In this paper (the second of two parts) we propose a structural interpretation of Schröder’s work, pointing out his insistence on the priority of a whole in comparison with its parts. The examples are taken from the diverse areas in which Schröder was active, with a particular interest in his project of an absolute algebra.