Proof that in the Simple Type Theory (as stated in Grelling/Theory.lean) the Grelling's Paradox can be derived.
This proof has no computational-content due to the proof requiring impredicative quantification which is only achievable in Prop.
This proof is presented using Classical reasoning, in particular appealing to the Law of Excluded Middle. There are other formulations that use Intuionistic reasoning.
The proof can be found on Grelling/Proof.lean.
Thank you to Oliver Marshall for his presentation of the paradox and its proofs during the Seminar on Language Theory and Programming Languages Foundations at UNAM, co-hosted by Dr. Lourdes del Carmen Gonzáles Huesca.
The proof in this repository follows the one shared by Oliver.