Path: ...!3.eu.feeder.erje.net!feeder.erje.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: How to make cyclic terms (Was: A miraculous match?)
Date: Thu, 9 Jan 2025 13:23:57 +0100
Message-ID: <vlof4t$21qd0$1@solani.org>
References: <vlkfq7$1vh4j$1@solani.org> <vlkrge$2dkpc$1@dont-email.me>
 <vllgli$2039r$1@solani.org> <vlmdk8$2dkpd$6@dont-email.me>
 <vlme6h$2dkpc$3@dont-email.me> <vlo9os$2dkpd$11@dont-email.me>
 <vloa2b$2dkpd$12@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 9 Jan 2025 12:23:57 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2156960"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:128.0) Gecko/20100101
 Firefox/128.0 SeaMonkey/2.53.20
Cancel-Lock: sha1:/8quoHJbgIMiH1/lZbgNYgBNuZM=
X-User-ID: eJwFwQkBwDAIA0BL0JKUyeH1L2F3uFTWM4KGxRIxayw3kS73cZuumGGcffGyOL1fSgHNoxmm6Rj1vSeP/ICNFn8=
In-Reply-To: <vloa2b$2dkpd$12@dont-email.me>
Bytes: 2293
Lines: 33


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.

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.)