←back to thread

Baking the Y Combinator from Scratch

(the-nerve-blog.ghost.io)
123 points mprast | 1 comments | | HN request time: 0.234s | source
1. programjames ◴[] No.43638940[source]
I'm a constructivist, but I still believe in proof by contradiction. In fact, I don't think you can believe in proof by contradiction without constructivism. How do you know you can take an arbitrary proof P, and show it leads to a contradiction, if you don't even know you can touch P to begin with?

Anyway, how I would construct a proof by contradiction is:

1. Suppose you want to know if there exists a proof P of length less than N.

2. Do the usual "proof by contradiction" with a placeholder P.

3. You can write a very short algorithm that then plugs in all 2^N possible proofs into your proof by contradiction algorithm.

4. And voila! You have a constructive proof.