Outlook: Applications and Extensions of Definitional Reflection

We have not discussed computational issues here. Clausal definitions give rise to computational procedures as investigated and implemented in logic programming, and definitional reflection adds a strong component to such computation (see Hallnäs and Schroeder-Heister [31], Eriksson [17]). This computational aspect is important to proof-theoretic semantics. We should not only be able to give a definition of a semantically correct proof, where 'semantically' is understood in the sense of prooftheoretic semantics, we should also be interested in ways to construct such proofs that proceed according to such principles. Programming languages, theorem provers and proof editors based on inversion principles make important contributions to this task. Devising principles of proof construction that can be used for proof search is itself an issue of proof-theoretic semantics that is a desideratum in the philosophically dominated community. Theories that go beyond logic are of particular interest here, as theorems outside pure logic are what we normally strive for in reasoning.

If we want to deal with more advanced mathematical theories, stronger closure and reflection principles are needed. At an elementary level, clauses aB in a

definition can be used to describe function computation in the form

f (x1,..., xk )(x1,..., xk )

which is supposed to express that from the arguments x1,..., xk the value f (x1,

..., xk ) is obtained, so that by means of definitional reflection f (x1,..., xk ) can be

computed. More generally, one might describe functionals F by means of (infini-

tary) clauses the bodies of which describe the evaluation of functions f which are arguments of F (for some hints see Hallnäs [29, 30]). An instructive example is the analysis of abstract syntax (see McDowell and Miller [41]).

There are several other approaches that deal with the atomic level proof-theoretically, that is, with issues beyond logic in the narrower sense. These approaches include Negri and von Plato's [42] proof analysis, Brotherston and Simpson's [2] infinite derivations, or even derivations concerning subatomic expressions (see Wie˛ckowski [73]), and corresponding linguistic applications, as discussed by Francez and Dyckhoff [19] and Francez et al. [20]. Proof-theoretic semantics beyond logic is a broad field with great potential, the surface of which, thus far, has barely been scratched.

< Prev   CONTENTS   Next >