Re: Simple Types cannot ban Curry Paradox? (Was: Honoring Raymond Smullyan)

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