Re: What are Simple Types (Was: Proofs as programs)

This is also not in the scope of advent of logic:
From: Mild Shock <janburse@fastmail.fm>
Date: Mon, 18 Nov 2024 23:22:11 +0100
Subject: Re: How to prove this theorem with intuitionistic natural deduction?
 > 0: P -> (Q -> R) (Premisse)
 > 1: P /\ Q        (Assumption)
 > 2: P             (/\E,1)
 > 3: Q -> R        (->E,0,2)
 > 4: Q             (/\E,1)
 > 5: R             (->E,3,4)
 > 6: P /\ Q -> R   (Discharge,1)
The advent of logic has only implication (->)/2
and no conjunction (/\)/2:
 > Advent of Logic 2024: Weekend 2
 > [...]
 > The propositional logic can do with
 > *implication only*, and it should be Linear Logic.
 > French logician Jean-Yves Girard is credited
 > [...]
It says implication only. Just like here, implication
only is sometimes called positive logic:
Meredith, D. (1978). Positive logic and λ-constants.
Studia Logica, 37(3), 269–285. doi:10.1007/bf02124728
I think the example I gave is on page 288. The
lambda expression would need an additional combinator
W, it cannot be modelled with BCI alone:
λx:A->A.λy:A.(x (x y))   :  ((A -> A) -> (A -> A))
Meredith, D. gives the combinator expression BCWI.
Didn't verify. The combinator W is left contraction,
and since affine logic has no contraction, the
combinator W is not part of affine logic:
W: ((A -> (A ->B)) -> (A -> B))
Mild Shock schrieb:

Julio Di Egidio schrieb:

On 19/12/2024 00:30, Mild Shock wrote:

It cannot be a proof term of Affine Logic, since x occurs twice.

That is not what affine logic means.

 Well it does. It is based on the combinators B and C.
You cannot translate a lambda expression where x occurs twice
with B and C. You would need S.
 Rule 7 and 8
https://en.wikipedia.org/wiki/Combinatory_logic#Combinators_B,_C
 With B and C, you can only translate λx.(E1 E2) if x
occurs in E1 or E2 or none, but not in both E1 and E2.
 Basically the implied requirement to have an equivalence
between the natural deduction and the hilbert style proofs,
that every lambda express can be translated to BCI.
 Bye