Edinburgh Research Archive >
Informatics, School of >
Informatics Publications >
Please use this identifier to cite or link to this item:
|Title: ||An Illative Theory of Relations|
|Authors: ||Plotkin, Gordon|
|Issue Date: ||3-Nov-2003|
|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.|
|Keywords: ||Laboratory for Foundations of Computer Science|
|Appears in Collections:||Informatics Publications|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.