Re: How to make cyclic terms (Was: A miraculous match?)

On 09/01/2025 13:23, Mild Shock wrote:

Julio Di Egidio schrieb:

(But I still wouldn't know how to create a cyclic term proper in Coq or in fact in any total functional language, despite the mechanism underlying conversion/definitional equality is logical unification, and we can even somewhat access it in Coq, via the definition of `eq`/reflexivity.)

 See here:
 A Modality for Recursion
Hiroshi Nakano - 2000 - Zitiert von: 237
https://www602.math.ryukoku.ac.jp/~nakano/papers/modality-lics00.pdf
 Even if you disband cyclic terms in your
model, like if you adhere to a strict Herband model.
If the Herband model has an equality which is a
congruence relation ≌. Nakano's paper contains
an inference rule for a congruence relation ≌.
When you have such a congruence relation, you can
 of course derive things like for example for a certain
exotic recursive type C, that the following holds:
 C ≌ C -> A
 You can then produce the Curry Paradox in simple
types with congruence. And then ultimately derive:
 |- (λx.x x)(λx.x x): A
 As in Proposition 2 of Nakano's paper.

Besides that I can now say for sure that there is no such thing as a (first-class) cyclic term in Coq (*), or in any total functional language I'd surmise, you have copiously posted and belaboured on what I had already derived, and have not actually answered the question:
Can you read at all? -- No, seriously, the question is: are you saying that System F is inconsistent?  As that's what my (formally verified) proof derives from that axiom F.
(*) <https://proofassistants.stackexchange.com/questions/4612>
-Julio