Warning: mysqli::__construct(): (HY000/1203): User howardkn already has more than 'max_user_connections' active connections in D:\Inetpub\vhosts\howardknight.net\al.howardknight.net\includes\artfuncs.php on line 21
Failed to connect to MySQL: (1203) User howardkn already has more than 'max_user_connections' active connectionsPath: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: Julio Di Egidio Newsgroups: sci.logic Subject: Re: Negative translation for propositional linear (or affine) logic? Date: Thu, 28 Nov 2024 02:17:15 +0100 Organization: A noiseless patient Spider Lines: 46 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Thu, 28 Nov 2024 02:17:15 +0100 (CET) Injection-Info: dont-email.me; posting-host="52d3d32bb300a58b1c7fce645c7cbe65"; logging-data="56369"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+VPGvrO/AbtGKDNnVsOLf/kA46QGSEQo0=" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:743ruG3UmLQfHq+t8TTbvoCiqJE= In-Reply-To: Content-Language: en-GB Bytes: 3161 On 28/11/2024 01:52, Julio Di Egidio wrote: > On 28/11/2024 00:55, Mild Shock wrote: >> This is Peirce law: >> ((p->q)->p)->p >> Peirce law is not provable in minimal logic. >> >> But I guess this is not Glivenko: >> notation(dnt(X), ~X->(~(~X))) >> >> https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic >> >> Glivenko would be simply: >> notation(gliv(X), (~(~X))) > > Indeed Glivenko's is to embed classical into intuitionistic, not into > linear (or affine). > > OTOH, you can try the code yourself: with that 'dnt' the solver solves > all the classical theorems I have been able to think about, Pierce's law > included, otherwise it fails: because of linearity essentially, i.e. not > enough hypotheses... > > > That said, that 'dnt' is almost surely not really correct, indeed maybe > it only works for me because my reduction rules are linear (affine > actually), yet my operators for now are only the intuitionistic ones, I > do not have the whole set of linear operators. Though that is itself most probably nonsense: there are no linear operators in the classical theorems... > Here are lecture notes that maybe have a complete answer/recipe, see > from page 5, but I still cannot fully parse what they write: > > > Meanwhile, you might have seen it, I have also asked on SE: > And I thought this was an easy one. Maybe that 'dnt' *is* correct: but maybe not. I just thought the expert would know straight away: me, I'd have to formalize the whole thing in Coq to prove meta-properties, but then I don't know what I am paying taxes for... -Julio