Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Relation Between Type Theory, Category Theory and Logic

ncatlab.org

Post reply on HN
Print view View original

41–50 of 77 posts

Re: Relation Between Type Theory, Category Theory and Logic

#41

Post by igravious »

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…

Yes, of course. I was coming dangerously close to conflating the fact of a sequence being uncountable with the proof that the sequence is uncountable being constructive. In other words, having no constructive method for generating the reals is not at all the same thing, of course, as having a proof that the reals are uncountable. In fact having a constructive proof that the reals are uncountable indicates to us that there is no constructive method for generating them! Oof. You have to so careful with this stuff :)

Re: Relation Between Type Theory, Category Theory and Logic

#42

Post by igravious »

IngoBlechschmid wrote: post #37
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.

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…

You melted my brain. What does “quantify over all formulas” mean?

From the way you state it, that's an interesting perspective. But it seems to be from a perspective of totality which I'm wary of. Not saying you're wrong, going to check out those links. Andrej Bauer was very kind to answer an out-of-the-blue email query of mine once :)

Seriously appreciative of your response, a thousand thanks!

EDIT: Ok, I've read your paper/slides. Very interesting. Don't you show that for specific constructions you can make LEM work for classical proofs with continuation monads? How does that show that _in general_ in constructive mathematics that the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) holds but not its inverse? Also, your bit about rewinding time makes complete sense imho because classical logic is atemporal and continuation monads inject the idea of flowing time into those proofs in a controlled manner.

EDIT 2: I _highly_ reccommend Dennis E. Hesseling's Gnomes in the Fog: The Reception of Brouwer's Intuitionism in the 1920s which I think gives a different slant on what Brouwer actually claimed than what you might imagine if you go with Andrej Bauer's interpretation. I can shoot you a copy if you can't lay your hands on it online :)

Re: Relation Between Type Theory, Category Theory and Logic

#43

Post by igravious »

IngoBlechschmid wrote: post #39
igravious wrote: post #33

Earlier quoted context omitted.

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.

Once those definitions are given then my trivial example holds though, correct?

Which are you saying; that it is, or, it is not possible to give those definitions?

Re: Relation Between Type Theory, Category Theory and Logic

#44

Post by igravious »

noreasonw wrote: post #38
igravious wrote: post #24

Earlier quoted context omitted.

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…

This is out of my depth but the work of the physicists David Bohm and Basil Hiley (an article with him was recently linked to HN) seems to point in this direction? See, for instance, http://www.amazon.com/The-Undivided-Universe-Ontological-Int...

But like I say, out of my depth! :)

Re: Relation Between Type Theory, Category Theory and Logic

#45

Post by tmvphil »

Kutta wrote: post #25
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.

Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll be a crazy nuclear weapon of generic programming and code generation. The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). For example, one Boolean type may be defined as an enum conta…

I must be missing something.

A proof that Bool and Bool2 are equal is a bijection f :: Bool -> Bool2. So given any g :: Bool -> Bool we have (f . g . f^-1) :: Bool2 -> Bool2. So it seems trivial.

Re: Relation Between Type Theory, Category Theory and Logic

#46

Post by IngoBlechschmid »

igravious wrote: post #43
IngoBlechschmid wrote: post #39

Earlier quoted context omitted.

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.

Once those definitions are given then my trivial example holds though, correct? Which are you saying; that it is, or, it is not possible to give those definitions?

I didn't check it. If you want to do it (the key step being to verify that the axioms of intuitionistic logic holds for your definitions of AND and OR), you can check Wikipedia for the list of axioms to verify: https://en.wikipedia.org/wiki/Heyting_algebra

Re: Relation Between Type Theory, Category Theory and Logic

#47

Post by IngoBlechschmid »

igravious wrote: post #42
IngoBlechschmid wrote: post #37

Earlier quoted context omitted.

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…

You melted my brain. What does “quantify over all formulas” mean? From the way you state it, that's an interesting perspective. But it seems to be from a perspective of totality which I'm wary of. Not saying you're wrong, going to check out those links. Andrej Bauer was very kind to answer an out-of-the-blue email query of mine once :) Seriously appreciative of your response, a thousand thanks! EDIT: Ok, I've read yo…

Sorry, didn't intend to use so much jargon. By "quantifying over all formulas" I just meant that one has to distinguish between the following two statements:

1. The law of excluded middle holds for a particular formula p.

2. The law of excluded middle holds for _all_ formulas p.

Also note that "formula" just means "formal logical statement", i.e. structured string consisting of v, ==>, and so on.

What do you mean by "perspective of totality"?

Regarding your first edit: There is indeed a metatheorem which says "any classical proof can be turned into a constructive proof". The catch is that this does _not_ apply to all formulas (of course, else the discussion would be moot), but only to formulas of a special kind. Not many formulas are of this kind, but for instance "There exist infinitely many prime numbers" and "A particular Turing machine halts" are (when suitably formulated). If you want to lookup the details, look for "Friedman's Trick".

That the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) holds is because there is a direct proof of this. I didn't show (here or in the slides) that the reverse implication is not intuitionistically valid. A simple way to do this would be to proceed along your lines, that is construct a Heyting algebra in which (¬¬p ⇔ p) holds for a particular element p but in which (~p v p) does not holds for this p. A fancier way would be to look at toposes arising "in nature", not specifically constructed for giving a counterexample.

Thanks for the book recommendation! I'll check it out. I won't have Internet over the weekend but I'd be glad to continue the discussion later.

Re: Relation Between Type Theory, Category Theory and Logic

#48

Post by kylebrown »

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.

In the comments of a recent mathematics-without-apologies blog post[1], there was a back-and-forth between Jacob Lurie and Urs Schreiber (the author of the OP article on nLab). I've been trying to parse the material on nLab for years, good to know I'm not the only one who seems to have trouble with it. A refreshingly blunt discussion, not to be missed!

1. https://mathematicswithoutapologies.wordpress.com/2015/05/13...

Re: Relation Between Type Theory, Category Theory and Logic

#49

Post by kazinator »

Kutta wrote: post #25
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.

Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll be a crazy nuclear weapon of generic programming and code generation. The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). For example, one Boolean type may be defined as an enum conta…

In C, you can convert back and forth between void * and some integer type, aliased as intptr_t since C99, so they must be equal under the univalence axiom.

Ah, "nuclear weapon" ... gotcha!

Re: Relation Between Type Theory, Category Theory and Logic

#50

Post by kazinator »

joe_the_user wrote: post #10
szany wrote: post #7

See also Bob Harper's blog for a more leisurely exposition: https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...

"Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!" The thing I never understood about statements of this sort is that in my understanding of model theory, Godel's theorem and so-forth, a proof is a rare thing. Most of the true statements in a given model don't have proofs. Any consistent proof…

Unfortunately, that isn't a world in which you could connect a USB camera to your laptop and just have it work after the system finds the right driver.
Post reply on HN