Relation Between Type Theory, Category Theory and Logic • Hacker News Board

Re: Relation Between Type Theory, Category Theory and Logic

#31

Post by jules » Sat, Jul 11, 2015, 10:03 AM UTC

igravious wrote: post #29

mafribe wrote: post #18

Earlier quoted context omitted.

Rest assured that (contrary to j2kun's misleading claims) if some of the world's top mathematicians and computer scientists propose a new foundation of mathematics, they don't forget real numbers. You need to distinguish between non-computable and non-constructive. The proof that the cardinality of the reals is non-countable is perfectly constructive, see [1] for a discussion of these and related issues. [1] https://…

Eh? Your very own link says that there is debate within the mathematical community about whether Cantor's uncountability proof is constructive or not. I just realised that in my mind uncountable (not in a one-to-one correspondence with the natural numbers) means non-constructive. For me countability just says that we have a (constructive) method for generating a sequence of what would be all the terms in the sequence…

Even though there isn't a constructive method of generating uncountable sequences, that doesn't mean that this also assumed from within the logic. In conventional mathematics you can also only write down countably many sequences, but the space of all sequences is still uncountable. We don't assume that the set of all sequences is the set of sequences which we can actually define. Similarly in constructive mathematics we don't say that ALL sequences are generated by some computer program, just that YOU are only allowed to generate sequences in that way.

So this doesn't contradict in any way that Cantor's proof is constructive (which contrary to that wikipedia article, it most definitely is).

Re: Relation Between Type Theory, Category Theory and Logic

#32

Post by YorkshireSeason » Sat, Jul 11, 2015, 10:04 AM UTC

jules wrote: post #27

Xcelerate wrote: post #8

Can someone give me an absolute layman explanation to homotopy type theory (and why it's so interesting)? I'm hearing about it everywhere, but most of the introductions to the subject assume the reader is already familiar with either type theory or category theory.

First the type theory part of homotopy type theory. Mathematicians have been doing logic for a long time, but mathematical statements and proofs were not themselves mathematical objects. They were just human language text with some math notation thrown in. Around 1900 Brouwer, Heyting and Komolgorov came up with a cool idea: treat proofs as first class mathematical objects. Then giving a proof is equivalent to constr…

It is wrong to say that it's key novelty is that "Homotopy type theory: extends type theory with proofs of equality in a proper way". This was done already with Martin Lof's type theory, as used in e.g. Agda. Homotopy type theory adds univalence!

Re: Relation Between Type Theory, Category Theory and Logic

#33

Post by igravious » Sat, Jul 11, 2015, 10:08 AM UTC

igravious wrote: post #26

j2kun wrote: post #13

Earlier quoted context omitted.

I'll try to keep it short and skip the details of the mathematical framework itself. Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not…

Careful! Here is LEM: ⊢. ~p ∨ p (one of either p or p's inverse must be true -- and thus the other false -- with no third (truth) value allowed), hence also called principle of bivalence. What you wrote is the principle of double negation. In general: (~p ∨ p) ⇒ (¬¬p ⇔ p) but not the other way around if I not mistaken? Please correct me if I am wrong.

In other words, what you wrote is that every value when negated twice returns to itself. Here's a truth table of 3 values for the negation operator

     v | 0 | 1 | 2
    --------------
    ¬v | 1 | 0 | 2

So ¬¬0 ⇔ 0 and ¬¬1 ⇔ 1 and ¬¬2 ⇔ 2 which satisfies the principle of double negation but not LEM. Correct?

Re: Relation Between Type Theory, Category Theory and Logic

#34

Post by jules » Sat, Jul 11, 2015, 10:16 AM UTC

YorkshireSeason wrote: post #32

jules wrote: post #27

Earlier quoted context omitted.

First the type theory part of homotopy type theory. Mathematicians have been doing logic for a long time, but mathematical statements and proofs were not themselves mathematical objects. They were just human language text with some math notation thrown in. Around 1900 Brouwer, Heyting and Komolgorov came up with a cool idea: treat proofs as first class mathematical objects. Then giving a proof is equivalent to constr…

It is wrong to say that it's key novelty is that "Homotopy type theory: extends type theory with proofs of equality in a proper way". This was done already with Martin Lof's type theory, as used in e.g. Agda. Homotopy type theory adds univalence!

I wouldn't call that a proper treatment of equality. It is unsatisfactory in several ways: no proper equality on functions (function extensionality), no proper equality on types (univalence), no quotient types (~= HITs), and since refl is the only proof of equality it doesn't even make much sense to talk about equality on equalities. More fundamentally the idea that refl is the only proof of equality just doesn't sit well in the philosophy of type theory. The whole idea of type theory is that things can have more than one proof and are not 'just true' as in conventional mathematics.

Re: Relation Between Type Theory, Category Theory and Logic

#35

Post by YorkshireSeason » Sat, Jul 11, 2015, 10:16 AM UTC

jules wrote: post #31

igravious wrote: post #29

Earlier quoted context omitted.

Eh? Your very own link says that there is debate within the mathematical community about whether Cantor's uncountability proof is constructive or not. I just realised that in my mind uncountable (not in a one-to-one correspondence with the natural numbers) means non-constructive. For me countability just says that we have a (constructive) method for generating a sequence of what would be all the terms in the sequence…

Even though there isn't a constructive method of generating uncountable sequences, that doesn't mean that this also assumed from within the logic. In conventional mathematics you can also only write down countably many sequences, but the space of all sequences is still uncountable. We don't assume that the set of all sequences is the set of sequences which we can actually define. Similarly in constructive mathematics…

Exactly. Here is an implementation of Cantor's diagonal method in Agda which is entirely constructive: http://www.playingwithpointers.com/agda-cantor.html

Re: Relation Between Type Theory, Category Theory and Logic

#36

Post by YorkshireSeason » Sat, Jul 11, 2015, 10:43 AM UTC

jules wrote: post #34

YorkshireSeason wrote: post #32

Earlier quoted context omitted.

It is wrong to say that it's key novelty is that "Homotopy type theory: extends type theory with proofs of equality in a proper way". This was done already with Martin Lof's type theory, as used in e.g. Agda. Homotopy type theory adds univalence!

I wouldn't call that a proper treatment of equality. It is unsatisfactory in several ways: no proper equality on functions (function extensionality), no proper equality on types (univalence), no quotient types (~= HITs), and since refl is the only proof of equality it doesn't even make much sense to talk about equality on equalities. More fundamentally the idea that refl is the only proof of equality just doesn't sit…

This discussion goes way beyond an "absolute layman explanation to homotopy type theory" ...

Anyway, I disagree that the "whole idea of type theory is that things can have more than one proof". UIP is about identity types and their proofs. Identity types are very special types. It is far from obvious that they should be inhabited by more than one proof. Indeed, it was a surprising breakthrough when Streicher/Hoffmann discovered that UIP does not hold in general and new axioms like Streicher's K or Univalence needed to be formulated to deal with this question.

Re: Relation Between Type Theory, Category Theory and Logic

#37

Post by IngoBlechschmid » Sat, Jul 11, 2015, 10:51 AM UTC

igravious wrote: post #26

j2kun wrote: post #13

Earlier quoted context omitted.

I'll try to keep it short and skip the details of the mathematical framework itself. Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not…

Careful! Here is LEM: ⊢. ~p ∨ p (one of either p or p's inverse must be true -- and thus the other false -- with no third (truth) value allowed), hence also called principle of bivalence. What you wrote is the principle of double negation. In general: (~p ∨ p) ⇒ (¬¬p ⇔ p) but not the other way around if I not mistaken? Please correct me if I am wrong.

You are right that for a particular formula p, the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) is an intuitionistic tautology and that the reverse implication is not (in general).

However the situation is different when you quantify over all formulas. If you have (¬¬p ⇔ p) for _any_ formula p, you also have (~q ∨ q) for any formula q (written with a different letter to not get lost in variable capturing issues).

This is because, for any formula q, we have the intuitionistic tautology ~~(~q v q). (Proving this is a fun exercise. If you get stuck, see page 26 of https://github.com/iblech/talk-constructive-mathematics/raw/... or elsewhere on the Internet.) So, if you assume the principle of double negation for all formulas, then in particular you assume that, for any formula q, the implication ~~(~q v q) ⇒ (~q v q) holds. Since the antecedent is unconditionally valid, the consequent is as well. Thus you have the law of excluded middle for q.

I highly recommend Andrej Bauer's blog for such matters. The post http://math.andrej.com/2008/08/13/intuitionistic-mathematics... is a good starting point.

Re: Relation Between Type Theory, Category Theory and Logic

#38

Post by noreasonw » Sat, Jul 11, 2015, 11:06 AM UTC

igravious wrote: post #24

igravious wrote: post #23

Earlier quoted context omitted.

Wonderfully accessible synopsis. One ever so _minor_ point. Did you really mean to say "The former and the latter are not the same thing" or "The former and the latter are not _formally_ the same thing" ??? Here's a fun fact for you, you might enjoy this. I picked up a copy of a 1943, second edition, hardback copy of Bertrand Russell's An Inquiry into Meaning and Truth . (In an antiquarian bookstore for €25, as one d…

Wow. Replying to myself. What is brought into question is the status of Proof by Contradiction, not the status of the Law of Noncontradiction. Russell seems to have confused these two things. And I don't blame him. It was 1940 after all, and there was a war on. Another interesting fact. The book is built up from from accumulated material finally delivered over a course of lectures at Harvard University in a series ca…

Just reading your comment I was thinking about the closed world assumption in logic (prolog), perhaps there are some middle concept between the Proof by Contradiction and the closed world assumption. In the real world we learn concepts (think about relativity or a non planar world) and then the old question is no longer a two value alternative.

Perhaps something like: In this field a new conception could appear that would invalidate what we consider today to be only two alternatives. Is not about many worlds reality or quantum computation, (3 minutes thinking time out).

Re: Relation Between Type Theory, Category Theory and Logic

#39

Post by IngoBlechschmid » Sat, Jul 11, 2015, 11:07 AM UTC

igravious wrote: post #33

igravious wrote: post #26

Earlier quoted context omitted.

Careful! Here is LEM: ⊢. ~p ∨ p (one of either p or p's inverse must be true -- and thus the other false -- with no third (truth) value allowed), hence also called principle of bivalence. What you wrote is the principle of double negation. In general: (~p ∨ p) ⇒ (¬¬p ⇔ p) but not the other way around if I not mistaken? Please correct me if I am wrong.

In other words, what you wrote is that every value when negated twice returns to itself. Here's a truth table of 3 values for the negation operator v | 0 | 1 | 2 -------------- ¬v | 1 | 0 | 2 So ¬¬0 ⇔ 0 and ¬¬1 ⇔ 1 and ¬¬2 ⇔ 2 which satisfies the principle of double negation but not LEM. Correct?

Your counterexample could work, but it is not obvious that it does so. This is because you also have to give definitions of ∧, v, and ==>, and then check that your definitions satisfy the axioms of intuitionistic logic.

As stated, your example only shows that one can define a function f on a set which contains more than two elements such that f . f = id. But this by itself is a trivial statement.

Re: Relation Between Type Theory, Category Theory and Logic

#40

Post by leoc » Sat, Jul 11, 2015, 11:10 AM UTC

igravious wrote: post #26

j2kun wrote: post #13

Earlier quoted context omitted.

I'll try to keep it short and skip the details of the mathematical framework itself. Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not…

Careful! Here is LEM: ⊢. ~p ∨ p (one of either p or p's inverse must be true -- and thus the other false -- with no third (truth) value allowed), hence also called principle of bivalence. What you wrote is the principle of double negation. In general: (~p ∨ p) ⇒ (¬¬p ⇔ p) but not the other way around if I not mistaken? Please correct me if I am wrong.

Careful: https://en.wikipedia.org/wiki/Principle_of_bivalence#Relatio...