Home Philosophy Advances in ProofTheoretic Semantics
The Language of TDescribed in general terms, T is an equational term calculus with pairing, projection, and lambda abstraction operators, application, as well as various other primitive terms 5Goodman's dissertation [16] provides the most comprehensive exposition of T ω , inclusive of the interpretation of intuitionistic firstorder logic, Heyting arithmetic, and accompanying consistency and faithfulness proofs. But whereas in [16] the KreiselGoodman paradox is presented informally, [17] contains a more detailed derivation in theory (similar or identical to what we will call T +) which is similar to the “starred” variant originally described by Kreisel [25]. We will discuss these systems in greater detail in the context of evaluating Goodman and Kreisel's response to the paradox in Sect. 5. and predicates (which are formalized as booleanvalued terms). The terms of the theory are intended to denote “constructions” which can be understood simultaneously as either proofs or operations on proofs—i.e. what the theory seeks to axiomatize is a notion of “selfapplicable” proof. The distinctive feature of all versions of the Theory of Constructions is the inclusion of a proof operator π whose intended role can be most readily described as that of axiomatically mimicking certain properties of a traditional proof predicate ProofT(x , y) for an arithmetical theory T (such as Peano or Heyting arithmetic). More formally, the class of terms of T is defined by the grammar t : : = x T⊥ (D(tt )) (D1(t )) (D2(t )) (λx .t ) (tt ) (π tt ) where x , y, z,... are variables, T and ⊥ are intended to denote the truth values true and false, D(st ) is intended to denote the pair (s, t ), Di (t ) is intended to denote the first (i = 1) or second (i = 2) member of t if t is a pair and is undefined otherwise, and λx .t (i.e. abstraction) and st (i.e. application) are defined as usual in the untyped lambda calculus. The formulas of T are equations of the form s ≡ t . Note, however, that implicit in Goodman's [17] (and previously Kreisel's [25]) decision to base the Theory of Constructions on the untyped lambda calculus is that terms of the theory may be undefined. The relation ≡ is thus intended to denote a notion of intensional identity between terms—i.e. s ≡ t is intended to hold just in case s and t are both defined and reduce to the same normal form under βconversion. The Axiomatization of TGoodman's axiomatization of T is based on a single conclusion sequent calculus relative to which Δ fT s ≡ t is assigned the intended interpretation “if all the equations in Δ hold, then s ≡ t ”. The structural rules of the system include weakening and cut. Additionally, equality axioms for ≡ (e.g. fT s ≡ s) as well as axioms governing the pairing operators (e.g. fT Di (Ds1s2) ≡ si ) are adopted. We will assume that lambda terms are axiomatized by the formal theory λβ of [22, p. 70] ^{[1]}. The most significant axioms of T are those pertaining to the binary operator π . Goodman [17, p. 107] describes the intended interpretation of this symbol as follows: π st ≡ Tif and only if t is a proof that for all x , sx ≡ T Thus an equation of the form of the π st ≡ T is intended to express that t is a construction which serves as a proof of the fact that for all x the term sx reduces to the value T.7 One of the rules which is assumed to hold of π is intended to express that the proof relation described in Sect. 2 is decidable. This is achieved as follows: (Dec) Δ, π uv ≡ ⊥fT s ≡ t Δ, π uv ≡TfT s ≡ t Δ fT s ≡ t The other principle which is assumed to hold of π is a form of reflection principle stating that if the proof relation holds between s and t then sx is true: (ExpRfn) π st ≡ T fT sx ≡ T. As both Dec and ExpRfn play a role in the derivation of the KreiselGoodman paradox, it will be useful to say something additional both about their motivation and also their formulation in the Theory of Constructions. As we have observed in Sect. 2, the decidability of the proof relation appears to have a strong pretheoretical basis in the intuitionists' desire to view the BHK clauses as providing a decidable proof condition for formulas of arbitrary logical complexity. Although T does not contain any primitive relation symbols itself, a term α can be understood as expressing a binary relation just in case for all pairs of terms s, t , if αst is defined, then αst ≡ T or αst ≡ ⊥ may be derived in the theory. The decidability of such a relation α may then be expressed by stating that αst is defined for all pairs of terms s, t —i.e. that α is bivalent^{[2]}. This is what is formulated proof theoretically by the rule Dec in the case of the term π —i.e. in order to exclude the “third” case that π uv is undefined, we stipulate that it is sufficient to conclude s ≡ t from Δ if this equation is derivable from both the hypotheses Δ, π uv ≡ T and also Δ, π uv ≡ ⊥. ExpRfn is a form of what we will call an explicit reflection principle (cf. [1])—i.e. an expression of the fact that if the proof relation holds between a constructive proof p and a formula A, then we can conclude that A is true. Kreisel [25, p. 204] remarks of such a principle that it is “obvious on the intended interpretation” of π . In the arithmetical case, we would typically express this using a conditional statement of the form ProofT(n, 'φ') → φ, all of whose instances are both valid in the standard model and provable in even weak arithmetical systems T ^{[3]}. But since the Theory of Constructions does not contain a sign for implication in its object language, this is expressed in T by the rule ExpRfn which allows us to conclude sx ≡ T for all x from the premise π st ≡ T. As Goodman [17, p. 106] observes, in this sense the derivability relation fT should itself be interpreted as expressing a form of intuitionistic implication.

< Prev  CONTENTS  Next > 

Related topics 