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 \( t \neq 0 \)) 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 \( t \in F \) such that \( F \vdash A_D(t, y) \), where \( \exists x \forall y A_D(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 \( a \in F' \) there exists a closed term \( b \in F' \) such that \( F' \vdash A(a, b) \), then it must be the case already that in \( F \) we have a function \( c \) such that \( F \vdash A(x, c x) \). We sketch the proof of this here.
Theorem. Suppose that for all functional systems \( F' \supset F \) and closed term \( a \in F' \) of type \( \rho \) there exists a closed term \( b \in F' \) of type \( \tau \) such that \( F' \vdash A(a, b) \). Then, there exists a closed term \( c \in F \) of type \( \rho \to \tau \) such that \( F \vdash A(x, c x) \).
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] \in F \). We could then take \( c = \lambda 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 \( u_n[x^\rho] \) of all the formulas of \( F \) with a single free-variable of type \( \rho \). Let \( a \) be a new constant of type \( \rho \).
II. For each partial function \( p \colon \mathbb{N} \to 2 \) define \( F_p \) as \( F \) plus the new constant \( a \) and axioms $$ u_n[a] = \top $$ when \( p(n) \) is defined and \( p(n) = \top \) and $$ u_n[a] = \bot $$ when \( p(n) \) is defined and \( p(n) = \bot \). Note that \( F_p \) might not be a functional system.
III. Let us argue that for all total \( f \) there exists a closed term \( c_f \in F \) such that \( F_f \vdash A(a, c_f a) \). Because \( f \) is total, \( F_f \) is complete. But it is either consistent or inconsistent. If it is inconsistent then we can take \( c_f \) to be anything we wish. On the other hand, if \( F_f \) is consistent then it is a functional system which extends \( F \). By the assumption of the theorem we have a closed term \( b \in F_f \) such that \( F_f \vdash A(a, b) \). But \( b \) must be of the form \( t[a] \) for some \( t[x] \in F \). Hence, take \( c_f = \lambda x . t[x] \).
IV. Let \( U_A = \{ p \colon [n] \to 2 \; | \; \exists c_p \in F (F_p \vdash A(a, c_p a)) \} \) and \( O_p = \{ f \; | \; f \colon \mathbb{N} \to 2 \wedge p \prec f \} \). That is, \( U_A \) contains all the partial functions \( p \) for which III above already holds. And \( O_p \) is the open set of the Baire space defined by the partial function \( p \).
V. We have that \( 2^\mathbb{N} = \bigcup_{p \in U_A} O_p \). This follows because for any total \( f \in 2^\mathbb{N}\) we can see that in III we only use finitely many axioms of \( F_f \) to prove \( A(a, c_f a) \). So, for such finite approximation \( p \) the result also holds and \( f \in O_p \).
VI. Since \( 2^\mathbb{N} \) is compact, a finite cover exists, i.e. \( 2^\mathbb{N} = O_{p_0} \cup \ldots \cup O_{p_n} \).
VII. It is easy to see that the extra axioms of \( F_{p_i} \) can be equivalently written as a single formula \( P_i[a] \) such that \( F_{p_i} = F_{\emptyset} + P_i[a] \), where \( \emptyset \) denotes the everywhere undefined function.
VIII. Because we had a covering of \( 2^\mathbb{N} \) we have $$ F_{\emptyset} \vdash P_0[a] \vee \ldots \vee P_n[a]. $$
IX. Moreover, $$ F_{\emptyset} \vdash P_i[a] \to A(a, c_{p_i}(a)). $$
X. Finally, this means we have \( F \vdash P_0[x] \vee \ldots \vee P_n[x] \) and \( F \vdash P_i[x] \to A(x, c_{p_i}(x)) \). The desired function \( c \) can be defined by cases as \( c x = c_{p_i} x \) for the least \( i \leq n \) such that \( P_i[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:
Post a Comment