Re: Honoring Raymond Smullyan

On 08/01/2025 01:10, Mild Shock wrote:

Hi,
 Now you can listen to Bird songs for a minute:
 2016 Dana Scott gave a talk honoring Raymond Smullyan
https://www.youtube.com/watch?v=omz6SbUpFQ8

Define Smullyan.

A little quiz:
 Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
 A: Hardly, because xx has no simple type.
 Right?

Let `F : forall (X Y : Type), X -> Y`, then we can
(almost) write `F F`.  Simple seems simple, it just
doesn't end well:
```coq
(** There exists a function
     from any type to any type! *)
Axiom F : forall (X Y : Type), X -> Y.
(** Any two types: might be False False if
     that's all there is, an uninhabited type. *)
Parameters (T U : Type).
(** Now we can prove False. *)
Definition absurd : False :=
   F (T -> U) False (F T U).
```
-Julio