Distinction between Computation & Derivation (Was: Minimal Logics in the 2020's: A Meteoric Rise)

Hi,
Thats quite a deseases, even Wadler makes the
error, when he automatically associates the curry
howard isomorphism, to evaluation strategies.
Often proof normalization cannot go as far
as evaluation strategies can go. A simple example
is the Y combinator. You can try yourself,
I am adding the “I” combinator which we have
already shown to be derivable, and then a
new “Y” combinator:
/* I axiom */
typeof(i, (A -> B)) :-
    unify_with_occurs_check(A,B).
/* Y axiom */
typeof(y, ((A -> B) -> C)) :-
    unify_with_occurs_check(A,B),
    unify_with_occurs_check(A,C).
Lets see what happens, can we prove anything?
?- between(1,6,N), search(typeof(X, a), N, 0).
N = 3,
X = y*i .
Yes it collapses trivally, even doesn’t need a
complicated Curry Paradox.
Bye
Mild Shock schrieb:

Could be a wake-up call this many participants
already in the commitee, that the whole logic
world was asleep for many years:
 Non-Classical Logics. Theory and Applications XI,
5-8 September 2024, Lodz (Poland)
https://easychair.org/cfp/NCL24
 Why is Minimal Logic at the core of many things?
Because it is the logic of Curry-Howard isomoprhism
for symple types:
 ----------------
Γ ∪ { A } ⊢ A
 Γ ∪ { A } ⊢ B
----------------
Γ ⊢ A → B
 Γ ⊢ A → B           Δ ⊢ A
----------------------------
Γ ∪ Δ ⊢ B
 And funny things can happen, especially when people
hallucinate duality or think symmetry is given, for
example in newer inventions such as λμ-calculus,
 but then omg ~~p => p is nevertheless not provable,
because they forgot an inference rule. LoL
 Recommended reading so far:
 Propositional Logics Related to Heyting’s and Johansson’s
February 2008 - Krister Segerberg
https://www.researchgate.net/publication/228036664
 The Logic of Church and Curry
Jonathan P. Seldin - 2009
https://www.sciencedirect.com/handbook/handbook-of-the-history-of-logic/vol/5/suppl/C   Meanwhile I am going back to my tinkering with my
Prolog system, which even provides a more primitive
logic than minimal logic, pure Prolog is minimal
 logic without embedded implication.