Liste des Groupes | Revenir à s logic |
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
Les messages affichés proviennent d'usenet.