An Illative Theory of Relations

Abstract

In a previous paper an intensional theory of relations was formulated [Plo90]. It was intended as a formalisation of some of the ideas of Situation Theory concerning relations, assignments, states-of-a airs and facts; it was hoped it could serve as a springboard for formalising other notions especially those concerning situations and propositions. The method chosen was to present a formal theory in a variation of classical first-order logic allowing terms with bound variables (and also quantification over function variables, but no axioms of choice). One infelicity of this work was that not every formula corresponded to a state-of-a airs according to a certain notion of internal definability; indeed one could show such correspondences inconsistent with the theory. Jon Barwise suggested changing the logic to allow partial predicates and partial functions. The idea of using a 3-valued approach is an old one: see [Fef84] for general information about results closely related to those given below. Another infelicity, pointed out by Peter Aczel, was that the logic formalised part of the metalanguage of the structures concerned, and these structures already had their own notion of proposition or, better, state-of-a airs. This meant that there was a repetition of logical apparatus; for example the logical conjunction was replicated by a conjunction for soas. In this paper we present a non-standard logic for our structures. It is a type-free intensional logic, and is also in the tradition of Curry’s illative logic [HS86]; see also [AczN, FM87, Smi84, MA88]. The logic has two judg- ments: that an object is a fact and that an object is a state-of-a airs (cf. truth and proposition). Objects are given using a variant of the traditional situation theory notation which is more standard, logically speaking, with explicit negation and quantification (see also [Bar87]). No metalinguistic apparatus is employed.