Hacker News new | past | comments | ask | show | jobs | submit login
The death of Classical logic and the (re?)birth of Constructive Mathematics (philosophynow.org)
4 points by ukj on Feb 27, 2019 | hide | past | favorite | 1 comment



The law of identity is the cornerstone of Arostotelian/Classical logic. A = A is True.

In the 2nd half of the 20th century the American mathematician Haskell Curry and logician William Alvin Howard discovered an analogy between logical proofs and working computer programs. This is known as the Curry-Howard correspondence. Mathematical proofs are working computer programs. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Therefore, if we can write a working computer program which asserts that A = A is false without producing an error then we have living proof contradicting the founding axiom of Classic/Aristotelian logic.

I hereby reject the law of identity, and give you the law of humanity: A = A is False.

A thing needs not be the same as itself!

Version 1: https://repl.it/repls/SuperficialShimmeringAnimatronics

Turing-completeness/equivalence is the bar for "reason": λ-calculus ⇔ λ-calculus ⇔ λ-calculus ⇔ λ-calculus ⇔ λ-calculus ⊇ Type theory ⊇ Mathematics

I will spell this out in English: Turing-completeness guarantees GLOBAL consistency. Type theory allows for the containment of LOCALIZED contradictions thus preventing explosions. This is why intuitionistic logic is vastly superior to any "complete" logic that is NOT Turing-complete. Consistency paralyzes human thought! We are wildly inconsistent!

Being able to contain LOCAL inconsistencies actually allows for the GLOBAL system to become more and more consistent. This is completely and utterly counter-intuitive to most logicians!




Join us for AI Startup School this June 16-17 in San Francisco!

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: