Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics Publications >

Please use this identifier to cite or link to this item:

This item has been viewed 30 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
illative.pdf159.89 kBAdobe PDFView/Open
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.


Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy