Logic:Favorite

From Tractatus

My favorite proof from Type Theory is the Extensibility of the Axiom of Infinity, i.e that if a set is infinite, then the power set of that set is infinite. I use the word set here instead of type, because if you are not familiar with type theory, it will make sense, and if you are, you can translate.

The definition of an infinite set is a set such that there exists a relation on that set which has no maximum, is irreflexive, and transitive. This is $I n f i n α$ :

$\exists r_{o\alpha\alpha} \forall x_\alpha \forall y_\alpha \forall z_\alpha [ \exists w_\alpha rxw \and \sim rxx \and .\ rxy \supset .\ ryz \supset rxz]$

Basically, to understand why this means a type(set) is infinite, think about the $< o σσ$ relation( $σ$ means 'number' in type theory):

$\forall x_\sigma \forall y_\sigma \forall z_\sigma [ \exists w_\sigma x < w \and x \not< x \and .\ x < y \supset .\ y < z \supset x < z]$

In English: if you give me a number $x$ , then there is number $w$ greater than $x$ ('no maximum'), $x$ is not greater than itself('irreflexive'), and if $x < y$ and $y < z$ then $x < z$ ('transitive'). That is what it means for something to be infinite.

1 What we want to prove
2 The Outline of the Proof
3 The Proof
- 3.1 The trick

What we want to prove

We want to show that this definition of infinity extends, which is to say that if we start with an infinite type, then collections of things with that type are infinite.

This is actually one of the fundamental concepts of Cardinality(Size). Most people first encounter this, when the come upon Cantor's Theorem, which states that Numbers(1,2,3,4,5...) and Real Numbers (.1, .3, .77758, .000032, 3.1415..., ...) don't have the same size. For the non-mathematicians out there, Cantor's Theorem is one of those wierd things you learn which changes your view of the universe. It demonstrates that at some fundamental level you don't understand the concept of size. Yeah, size.

The difference is that we are working with objects, types, unlike any you have ever dealt with. You don't know anything about them except the following five axioms:

[list axioms of type theory. Technically schema, but who knows the difference?]

What we need to prove is that:

$\vdash_{\mathcal{Q}_0} Infin_\alpha \supset Infin_{o\alpha}$

(The funny turnstile means that we want to prove that it is a tautology, that it requires _nothing_ to be True. The $\mathcal{Q}_0$ refers to our axioms, because we will use them).

The Outline of the Proof

$I n f i n α$ states that there is a relation with a bunch of properties. $I n f i n o α$ states that there is a relation with a bunch of properties.

What we need to do is given such a relation $r α$ for $α$ with those properties construct a relation $r o α$ with the same properties over $o α$ .

The normal way to do this for a set is to for a given set is to take the supremum('the least element of the integers which is greater than all the elements of the set') of each set, and then use the relation on the elements to inflict a relation on the sets. The reader with some mathematical experience should spend some time (a day or two) thinking about how to construct such a relation. It is harder than you might think.

The Proof

I stuggled for a week and then, it occurred to me that the answer lay in how to map from a type $o α$ to a type $α$ . $\vdash_{\mathcal{Q}_0} \exists r_{o\alpha\alpha} \forall x_\alpha \forall y_\alpha \forall z_\alpha [ \exists w_\alpha rxw \and \sim rxx \and .\ rxy \supset .\ ryz \supset rxz]$

....

$\vdash_{\mathcal{Q}_0} \exists r_{o(o\alpha)(o\alpha)} \forall x_{o\alpha} \forall y_{o\alpha} \forall z_{o\alpha} [ \exists w_{o\alpha} rxw \and \sim rxx \and .\ rxy \supset .\ ryz \supset rxz]$

The trick

TODO

The trick is to realize that the relation established on $α$ does not need to be similar in any way to the relation established for $o α$ .

The ... axiom provides you with the answer. For singleton types, the $ι$ operator maps an object of type $o α$ to the single member of type $α$ . This is not a choice function because there is no guarantee that if there is more than one member a member will be returned. But... the beatiful thing is that we don't care. As long as every member of $o α$ is mapped to some (arbitrary) member of $α$ , we can satisfy the requirements of the Axiom of Infinity.

Our new relation is the composition $[λ a o α .λ b o α r o αα (ι a)(ι b)]$

Retrieved from "http://www.tractat.us/wiki/Logic:Favorite"

This page has been accessed 1,891 times. This page was last modified on 14 March 2011, at 06:07. Content is available under Attribution-Noncommercial-Share Alike 2.5 .

Tractat.us	Iain \| About \| Help \| FAQ \| Special pages \| Log in
n. handling , management, treatment.	Printable version \| Disclaimers \| Privacy policy

Logic:Favorite

Contents

What we want to prove

The Outline of the Proof

The Proof

The trick

Find

Browse

Edit

This page

Context

My pages

Special pages