Anyone interested in this might get a kick out of the book “To Mock A Mockingbird”.

The first half of the book is an almost exhaustive exploration of self-referential riddles. Like “if the barber shaves everyone who doesn’t shave themselves, who shaves the barber?” and “if one gremlin always tells the truth and the other always lies, how can you ask them for directions?”

The second half of the book is a rigorous examination of combinatorial logic through an analogy of birds who make calls depending on the calls of other birds they hear. It touches on function composition,recursion, fixed points, godels theorems, and the Y combinator (the mockingbird).

My only gripe with the book is that it stays completely within the bird metaphor, and doesn’t always explicitly state the underlying math concept.

If anyone wants this in a humorous 1 hour format, watch the legendary Jim Weirich (rip) explain it here: https://www.youtube.com/watch?v=FITJMJjASUs

Don't be discouraged that it is in Ruby as the concepts are completely general. Great watch even though I never coded a line of Ruby.

Is there a technique to remember this? I will understand it today and forget after a few weeks.

Here's a write-up I did on deriving the Y combinator from Lawvere's fixed-point theorem: https://emarzion.github.io/Y-Comb/

From scratch it's also easy dress up a quoted Y combinator as in Löb's theorem. Start with the usual Y combinator

  Y = \f. (\x.f(x x)) (\x.f(x x))
    : (p -> p) -> p

Now Löb's theorem states that []([]p -> p) -> []p, which can be read, "if you have the source code to transform (the source code of a thing of type p) to a thing of type p, then you can produce the source code for a thing of type p". Let's embellish Y using {} to denote the quoting comonad.

  Y' = \{f}. (\{x}.{f{x{x}}}) {\{x}.{f{x{x}}}}
     : []([]p -> p) -> []p

> you technically can't do name = term

But you can do

    let name = term in term2

    ((λname. term2) term)

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.

At first I thought they were going to implement it in MIT Scratch.

[flagged]

[flagged]

[flagged]