4 ms·

The key to understanding logic constructively goes through type theory, not philosophy. I'll just leave this here https://78.media.tumblr.com/bfc158b432199a3e4

• arto 8y ago
  Source, pretty please?
  • shawn 8y ago
    https://books.google.com/books?id=LkDUKMv3yp0C&pg=PA11&lpg=PA11&dq=%22We+summarize+the+different+points+of+view+of+the+type-theoretic+operations+in+Table+1.%22&source=bl&ots=au08DGQydm&sig=v9DrnObM_x9ygzdCCNMsk0VZ63Y&hl=en&sa=X&ved=2ahUKEwjRkuPW6L_bAhVU_oMKHfSvC7EQ6AEwAHoECAEQKg#v=onepage&q=%22We%20summarize%20the%20different%20points%20of%20view%20of%20the%20type-theoretic%20operations%20in%20Table%201.%22&f=false https://books.google.com/books?id=LkDUKMv3yp0C&pg=PA11&lpg=P... Homotopy Type Theory: Univalent Foundations of Mathematics
    • arto 8y ago
      Thanks!
  • hiker 8y ago
    It's from https://hott.github.io/book/nightly/hott-online-1174-g29279f5.pdf#page=23 https://hott.github.io/book/nightly/hott-online-1174-g29279f...
    • arto 8y ago
      Thanks!
• curuinor 8y ago
  The progenitor of types was Russell, who considered himself a philosopher.
• Sangermaine 8y ago
  >goes through type theory, not philosophy. You’re going to be very surprised when you look up the origins of type theory.
  • hiker 8y ago
    https://en.wikipedia.org/wiki/History_of_type_theory https://en.wikipedia.org/wiki/History_of_type_theory Not that much surprised. History of type theory is a history of trying to define precisely computation. That is, try to allow recursion but enforce that all programs terminate. The solution to this problem these days is to use a purely functional programming language with dependent types (e.g. Homotopy Type Theory, Lean). Haskell, for example, being a practical functional programming language, is logically inconsistent. Using the fix function: fix :: (a -> a) -> a fix f = let x = f x in x one can produce proof of everything Prelude Data.Function> :t fix id fix id :: a that is just an infinite loop. In a logically consistent functional language such as Lean https://leanprover.github.io https://leanprover.github.io, this definition is not allowed.
• mbid 8y ago
  So you think the key for understanding constructive logic is to understand some peculiar syntax for a fragment of it. Ridiculous, but sadly quite typical among type theory cultists.
  • hiker 8y ago
    > So you think the key for understanding constructive logic is to understand some peculiar syntax. It's not only a syntax, it's a functional programming language which turns out to be a computational model for logic.
    • teilo 8y ago
      No one is saying type theory is useless, particularly when it comes to computation. It works within its own boundaries, but it does indeed have boundaries. There is a reason the ZFC has triumphed in mathematics.
      • hiker 8y ago
        Not really. The boundaries of type theory (say HoTT) are exactly what is possible on a Turing machine (computable). And a step beyond those throws ZFC itself into paradoxes (say Russel's). Moreover ZFC is directly expressible in type theory https://hott.github.io/book/nightly/hott-online-1174-g29279f5.pdf#page=353 https://hott.github.io/book/nightly/hott-online-1174-g29279f...
        • teilo 8y ago
          I agree regarding the completeness of type theory in regards to Turing computability. But I disagree regarding paradoxes in ZFC. Russel's paradox specifically applies to naive (simple Cantor) set theory, something the ZFC was explicitly designed to address with its axioms of choice and infinity. Furthermore the HoTT is itself expressible in the common extension of ZFC which adds at least one inaccessible cardinal. And, mathematically speaking, the ZFC excels in dealing with infinities, which is more difficult (though possible) in the various type theories.
• teilo 8y ago
  Anyone who prefers type theory to (non-naive) set theory does so for philosophical reasons. Therefore your argument is self-defeating.