###
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