Maybe you know most of the below, I'll just state it for completeness.
Curry-Howard isomorphism establishes a correspondence between types and propositions, and proofs and programs.
That is, a proposition is true, if there is a program of the corresponding type. This means a type is inhabited.
A false is represented by a type postulated to be uninhabited, ⊥. (Notice "postulated" - this is the type whose emptiness does not require a proof)
A negation is represented as implication of false. You will recall this from the definition of implication.
That is, a proposition "not A" is a type A→⊥. You can easily see that for inhabited types A type A→⊥ is uninhabited, and for uninhabited types A type A→⊥ is inhabited. What is the latter one inhabited with? A function that establishes isomorphism of types A and ⊥ (or you could think of id⊥ in the skeleton category).
Then to see the former case, that A→⊥ is uninhabited for an inhabited type A, consider idA→⊥: (A→⊥)→(A→⊥). Given a witness of type A (given a proof that A is inhabited), (flip id) can produce a proof that (A→⊥) is isomorphic to ⊥ - i.e. A→((A→⊥)⊥). This is only one side of isomorphism.
The other part of isomorphism is always there: it is postulated that there is an arrow from uninhabited type ⊥ to every other type such that any diagrams with it commute. You can see this as the existence of ⊥→A - existence without a proof (because it is postulated). You can also see this as the part of implication where "everything follows from false premise - both false (id) and true".
The "any diagrams with it commute" means that ⊥→A≡B→A for any B, if B→A factors through ⊥ - that is, if at some point you are able to compute an "instance" of ⊥.
Now we can show that (B→⊥)→⊥≡B for B=A→⊥. You can see that this can be rewritten as ((A→⊥)→⊥)→⊥≡A→⊥, which is none other than a proof of extensional equality of two functions.
Extensional equality of functions f and g of type A→B is: given any value of type A they should produce equal values of type B. That is a proposition of type (a:A)→(f a≡g a). If this proposition is inhabited for given f and g, then we call type f≡g inhabited (equality of functions proven).
The proof is trivial:
flatten-triple : {A : Set} ((((A→⊥)→⊥)→⊥)) → (A→⊥) flatten-triple f a = f (flip id a)
bool : {A : Set} (g : A→⊥) → flatten-triple (flip id g) ≡ g bool g = ext λ a → ⊥-elim (g a) -- remember the function from ⊥ to any type? Here is the arrow to the type flatten-triple (flip id g) a ≡ g a
Then we use extentionality axiom to prove double negation of g and g are equal. Since we can do this for any witness g, we conclude the types are isomorphic: composition of (flip id) and flatten-triple is id; you can similarly show the opposite, too; two types have arrows whose composition is respective id - isomorphism established, and the types are proven equivalent (and equal, if we have univalence axiom).
If double negation of A is equal to A, the logic is boolean. So the whole negative segment of intuitionistic logic is boolean. (That is, the segment of types that are of the form A→⊥)
You can see why this is so. Remember that all types of the form A→⊥ are either empty (contain no functions; the type is isomorphic to ⊥) or contain one function, id (the type is isomorphic to T). This observation makes the negative segment so boring: it's all just ones or zeros!
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2020-05-14 07:08 am (UTC)Curry-Howard isomorphism establishes a correspondence between types and propositions, and proofs and programs.
That is, a proposition is true, if there is a program of the corresponding type. This means a type is inhabited.
A false is represented by a type postulated to be uninhabited, ⊥. (Notice "postulated" - this is the type whose emptiness does not require a proof)
A negation is represented as implication of false. You will recall this from the definition of implication.
That is, a proposition "not A" is a type A→⊥. You can easily see that for inhabited types A type A→⊥ is uninhabited, and for uninhabited types A type A→⊥ is inhabited. What is the latter one inhabited with? A function that establishes isomorphism of types A and ⊥ (or you could think of id⊥ in the skeleton category).
Then to see the former case, that A→⊥ is uninhabited for an inhabited type A, consider idA→⊥: (A→⊥)→(A→⊥). Given a witness of type A (given a proof that A is inhabited), (flip id) can produce a proof that (A→⊥) is isomorphic to ⊥ - i.e. A→((A→⊥)⊥). This is only one side of isomorphism.
The other part of isomorphism is always there: it is postulated that there is an arrow from uninhabited type ⊥ to every other type such that any diagrams with it commute. You can see this as the existence of ⊥→A - existence without a proof (because it is postulated). You can also see this as the part of implication where "everything follows from false premise - both false (id) and true".
The "any diagrams with it commute" means that ⊥→A≡B→A for any B, if B→A factors through ⊥ - that is, if at some point you are able to compute an "instance" of ⊥.
Now we can show that (B→⊥)→⊥≡B for B=A→⊥. You can see that this can be rewritten as ((A→⊥)→⊥)→⊥≡A→⊥, which is none other than a proof of extensional equality of two functions.
Extensional equality of functions f and g of type A→B is: given any value of type A they should produce equal values of type B. That is a proposition of type (a:A)→(f a≡g a). If this proposition is inhabited for given f and g, then we call type f≡g inhabited (equality of functions proven).
The proof is trivial:
flatten-triple : {A : Set} ((((A→⊥)→⊥)→⊥)) → (A→⊥)
flatten-triple f a = f (flip id a)
bool : {A : Set} (g : A→⊥) → flatten-triple (flip id g) ≡ g
bool g = ext λ a → ⊥-elim (g a) -- remember the function from ⊥ to any type? Here is the arrow to the type flatten-triple (flip id g) a ≡ g a
Then we use extentionality axiom to prove double negation of g and g are equal. Since we can do this for any witness g, we conclude the types are isomorphic: composition of (flip id) and flatten-triple is id; you can similarly show the opposite, too; two types have arrows whose composition is respective id - isomorphism established, and the types are proven equivalent (and equal, if we have univalence axiom).
If double negation of A is equal to A, the logic is boolean. So the whole negative segment of intuitionistic logic is boolean. (That is, the segment of types that are of the form A→⊥)
You can see why this is so. Remember that all types of the form A→⊥ are either empty (contain no functions; the type is isomorphic to ⊥) or contain one function, id (the type is isomorphic to T). This observation makes the negative segment so boring: it's all just ones or zeros!