Processing math: 100%

Friday, 16 August 2013

Kripke models and the dialectica interpretation


Few people know that Girard's PhD dissertation contained some results about Gödel's dialectica interpretation. As a fan of both Girard and the dialectica interpretation I feel I have to explain this rather unknown bit of Girard's work here.

The result I mention is in part IV of his dissertation, and was published in [1]. It is an interesting connection between validity in a certain Kripke structure and validity with respect to the dialectica interpretation. Not only is the result interesting, but the proof as well is quite clever, involving an unexpected use of the fan theorem in the form of "any open convering of a compact set has a finite sub-covering".

More precisely, let any quantifier-free extension F of system T which is consistent and complete (i.e. for any term t of ground type F proves exactly one of either t=0 or t0) be called a functional system. Consider the Kripke structure where worlds are functional systems, with the pre-order on the worlds being the relation "subsystem of". Girard's main result is that a formula A is valid at a node F if and only if there exists a closed term tF such that FAD(t,y), where xyAD(x,y) is the dialectica interpretation of A. The most difficult part of the proof is to show that if in any extension F of F and any closed term aF there exists a closed term bF such that FA(a,b), then it must be the case already that in F we have a function c such that FA(x,cx). We sketch the proof of this here.

Theorem. Suppose that for all functional systems FF and closed term aF of type ρ there exists a closed term bF of type τ such that FA(a,b). Then, there exists a closed term cF of type ρτ such that FA(x,cx).

Note that without the assumption of completeness of functional systems the result would be easy. Just take F to be F with a single new constant a. Then, by the assumption there would be a closed term b in the language of F plus the new constant. So, it would have to be t[a] for some t[x]F. We could then take c=λx.t[x]. The problem is that we can only consider extensions F of F which are functional systems, i.e. consistent and complete.

The proof goes as follows:

I. Consider an enumeration un[xρ] of all the formulas of F with a single free-variable of type ρ. Let a be a new constant of type ρ.

II. For each partial function p:N2 define Fp as F plus the new constant a and axioms un[a]= when p(n) is defined and p(n)= and un[a]= when p(n) is defined and p(n)=. Note that Fp might not be a functional system.

III. Let us argue that for all total f there exists a closed term cfF such that FfA(a,cfa). Because f is total, Ff is complete. But it is either consistent or inconsistent. If it is inconsistent then we can take cf to be anything we wish. On the other hand, if Ff is consistent then it is a functional system which extends F. By the assumption of the theorem we have a closed term bFf such that FfA(a,b). But b must be of the form t[a] for some t[x]F. Hence, take cf=λx.t[x].

IV. Let UA={p:[n]2|cpF(FpA(a,cpa))} and Op={f|f:N2pf}. That is, UA contains all the partial functions p for which III above already holds. And Op is the open set of the Baire space defined by the partial function p.

V. We have that 2N=pUAOp. This follows because for any total f2N we can see that in III we only use finitely many axioms of Ff to prove A(a,cfa). So, for such finite approximation p the result also holds and fOp.

VI. Since 2N is compact, a finite cover exists, i.e. 2N=Op0Opn.

VII. It is easy to see that the extra axioms of Fpi can be equivalently written as a single formula Pi[a] such that Fpi=F+Pi[a], where denotes the everywhere undefined function.

VIII. Because we had a covering of 2N we have FP0[a]Pn[a].

IX. Moreover, FPi[a]A(a,cpi(a)).

X. Finally, this means we have FP0[x]Pn[x] and FPi[x]A(x,cpi(x)). The desired function c can be defined by cases as cx=cpix for the least in such that Pi[x] holds.

[1] Jean-Yves Girard, Functional interpretations and Kripke models. Logic and Foundations of Mathematics and Computability Theory. The University of Western Ontario Series in Philosophy of Science, volume 9, 33-57, 1977.


No comments: