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

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,
 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
 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?
 Bye