In a world where cranks use Curry-Howard to justify their ridiculous beliefs, it is refreshing to see not just a correct application, but a well-formed and aesthetically pleasing presentation. Thank you for not trying to obfuscate the material.
IMO Paul Tarau has some good stuff in this area, e.g.: "On a uniform representation of combinators, arithmetic, lambda terms and types", Paul Tarau <a href="https://dl.acm.org/doi/10.1145/2790449.2790526" rel="nofollow">https://dl.acm.org/doi/10.1145/2790449.2790526</a><p>Abstract:<p>> A uniform representation, as binary trees with empty leaves, is given to expressions built with Rosser's X-combinator, natural numbers, lambda terms and simple types. Type inference, normalization of combinator expressions and lambda terms in de Bruijn notation, ranking/unranking algorithms and tree-based natural numbers are described as a literate Prolog program.<p>> With sound unification and compact expression of combinatorial generation algorithms, logic programming is shown to conveniently host a declarative playground where interesting properties and behaviors emerge from the interaction of heterogenous but deeply connected computational objects.
> Yet, I believe it is fairly common to call this kind of logic intuitionistic logic, even though there is no rule for ⊥.<p>I don't believe this is very common—it's _an_ intuitionist logic, but "intuitionistic logic" by itself pretty much always includes ex falso—but actually it's rather strange that this is the case; it's not immediately clear that ex falso is constructive at all!<p>Minimal logic is both 'intuitionistic' (since LEM does not hold) and paraconsistent (since ex falso does not hold). I actually think there's a fairly solid case to say that only paraconsistent logics can be thought of as truly constructive; certainly if we start from BHK, it's not at all obvious that ex falso is a sound principle, and Kolmogorov himself had great issues accepting this. When he finally managed to convince himself of this in 1932 [1], it seems more that he was trying to finish off the logical framework by sidestepping the issue.<p>Kapsner [2] argues that the constructivist can only accept ex falso if she is willing to accept so called "empty promise constructions" as being constructive (see the source for more details on what this means, but it seems to broadly line up with Kolmogorov's justification); I personally don't think that they are compatible with the way BHK is usually presented at all.<p>Brouwer isn't around to tell us exactly what _he_ means by constructivism, so ultimately this is all philosophical, but I think this it's an interesting area that people don't really think aboutl I think a lot of people are exposed to intuitionistic logic via Martin-Lof type theories but don't actually consider how the logic fits into the wider notion of constructivism.<p>[1] : <a href="https://plato.stanford.edu/entries/intuitionistic-logic-development/#Kolm1932Heyt1934" rel="nofollow">https://plato.stanford.edu/entries/intuitionistic-logic-deve...</a><p>[2] : <a href="https://www.springer.com/gp/book/9783319052052" rel="nofollow">https://www.springer.com/gp/book/9783319052052</a>
During undergrad, I was only exposed to logic in my set theory and theory of computation classes. Any recommendations on good books/textbooks that are good for a relative beginners exploring set theory and type theory?
These are ideas are implemented in the theorem prover HOL light <a href="https://www.cl.cam.ac.uk/~jrh13/hol-light/" rel="nofollow">https://www.cl.cam.ac.uk/~jrh13/hol-light/</a><p>I find the discussion in of logic in <a href="https://sites.math.northwestern.edu/~richter/HolInformalMath.pdf" rel="nofollow">https://sites.math.northwestern.edu/~richter/HolInformalMath...</a> more concrete and more accessible.
I put a related question on Computer Science Stack Exchange a week ago. Linking it here in the hopes that HN users roll-calling here will shed some light.<p>Ref: <a href="https://cs.stackexchange.com/questions/122066/does-the-underlying-computational-calculus-in-type-theories-affect-decidability" rel="nofollow">https://cs.stackexchange.com/questions/122066/does-the-under...</a>