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

Re: Relation Between Type Theory, Category Theory and Logic

#71

Post by mafribe » Sat, Jul 11, 2015, 11:27 PM UTC

solomatov wrote: post #58

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.

Homotopy type theory formalizes informal reasoning style when things which have "the same structure" are considered equal in a constructive type theory setting. Another achievement is formulation of synthetic homotopy type theory, i.e. axiomatic as opposed to based on geometric type theory.

I don't think synthetic homotopy type theory is known to cover all of conventional homotopy theory, so it's work in progress.

Re: Relation Between Type Theory, Category Theory and Logic

#72

Post by kazinator » Sun, Jul 12, 2015, 4:42 AM UTC

mafribe wrote: post #70

kazinator wrote: post #51

Earlier quoted context omitted.

A proof in mathematics is not purely syntactic because it's not purely logical. For instance, in some steps of a proof, we do something to both sides of an equation and argue that it is still balanced, based on rules that are outside of logic. Such a step can have a nonconstructive element.

A proof in mathematics is not purely syntactic because it's not purely logical. This is confusing constructive reasoning with the decision problem for proof validity. They are different things. The very point of logic, constructive or otherwise, or at least one of the key points for having a logic is to be able to decide whether a given proof object is indeed a valid proof. Valid proofs of course typically also make…

I seem to have the impression that constructivism in math is the same thing as constructive logic, though they are related.

Constructivism in mathematics:

https://en.wikipedia.org/wiki/Constructivism_%28mathematics%...

Constructive (intuitionistic) logic:

https://en.wikipedia.org/wiki/Intuitionistic_logic

Surely, one can be a constructivist mathematician, yet not eschew double negatives?

Re: Relation Between Type Theory, Category Theory and Logic

#73

Post by mafribe » Sun, Jul 12, 2015, 8:29 AM UTC

kazinator wrote: post #72

mafribe wrote: post #70

Earlier quoted context omitted.

A proof in mathematics is not purely syntactic because it's not purely logical. This is confusing constructive reasoning with the decision problem for proof validity. They are different things. The very point of logic, constructive or otherwise, or at least one of the key points for having a logic is to be able to decide whether a given proof object is indeed a valid proof. Valid proofs of course typically also make…

I seem to have the impression that constructivism in math is the same thing as constructive logic, though they are related. Constructivism in mathematics: https://en.wikipedia.org/wiki/Constructivism_%28mathematics%... Constructive (intuitionistic) logic: https://en.wikipedia.org/wiki/Intuitionistic_logic Surely, one can be a constructivist mathematician, yet not eschew double negatives?

No.

Classically, LEM and double negation are equivalent.

Intuitionistically the situation is more complicated, see the discussion in this thread by IngoBlechschmid: We can prove that LEM implies double negation, but not the other way around. Intuitionistically, we can only prove that ⊢¬¬A⊃A, then ⊢A∨¬A, but not ⊢(¬¬A⊃A)⊃(A∨¬A).

For these and related reasons, double negation is not considered constructivistically valid.

Re: Relation Between Type Theory, Category Theory and Logic

#74

Post by mafribe » Sun, Jul 12, 2015, 9:08 AM UTC

IngoBlechschmid wrote: post #20

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…

Your comment is a good first approximation to the motivation for HoTT! However, let me add a couple of remarks. Firstly, HoTT can also be used with classical logic, i.e. where you freely use the law of excluded middle. This does not impact the ability to check proofs with the computer in any way. Secondly, HoTT is the first foundation with which computer-formalized proofs of nontrivial theorems in a subject called "h…

Very nice descriptions.

While constructive reasoning is has many advantages, it has one disadvantage that is rarely pointed out, but sometimes causes real trouble.

Let's say we have a formula A which is classically and constructively true. It may be the case that constructive proofs of A are longer and more complicated than classical proofs of A. If you are working with an interactive proof assistant, this may be the difference between the proof automation being able to deal with A automatically or not.

This explosion in proof size is the reason why the (perfectly constructive) nominal techniques of Pitts et al have been implemented to a high standard in Isabelle/HOL are are used frequently, but are not really in Coq.

Re: Relation Between Type Theory, Category Theory and Logic

#75

Post by joe_the_user » Sun, Jul 12, 2015, 4:42 PM UTC

jonsterling wrote: post #68

joe_the_user wrote: post #10

Earlier quoted context omitted.

"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…

Bob is coming from the perspective of Brouwerian Intuitionism, and so he is not really that interested in a closed "formal system". So, "proofs" in the setting that Bob cares about are not derivations in a formal system, so Gödel's result doesn't really apply.

I'm pretty sure if you are talking about proofs having to do with a determined, computation system, Godel applies.

I mean, the unsolvability of the halting problem certainly applies and this gives a somewhat similar picture of the world.

Re: Relation Between Type Theory, Category Theory and Logic

#76

Post by doall » Sun, Jul 12, 2015, 8:52 PM UTC

Kutta wrote: post #65

gallabytes wrote: post #61

Earlier quoted context omitted.

A lot of work was going into the cubical model, but IIRC they realized it was a dead end about a month and a half ago. Right now the most promising work looks to be formalizing the set theoretic model in NuPRL.

Could you give pointers wrt cubical model being a dead end? As yet I've heard nothing about this.

See this https://groups.google.com/d/msg/homotopytypetheory/oXQe5u_Mm...

Re: Relation Between Type Theory, Category Theory and Logic

#77

Post by jonsterling » Tue, Jul 14, 2015, 7:07 PM UTC

joe_the_user wrote: post #75

jonsterling wrote: post #68

Earlier quoted context omitted.

Bob is coming from the perspective of Brouwerian Intuitionism, and so he is not really that interested in a closed "formal system". So, "proofs" in the setting that Bob cares about are not derivations in a formal system, so Gödel's result doesn't really apply.

I'm pretty sure if you are talking about proofs having to do with a determined, computation system, Godel applies. I mean, the unsolvability of the halting problem certainly applies and this gives a somewhat similar picture of the world.

In bob's setting, the computation system is not determined or fixed. It is open-ended...

In intuitionistic mathematics, we of course accept that there is no Turing computable halting oracle, but we do not rule out the possibility that there is some other effective oracle that can decide halting. (This is in contrast to recursive mathematics / Russian constructivism)