Path: ...!npeer.as286.net!npeer-ng0.as286.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: Re: Simple Types cannot ban Curry Paradox? (Was: Honoring Raymond
 Smullyan)
Date: Thu, 9 Jan 2025 14:28:35 +0100
Message-ID: <vloiu3$2ddrt$1@solani.org>
References: <vlkfq7$1vh4j$1@solani.org> <vloh9r$21r7p$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 9 Jan 2025 13:28:35 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2537341"; 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:3y6buqiq1p9BhnvBL4WH97Abemw=
X-User-ID: eJwNycEBwCAIA8CVIECEcVB0/xHa+14YlWc5gx4v3qoGj+ZsvQmTP2G1nlW7pG6EzCExYXuku4iOqrmAemI+MswUlw==
In-Reply-To: <vloh9r$21r7p$1@solani.org>
Bytes: 3599
Lines: 99

Hi,

So what is the congruence relation that leads
to the amazing wild card derivation:

(C ≌ C -> A) -> A

In our formulation we prove this here:

(a <-> (a -> b)) -> b

But we are too lazy for biconditional,
so we prove this here:

(a -> (a -> b)) /\ ((a -> b) -> a) -> b

Well that also not quite right we are too lazy
for conjunction, so we prove this here.

(a -> (a -> b)) -> (((a -> b) -> a) -> b)

Bye

Mild Shock schrieb:
> Hi,
> 
> Although Simple Types can ban self application,
> like making (x x) typeable is impossible. It cannot
> completely ban the Curry Paradox,
> 
> since we can still derive:
> 
> ?- between(1,16,N), search(typeof(X, [],
>     ((a->(a->b))->(((a->b)->a)->b))), N, 0).
> N = 15,
> X = lam(lam(lam(0*(1*0))*lam(2*0*0))) .
> 
> This is a well known fact that in Minimal Logic
> the Curry Paradox is still derivable. But what
> about Affine Logic, can it ban the Curry Paradox?
> 
> I guess so, if Affine Logic ban contraction,
> then Lambda Exprssions such as lam(0*(1*0)) and
> lam(2*0*0) cannot be formed, since 0 apears twice.
> 
> But how rigorously show the conjecture that
> Affine Logic bans the Curry Paradox?
> 
> Bye
> 
> Source code for the proof search with de Brujin
> indexes, which requires a ternary typeof/3, since
> we need also pass around a context L:
> 
> /* Implication Intro */
> typeof(lam(Y), L, (A -> B)) :-
>     typeof(Y, [A|L], B).
> /* Axiom */
> typeof(K, L, B) :-
>     nth0(K, L, A),
>     unify_with_occurs_check(A, B).
> /* Modus Ponens */
> typeof((S*T), L, B) :-
>     typeof(S, L, (A -> B)),
>     typeof(T, L, A).
> 
> search(true, N, N).
> search((A,B), N, M) :-
>     search(A, N, H),
>     search(B, H, M).
> search(typeof(P, L, T), N, M) :- N>0, H is N-1,
>     clause(typeof(P, L, T), B),
>     search(B, H, M).
> search(unify_with_occurs_check(A,B), N, N) :-
>     unify_with_occurs_check(A,B).
> search(nth0(K, L, A), N, N) :-
>     nth0(K, L, A).
> 
> 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
>