Re: Honoring Raymond Smullyan

Hi,
Thats System F and not simple types. also
known as the polymorphic lambda-calculus
or second-order lambda-calculus, it is an
extension of simply typed lambda-calculus.
But in simple types itself, th self application
x x has no type. You can try yourself:
/* Typed Variable */
typeof(_:A, B) :-
    unify_with_occurs_check(A, B).
/* Modus Ponens */
typeof((S*T), B) :-
    typeof(S, (A -> B)),
    typeof(T, A).
And then the query:
?- X=_:_, typeof((X*X), T).
false.
The query will though succeed if you remove
the occurs check.
Bye
Julio Di Egidio schrieb:

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