Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

The Language of T

Described 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 first-order logic, Heyting arithmetic, and accompanying consistency and faithfulness proofs. But whereas in [16] the Kreisel-Goodman 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 boolean-valued 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 “self-applicable” 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 st . 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. st 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 T

Goodman's axiomatization of T is based on a single conclusion sequent calculus relative to which Δ f-T st is assigned the intended interpretation “if all the equations in Δ hold, then st ”. The structural rules of the system include weakening and cut. Additionally, equality axioms for ≡ (e.g. f-T ss) as well as axioms governing the pairing operators (e.g. f-T 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 ≡ ⊥f-T s t Δ, π uv ≡Tf-T s t

Δ f-T st

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 f-T sx ≡ T.

As both Dec and ExpRfn play a role in the derivation of the Kreisel-Goodman

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 pre-theoretical 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 st 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 f-T should itself be interpreted as expressing a form of intuitionistic implication.

  • [1] The systems of [16, 17] do not officially have the abstraction operator in their language, but rather the traditional combinators S and K which may be used to mimic lambda abstracti on—e.g. in the manner described in [22, Sect. 2.2]. But as Goodman makes free use of λ-notation throughout both of his expositions (apparently via such an abbreviation), it will be here simpler to assume that the system includes λβ instead of the rules which Goodman takes to axiomatize the combinators. Until Sect. 5, we will also suppress discussion of a number of other primitive notions and their corresponding axioms pertaining to the treatment of so-called “grasped domains” which are introduced in the formulation of T ω
  • [2] Relative to this interpretation, π st can be understood as expressing the characteristic function of the assertion that s is a proof of the universal closure of the logical formula which s interprets. In the sequel, however, s will most often be closed. And thus it will often be possible to understand π st as simply expressing that t is a proof of the formula interpreted by s
  • [3] We will return in Sect. 5.4 to compare ExpRfn to the better known “implicit” reflection principle ∃x ProofT (x , 1φ1)φ.
 
Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics