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

The Holy Trinity: Logic, Languages, Categories (2011)

existentialtype.wordpress.com

Post reply on HN
Print view View original

41–50 of 51 posts

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#41

Post by cousin_it »

s-phi-nl wrote: post #40
cousin_it wrote: post #33

Unfortunately the most beautiful form of that analogy is the one that's crippled on both sides: computation (without Turing completeness) is equivalent to logic (without excluded middle). Add Turing completeness and you lose soundness. Add excluded middle and you lose confluence. Of course you can put epicycles on top of the simple idea and make it do anything you want, but as far as I know, no one has ever used the…

Could you point to a reference for the non-confluence of logic without excluded middle? It sounds interesting and a quick Google search did not find anything.

With excluded middle. This is the explanation that clicked for me: http://stackoverflow.com/questions/24711643/how-come-that-we...

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#42

Post by s-phi-nl »

cousin_it wrote: post #41
s-phi-nl wrote: post #40

Earlier quoted context omitted.

Could you point to a reference for the non-confluence of logic without excluded middle? It sounds interesting and a quick Google search did not find anything.

With excluded middle. This is the explanation that clicked for me: http://stackoverflow.com/questions/24711643/how-come-that-we...

Thanks! Yes, with excluded middle is what I meant.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#43

Post by dvt »

mafribe wrote: post #31
chriswarbo wrote: post #30

Earlier quoted context omitted.

> Curry-Howard is not known to apply to Java and C++. That's because the typing systems of these languages are no logics. For a start, in both languages, you can write non-terminating programs, hence any type is inhabited, which means inconsistency if you interpret types as truth-bearing propositions. Currently Curry-Howard mostly only works for strongly normalising, pure functional languages. As far as I'm aware, a…

unsound logic is still a logic Hmmm ... If your logic is unsound, anything can be proven. Soundness is a key requirement of any logic for this reason.

This is actually wrong.. There's an old joke in logic: sound, complete, consistent -- pick two :)

I think you're misunderstanding what soundness is. Soundness means that a proof in that logic implies a (semantic) entailment in that logic. That is:

  Γ ⊢ A ⇒ Γ ⊨ A
It's a very specific characteristic.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#44

Post by mafribe »

dvt wrote: post #43
mafribe wrote: post #31

Earlier quoted context omitted.

unsound logic is still a logic Hmmm ... If your logic is unsound, anything can be proven. Soundness is a key requirement of any logic for this reason.

This is actually wrong.. There's an old joke in logic: sound, complete, consistent -- pick two :) I think you're misunderstanding what soundness is. Soundness means that a proof in that logic implies a (semantic) entailment in that logic. That is: Γ ⊢ A ⇒ Γ ⊨ A It's a very specific characteristic.

Sorry, I mean inconsistent where I wrote sound.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#45

Post by mafribe »

dvt wrote: post #39
mafribe wrote: post #37

Earlier quoted context omitted.

Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.

Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination: Let α → H be a functional type where α is a Person type, and H is a boolean type. Γ ⊢ α → H Γ ⊢ α --------------------- (→e) Γ ⊢ H What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic ins…

It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#46

Post by dvt »

mafribe wrote: post #45
dvt wrote: post #39

Earlier quoted context omitted.

Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination: Let α → H be a functional type where α is a Person type, and H is a boolean type. Γ ⊢ α → H Γ ⊢ α --------------------- (→e) Γ ⊢ H What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic ins…

It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.

There are many paraconsistent logics out there[1]. There are also many "trivial" logics out there[1] (which exhibit the Principle of Explosion). The former are useful, the latter not so much.

All them of them are logics. Consistency is not a requirement; it's simply a property a system may or may not have.

[1] http://plato.stanford.edu/entries/logic-paraconsistent/

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#47

Post by jsprogrammer »

mafribe wrote: post #44
dvt wrote: post #43

Earlier quoted context omitted.

This is actually wrong.. There's an old joke in logic: sound, complete, consistent -- pick two :) I think you're misunderstanding what soundness is. Soundness means that a proof in that logic implies a (semantic) entailment in that logic. That is: Γ ⊢ A ⇒ Γ ⊨ A It's a very specific characteristic.

Sorry, I mean inconsistent where I wrote sound.

I'm still not sure it's true that an inconsistent logic can prove anything. Certainly an inconsistent logic contains contradictory proofs, but I don't think every inconsistent logic can be used to "prove" any arbitrary theorem.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#48

Post by danharaj »

AnimalMuppet wrote: post #38
danharaj wrote: post #21

Earlier quoted context omitted.

20th century mathematics takes first order classical logic and set theory as foundational. All other mathematics then becomes the analysis of sets via proofs in first order classical logic. The ugliness of this definition is that it is unnatural. Mathematicians don't always think in sets, they think directly about mathematical objects intuitively. No one cares which set encodes the number e , for example, but foundat…

> All other mathematics then becomes the analysis of sets via proofs in first order classical logic. That's like saying that home construction becomes an exercise in atomic physics. Yes, in some sense it's true, but it's so far removed from what's actually going on that it's completely uninteresting. Take the person working on differentiable manifolds. Do they care about that as problems in set theory? Not at all. Ch…

https://ncatlab.org/nlab/show/motivation+for+higher+differen...

Without category theory, certain generalizations of differential geometry would be virtually impossible to describe in any useful matter. These generalizations are extremely important for applications to physics and elucidate a lot of the fundamental structure of the classical theory. Furthermore, you get a much nicer theory when you consider higher geometric structures.

The power of category theory as foundations is that it lets you efficiently study the structure of a theory and how to modify that structure in principled ways.

Sure, the mathematician who is doing hard analysis probably does not care too much about category theory, but every mathematician being educated today knows at least a little category theory because it is the natural setting for certain key mathematical ideas, like cohomology.

In contrast, Set Theory is powerful but it doesn't organize mathematics the way logic/languagecategory theory does.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#49

Post by mafribe »

dvt wrote: post #46
mafribe wrote: post #45

Earlier quoted context omitted.

It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.

There are many paraconsistent logics out there[1]. There are also many "trivial" logics out there[1] (which exhibit the Principle of Explosion). The former are useful, the latter not so much. All them of them are logics. Consistency is not a requirement; it's simply a property a system may or may not have. [1] http://plato.stanford.edu/entries/logic-paraconsistent/

C++ and Java are not even paraconsistent: every type is inhabited.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#50

Post by chriswarbo »

dvt wrote: post #39
mafribe wrote: post #37

Earlier quoted context omitted.

Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.

Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination: Let α → H be a functional type where α is a Person type, and H is a boolean type. Γ ⊢ α → H Γ ⊢ α --------------------- (→e) Γ ⊢ H What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic ins…

Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules.

I was struggling to think of a concrete example less trivial than function application, but I suppose my difficulty just shows how terrible these systems are when viewed as logics (but they're still logics!)

Post reply on HN