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

Hi,
 > are you saying that System F is inconsistent?
I didn't say anything about System F.
All the Prolog examples I posted were simple types.
Whats wrong with you? Can you point anything
I said originally about System F?
Otherwise you can read yourself about System F
I am not baby sitting on System F.
Bye
Julio Di Egidio schrieb:

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