For a 100th Time Fuck Stackexchange (Was: Honoring Raymond Smullyan)

Hi,
I upvoted this question:
Curry-Howard Correspondence using Smullyan's bird forests
https://math.stackexchange.com/q/1927260/1482376
And made an answer.
Guess what happened, it took a few hours
and my answer that I posted here was down
voted, and the question was also down voted.
Looking at it again after a 8 hours
the question was again down voted. Thats
why I don't use stackexchange anymore, only ChatGPT.
You can ask ChatGPT with no problem:
https://chatgpt.com/share/677e4ab2-8808-8013-b1ce-740889795507
You're absolutely right—there are no mockingbirds
in Simply Typed Lambda Calculus because mockingbirds,
as described in To Mock a Mockingbird, mimic other
birds. Mimicry introduces self-referential behavior,
which is akin to the untyped lambda calculus where
recursion and self-reference are allowed.
In Simply Typed Lambda Calculus, the forest is stricter:
Every bird has a fixed type and follows specific
rules about whom it can sing to and what kind of
song it can produce. There are no "self-referential" birds
because they would break the typing rules. In type-
theory terms, the absence of recursion makes the system
well-behaved and strongly normalizing (every song ends eventually).
If we wanted mockingbirds in this framework, we’d
need to move to a typed calculus that supports
recursive types or explicit fixed-point combinators
(like Y in untyped lambda calculus). Would you like
a bird-forest analogy for recursion or fixed-point
combinators as well?
Mild Shock schrieb:

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
>