Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

An Overview of the Theory of Constructions

Versions of the Theory of Constructions were presented by Kreisel [25, 26], and Goodman [16–18]. The details of the notation and formal systems formulated in these papers differ in several respects. Our goal here will thus not be to present a systematic exposition of the different formalisms proposed by Kreisel and Goodman, nor even to provide a complete formulation of any one of them. Rather we shall simply attempt to set down some of the common characteristics of these systems with the dual goals of explaining how Kreisel and Goodman proposed to use the language of the Theory of Constructions to formalize Kreisel's reformulation of the BHK clauses and also to be able to reconstruct as closely as possible the reasoning of the Kreisel-Goodman paradox.

In so doing, we will adhere as closely as possible to the notation and terminology of the unstratified (or “naive”) theory (which we will henceforth refer to as T ) which is sketched by Goodman [17] in the course of expositing the paradox. (This system should be understood in contradistinction to the stratified theory T ω which Goodman officially adopts.5) Before offering a formal description of T , however, it will be useful for orientation to record several of its features which are remarked on by Sundholm [39]:

(I) The system T treats proofs as constructions s, t, u,.. ., which themselves are understood as mathematical objects whose properties the theory attempts to axiomatize.

(II) Using the theory it is possible to define a decidable predicate Π( A, s) with the

intended interpretation “construction s proves proposition A”.

(III) Statements of the latter form are themselves treated by the theory as propositions which may themselves admit to proof. In particular, it is possible within the theory to formulate statements such as Π (Π( A, s), t ) (i.e. “construction t proves that construction s is a proof of A”).

It would appear that the ability to iterate the application of the predicate Π( A, s)

is necessary if we are to formalize clauses such as (P2

→ ). But note that if this is

allowed, it must also be acknowledged that the constructions must play a dual role

in T —e.g. if ( p, q) is a pair satisfying the proof conditions of AB per (P2 ),

then q is understood as a process (i.e. a method for transforming proofs of A into proofs of B), while q is regarded as an object (i.e. a completed proof that q has the required property). Sundholm [39, pp. 164–167] suggests that these two notions must be carefully distinguished if we are to develop a theory of constructions which is faithful to Heyting's original interpretation of the connectives. He also suggests (at least implicitly) that Kreisel may have conflated them in his own formulations of T . But although this concern might be taken to call for reconsideration of the theory on historical grounds, the perspective which we will adopt here is that the specific proposals of Kreisel and Goodman are of interest in their own right.

 
Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics