If you only want to go partway to catuskoti, consider the intuitionistic logic of Heyting and Brouwer. This is the actual form of logic which has the Curry-Howa

If you only want to go partway to catuskoti, consider the intuitionistic logic of Heyting and Brouwer. This is the actual form of logic which has the Curry-Howard isomorphism with lambda calculus. In particular, it rejects PEM but not PNC. What does this world feel like? Well, let's assume we've formulated a proposition. In type theory syntax we'd write the body of the proposition `B` and give it a name `p` like so p : B Here p is just a symbolic name and B is some formal language expression which describes the proposition p. It's important to note that while we've immediately written this proposition but we've not established whether it is true or false. PEM would imply that the state we are in currently is unstable—p must be either true or false already! Intuititionistic Logic, however, admits that the state of almost all propositions is far closer to what p is now—neither proven nor refuted. This neither-true-nor-false state is natural and only through a process of communication and work can we move forward. For instance, we could construct a proof of p p : B p = proof1 -- note how this looks like a typed program now or we could construct a proof of its refutation notp : not B notp = proof2 But we might be incapable of either. It is unclear whether a program searching through the space of possible proofs would ever terminate, one might note. What's immediately nice about this system is that it can model internally the notion of an independent statement—all statements are assumed independent until proven otherwise even! It also reflects the nature of (functional) programming (of a certain style) where we define the type we're hoping to achieve and then work to create a program satisfying that type. Note finally that Intutionistic Logic still holds that PNC is true. In particular, we can trivially prove the following proposition notPNC : forall prop . not (prop AND not prop) notPNC = /\_ -> \(p, np) -> np p -- this is a legitimate proof term written in (System F) lambda calculus