The key to understanding logic constructively goes through type theory, not philosophy.
I'll just leave this here https://78.media.tumblr.com/bfc158b432199a3e4f5de2ddc1bd7381...
I'll just leave this here https://78.media.tumblr.com/bfc158b432199a3e4f5de2ddc1bd7381...
You’re going to be very surprised when you look up the origins 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
Prelude Data.Function> :t fix id
fix id :: a
In a logically consistent functional language such as Lean https://leanprover.github.io, this definition is not allowed.
It's not only a syntax, it's a functional programming language which turns out to be a computational model for logic.
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.
inductive ℕ : Type
| zero : ℕ
| succ (n : ℕ) : ℕ
ℕ → ℕ
From then on one can start talking about different injective functions between those types and infer cardinality of which is bigger and so forth and so forth.
It's values, types and functions all the way down. Nothing from ZFC is lost, on the bright side, your proofs are checked by a computer. On an even brighter side, your proofs can be semi-automated, even brute forced.
Homotopy Type Theory: Univalent Foundations of Mathematics