Embed Notice

non-constructive logic just bugs me a lot.

why not have implications be an atomic thing?

implications can encode all the other operators (¬a is a → 0, a ∨ b is (a → c) → (b → c) → c for any c and a ∧ b is (a → b → c) → c for any c).

for a computer, implications are functions, and functions are atomic, they are just computation, and that's what computers do. so, by working like this, you make your proofs executable by a computer. this also means you can extract concrete witnesses from proofs of existence.

it also gives you an easier syntax to work with, because now you can write your formal proofs using a (typed) lambda calculus (like coq) as syntax instead of the abomination that sequence calculus is.

Instead, what classical logic has to do is encode an implication a → b as ¬a ∨ b.

working with this "desugared" version actually requires the law of the excluded middle, which is not constructive/computable.
trying to prove the desugared version in coq requires introducing an additional axiom (as seen in the attachment), which then prevents your proof from being executed as code.

with recursive functions, you can even get runnable inductive proofs - as long as the recursive function is proven to terminate.