Revisions to The true reason for the incompleteness of formal systems

Stuff on infinite types.

Source Link

edited Jun 5 at 9:58

119
3

$$ Y : \mu T . (T \to T) \to T. $$$$ Y = (\lambda f : T \to T) \big( (\lambda x: \mu A . A \to T). f (x x) \big) \big( (\lambda x: \mu A . A \to T). f (x x) \big) : (T \to T) \to T$$

AndNote that the $\mu$ types appear in the typing of the inner terms. In type systems that interpret $\forall$ such as with parametric polymorphism parametric polymorphism (this may not be correct…$\lambda P$):

$$ Y : \forall T . (T \to T) \to \forall T . (T \to T). $$ or dependent types ($\lambda \omega$) $Y$ can get a type as well, but the important point of this is addressed later (see Lambda Cube for a discussion of these type systems).

Relating the type of the $Y$-combinator and Godel's claim

Recall the claim that:

The true source of the incompleteness, is to be found ... in the fact that the formation of ever higher types can be continued into the transfinite

In type theory, the formation of ever higher types would correspond to using a type constructor, i.e. in $\lambda^{\to}$ that would be '$\to$.' For example, given types $A$ and $B$, we form the type $A \to B$, written more obscurely as $\to(A, B)$. When dealing with types mathematically, especially when considering recursive types, it can be convenient to think of types as trees, as demonstrated by this figure from Pierce's book:

In this figure, the labels 1 and 2 are just labels to identify positions and arity, and Top is some given base type (typically a type inhabited by a single element, like $\{\cdot\}$ or x = x - that these types exist and are inhabited are some axioms of the system). The type on the right of the figure is in fact an infinite type, as is hinted by the ellipsis. In $\mu$ notation it would be written:

$$ \mu T . \mathrm{Top} \to T $$

This can be interpreted as an (extended) equation:

$$ T = \mathrm{Top} \to T = \mathrm{Top} \to (\mathrm{Top} \to T) = \mathrm{Top} \to (\mathrm{Top} \to (\mathrm{Top} \to T))$$

(Here we get the continued equation by substituting the definition of $T$ for $T$ over and over again.)

This same procedure of unfolding the type definition from $\mu$ can be repeated with the inner types of the $Y$-combinator, revealing that there is an infinite type. Recall the type of the parameter of the inner term of $Y$:

$$ \mu A . A \to T$$

This is nearly the same as the infinite type shown above, but instead of "extending to the right" it will "extend to the left."

Unfortunately, $\mu$ doesn't correspond so nicely to logic. In other type systems, in particular when we have parametric polymorphism or dependent types, we need to interpret the $\forall$ symbol. But this is where the infinite type is hidden in these systems. In the notes above, $\forall$ is interpreted as an (transfinite) product, while in other systems it is interpreted as a natural transformation (see Bartosz Milewski's discussion of natural transformations in Category Theory for Programmers). In either case, we get infinite types if there is an infinite number of types.

The idea here is that when we can interpret:

$$ \forall x \phi(x) = \phi(x_1) \land \phi(x_2) \land \phi(x_3) ... $$

Where $x_1, x_2$ is an enumeration of all members of the domain. Don't ask what if the members aren't enumerable?, it's not relevant.

To truly wrap up Godel's claim we would need to show that any such extension to infinite types would lead to a typing of $Y$ and hence a valid proof of the diagonalization lemma (which, taking Kunen's lead, we'll assume is sufficient to prove incompleteness). I'm not prepared to really make this claim without making some further assumptions on the formal system. I bet if we assume that the formation of terms is defined inductively (or co-inductively), and composition is found somewhere, then something could be shown.

$$ Y : \mu T . (T \to T) \to T. $$

And with parametric polymorphism (this may not be correct…):

$$ Y : \forall T . (T \to T) \to \forall T . (T \to T). $$

$$ Y = (\lambda f : T \to T) \big( (\lambda x: \mu A . A \to T). f (x x) \big) \big( (\lambda x: \mu A . A \to T). f (x x) \big) : (T \to T) \to T$$

Note that the $\mu$ types appear in the typing of the inner terms. In type systems that interpret $\forall$ such as with parametric polymorphism ($\lambda P$) or dependent types ($\lambda \omega$) $Y$ can get a type as well, but the important point of this is addressed later (see Lambda Cube for a discussion of these type systems).

Relating the type of the $Y$-combinator and Godel's claim

Recall the claim that:

The true source of the incompleteness, is to be found ... in the fact that the formation of ever higher types can be continued into the transfinite

In type theory, the formation of ever higher types would correspond to using a type constructor, i.e. in $\lambda^{\to}$ that would be '$\to$.' For example, given types $A$ and $B$, we form the type $A \to B$, written more obscurely as $\to(A, B)$. When dealing with types mathematically, especially when considering recursive types, it can be convenient to think of types as trees, as demonstrated by this figure from Pierce's book:

In this figure, the labels 1 and 2 are just labels to identify positions and arity, and Top is some given base type (typically a type inhabited by a single element, like $\{\cdot\}$ or x = x - that these types exist and are inhabited are some axioms of the system). The type on the right of the figure is in fact an infinite type, as is hinted by the ellipsis. In $\mu$ notation it would be written:

$$ \mu T . \mathrm{Top} \to T $$

This can be interpreted as an (extended) equation:

$$ T = \mathrm{Top} \to T = \mathrm{Top} \to (\mathrm{Top} \to T) = \mathrm{Top} \to (\mathrm{Top} \to (\mathrm{Top} \to T))$$

(Here we get the continued equation by substituting the definition of $T$ for $T$ over and over again.)

This same procedure of unfolding the type definition from $\mu$ can be repeated with the inner types of the $Y$-combinator, revealing that there is an infinite type. Recall the type of the parameter of the inner term of $Y$:

$$ \mu A . A \to T$$

This is nearly the same as the infinite type shown above, but instead of "extending to the right" it will "extend to the left."

Unfortunately, $\mu$ doesn't correspond so nicely to logic. In other type systems, in particular when we have parametric polymorphism or dependent types, we need to interpret the $\forall$ symbol. But this is where the infinite type is hidden in these systems. In the notes above, $\forall$ is interpreted as an (transfinite) product, while in other systems it is interpreted as a natural transformation (see Bartosz Milewski's discussion of natural transformations in Category Theory for Programmers). In either case, we get infinite types if there is an infinite number of types.

The idea here is that when we can interpret:

$$ \forall x \phi(x) = \phi(x_1) \land \phi(x_2) \land \phi(x_3) ... $$

Where $x_1, x_2$ is an enumeration of all members of the domain. Don't ask what if the members aren't enumerable?, it's not relevant.

To truly wrap up Godel's claim we would need to show that any such extension to infinite types would lead to a typing of $Y$ and hence a valid proof of the diagonalization lemma (which, taking Kunen's lead, we'll assume is sufficient to prove incompleteness). I'm not prepared to really make this claim without making some further assumptions on the formal system. I bet if we assume that the formation of terms is defined inductively (or co-inductively), and composition is found somewhere, then something could be shown.

added 598 characters in body

Source Link

edited Jun 4 at 22:37

Nathan Chappell

119
3

But what's the point?

What we gain from looking at this using the Curry-Howard correspondence, I suppose, is just another point of view -- another perspective. When the question is about the the true reason of the incompleteness of formal systems and questions about type systems come up, it seems reasonable to point out the correspondence. It's interesting to note that in computability theory, type theory, and logic, wherever the serious "problems" occur, you find the same diagonalization argument, which inevitably requires producing this $Y$.

Maybe $Y$ is the true reason.

Additional explanation, remove superflous narrative

Source Link

edited Jun 3 at 7:46

Nathan Chappell

119
3

We will require the interpretation of the Curry-Howard isomorphism, that is:

types are propositions

terms are proofs

See these notes for more information on the Curry-Howard.

Remember fromUsing the Curry-Howard isomorphism thatinterpretation, we interpret types as propositions, and an inhabitantcan consider the problem of type inhabitation: *given a type is$T$ and a context proof of the proposition, i.e.$\Gamma$, ifdoes there exists a term $t$ such that $t$ has type is inhabitable, the corresponding proposition is provable.$T$ in context $\Gamma$? The following is an important result: Type-inhabitability is PSPACE-Complete (and therefore decidable) in $\lambda^{\to}$. This would imply that every proposition corresponding to a type from $\lambda^{\to}$ would be either provable or disprovable. (I'm not a logician, I hope the relevance to incompleteness is clear).

Finally, hopefully, we can see the $Y$-combinator's manifestation in logic: it's this awful procedure, formalized as a propostion in

The type of $Y$ is the lemma above

The $Y$-combinator itself is proof of the above lemma

It makes sense: the additional explanationproof above is an algorithm of sorts. It takes as input a proposition in one free variable, and returns a sentence with a particular property. The existence of this algorithm, AKA the $Y$-combinator, is the basic result behind the Second Incompleteness Theorem and Tarski's theorem on undefinability of truth.

All of this seems like it needs to be abstracted away to let the mechanisms showcase themselves a bit more cleanly, and in the paper DIAGONAL ARGUMENTS AND CARTESIAN CLOSED CATEGORIES, Lawvere does this (he even includes a few hot takes…).

Here is a quick synopsis…

Basically he breaks down the problem into category theoretic terms, and demonstrates the main issue being the existence of a weakly point-surjective morphism leading to the ability to create a $Y$-combinator that forces fixed point properties on certain objects.

He goes on to weaken the hypotheses of Cartesian-Closedness to having finite products and a terminal object. The main demonstration here is that the ability to structure information need not be so strong: we can get away with projections and selection.

There Here is some rather technical material that I'm not smart enough to comment on extensively, but its basically continuing the development to arrive at some more elegant results (eleganta pretty diagram from the point of view of category theory).paper:

Finally the definition of truth and 1st incompleteness theorem are addressed. The important parts here are the construction of appropriate categories from theories and the idea of morphisms representing equivalence classes of (tuples of) formulas or terms of the theory, where two formulas (or terms) are considered equivalent iff their logical equivalence (or equality) is provable in the theory.$$\require{AMScd}\begin{CD} 1 @>a>> A \\ @V\langle a, c\rangle VV @VV\varphi V \\ A \times A @>>\operatorname{sat}> 2 \end{CD}$$

This construction is used to showcase a number of claims like satisfiability is not definable. This is the main result here, and the rest are building useful abstractions to capture the remaining notions.

The definition of $\operatorname{sat}$Another approach is to relate some formulataken in one free variable $\varphi: A \to 2$ to some constant: $c: 1 \to A$Introduction to Turing categories, and results in a pretty diagram:

$$\require{AMScd}\begin{CD} 1 @>a>> A \\ @V\langle a, c\rangle VV @VV\varphi V \\ A \times A @>>\operatorname{sat}> 2 \end{CD}$$

This diagram is related to the discussion ofwhere weakly point-surjective morphismsTuring Categories and leads toare a fixed-point combinator (if such $\operatorname{sat}$ exists.) Again, most of the rest uses this result and extends it to other notions.

The last major generalization occurs with the introduction of $\operatorname{substitute}: A \times A \to A$ and of the metamathematicalconvenient setting for the categorical study of abstract notions of computability. binary relations $\Gamma$, which satisfies:

For all $\varphi: A \to 2$ (formula in one free variable), there is a $c_\varphi: 1 \to A$ (a constant, i.e. the godel number), such that for all $a: 1 \to A$ (any "element" of $A$), we have Example diagram from paper:

$$ \operatorname{substitute}(c, a) \; \Gamma \; \varphi(a). $$

This is the abstraction of a lot of ugly work, and is meant to capture notions of provability and the like. It's actually quite impressive to see him capture the spirit with category theory so well. I've also read a bit about Turing Categories, but this paper I found to be the most satisfying thing I've read on the matter.$$ \begin{CD} A^n @>>> A \\ @V{p \times 1}VV @VV{f}V \\ A \times A^n @>>> A \end{CD} $$

From the point of view of trying to describe formal systems in a metamathematical manner, it may be worth considering these requirements.

See these notes for more information on the Curry-Howard

Remember from the Curry-Howard isomorphism that we interpret types as propositions, and an inhabitant of a type is a proof of the proposition, i.e., if a type is inhabitable, the corresponding proposition is provable. The following is an important result: Type-inhabitability is PSPACE-Complete (and therefore decidable) in $\lambda^{\to}$. This would imply that every proposition corresponding to a type from $\lambda^{\to}$ would be either provable or disprovable. (I'm not a logician, I hope the relevance to incompleteness is clear).

Finally, hopefully, we can see the $Y$-combinator's manifestation in logic: it's this awful procedure, formalized as a propostion in the additional explanation. It takes as input a proposition in one free variable, and returns a sentence with a particular property. The existence of this $Y$-combinator is the basic result behind the Second Incompleteness Theorem and Tarski's theorem on undefinability of truth.

All of this seems like it needs to be abstracted away to let the mechanisms showcase themselves a bit more cleanly, and in the paper DIAGONAL ARGUMENTS AND CARTESIAN CLOSED CATEGORIES, Lawvere does this (he even includes a few hot takes…).

Here is a quick synopsis…

Basically he breaks down the problem into category theoretic terms, and demonstrates the main issue being the existence of a weakly point-surjective morphism leading to the ability to create a $Y$-combinator that forces fixed point properties on certain objects.

He goes on to weaken the hypotheses of Cartesian-Closedness to having finite products and a terminal object. The main demonstration here is that the ability to structure information need not be so strong: we can get away with projections and selection.

There is some rather technical material that I'm not smart enough to comment on extensively, but its basically continuing the development to arrive at some more elegant results (elegant from the point of view of category theory).

Finally the definition of truth and 1st incompleteness theorem are addressed. The important parts here are the construction of appropriate categories from theories and the idea of morphisms representing equivalence classes of (tuples of) formulas or terms of the theory, where two formulas (or terms) are considered equivalent iff their logical equivalence (or equality) is provable in the theory.

This construction is used to showcase a number of claims like satisfiability is not definable. This is the main result here, and the rest are building useful abstractions to capture the remaining notions.

The definition of $\operatorname{sat}$ is to relate some formula in one free variable $\varphi: A \to 2$ to some constant $c: 1 \to A$, and results in a pretty diagram:

$$\require{AMScd}\begin{CD} 1 @>a>> A \\ @V\langle a, c\rangle VV @VV\varphi V \\ A \times A @>>\operatorname{sat}> 2 \end{CD}$$

This diagram is related to the discussion of weakly point-surjective morphisms and leads to a fixed-point combinator (if such $\operatorname{sat}$ exists.) Again, most of the rest uses this result and extends it to other notions.

The last major generalization occurs with the introduction of $\operatorname{substitute}: A \times A \to A$ and of the metamathematical binary relations $\Gamma$, which satisfies:

For all $\varphi: A \to 2$ (formula in one free variable), there is a $c_\varphi: 1 \to A$ (a constant, i.e. the godel number), such that for all $a: 1 \to A$ (any "element" of $A$), we have:

$$ \operatorname{substitute}(c, a) \; \Gamma \; \varphi(a). $$

This is the abstraction of a lot of ugly work, and is meant to capture notions of provability and the like. It's actually quite impressive to see him capture the spirit with category theory so well. I've also read a bit about Turing Categories, but this paper I found to be the most satisfying thing I've read on the matter.

From the point of view of trying to describe formal systems in a metamathematical manner, it may be worth considering these requirements.

We will require the interpretation of the Curry-Howard isomorphism, that is:

types are propositions

terms are proofs

See these notes for more information.

Using the interpretation, we can consider the problem of type inhabitation: *given a type $T$ and a context $\Gamma$, does there exists a term $t$ such that $t$ has type $T$ in context $\Gamma$? The following is an important result: Type-inhabitability is PSPACE-Complete (and therefore decidable) in $\lambda^{\to}$. This would imply that every proposition corresponding to a type from $\lambda^{\to}$ would be either provable or disprovable. (I'm not a logician, I hope the relevance to incompleteness is clear).

Finally, hopefully, we can see the $Y$-combinator's manifestation in logic:

The type of $Y$ is the lemma above

The $Y$-combinator itself is proof of the above lemma

It makes sense: the proof above is an algorithm of sorts. It takes as input a proposition in one free variable, and returns a sentence with a particular property. The existence of this algorithm, AKA the $Y$-combinator, is the basic result behind the Second Incompleteness Theorem and Tarski's theorem on undefinability of truth.

All of this seems like it needs to be abstracted away to let the mechanisms showcase themselves a bit more cleanly, and in the paper DIAGONAL ARGUMENTS AND CARTESIAN CLOSED CATEGORIES, Lawvere does this (he even includes a few hot takes…). Here is a pretty diagram from the paper:

$$\require{AMScd}\begin{CD} 1 @>a>> A \\ @V\langle a, c\rangle VV @VV\varphi V \\ A \times A @>>\operatorname{sat}> 2 \end{CD}$$

Another approach is taken in: Introduction to Turing categories, where Turing Categories are a convenient setting for the categorical study of abstract notions of computability. Example diagram from paper:

$$ \begin{CD} A^n @>>> A \\ @V{p \times 1}VV @VV{f}V \\ A \times A^n @>>> A \end{CD} $$