Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: Honoring Raymond Smullyan
Date: Wed, 8 Jan 2025 04:30:21 +0100
Organization: A noiseless patient Spider
Lines: 41
Message-ID: <vlkrge$2dkpc$1@dont-email.me>
References: <vlkfq7$1vh4j$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 08 Jan 2025 04:30:24 +0100 (CET)
Injection-Info: dont-email.me; posting-host="2a46dd651168680e2ad36d621d0ac75a";
	logging-data="2544428"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+am39jnqcuOiFu+jozlSc7kJ87go3xx0Y="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:cXMH4Sgcmo0kEXHj/pSGQD1cwNA=
In-Reply-To: <vlkfq7$1vh4j$1@solani.org>
Content-Language: en-GB
Bytes: 1978

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