A logic of definitional reasoning

Desmond Fearnley-Sander
Department of Mathematics, University of Tasmania, GPO Box 252C, Hobart 7001, Australia.
dfs@hilbert.maths.utas.edu.au

Abstract

Definitional reasoning is a methodology that supports the creation of theories. A theory has a (structured, typed, variable-free) language and a meaning. A meaning is a referentially transparent function from the language to itself, that respects structure and preserves types. There is a well-defined notion of refinement of meaning that supports the evolution of theories. The practical problem of implementing a theory comes down to designing appropriate language and progressively refining meaning to capture the domain of interest.

In this paper we focus on the sentential aspect of definitional reasoning. There are nullary operators true and false and independent binary operators and, xor and sentence. The latter may be designed to capture provable equality. A critical point is that we may then distinguish a sentence p from the assertion that p is true, though both p and p=true are sentences. Derived operators include an idealistic (or classical) negation and a realistic (or constructive) negation. Entailment may be internalized and there is a derived modal operator `is provable' with the usual properties. We explore some simple aspects of the interplay that arises between structure and semantics.

The paper concludes with general remarks on definitional reasoning as a paradigm for the construction of theories and for computation within theories.

Conference Home Page