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: intuitionistic vs. classical implication in Prolog code Date: Sun, 1 Dec 2024 19:30:22 +0100 Organization: A noiseless patient Spider Lines: 27 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Sun, 01 Dec 2024 19:30:23 +0100 (CET) Injection-Info: dont-email.me; posting-host="9457540d49654f8b44273a26fe4626ef"; logging-data="2582992"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+XiPPNWqj90gw4ysMljjIKwSgnd0HMFQY=" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:o41KQCz7qujAEg/OdwvhC2znQmA= In-Reply-To: Content-Language: en-GB Bytes: 2165 On 01/12/2024 17:27, Mild Shock wrote: > Well then Pierce Law is not povable under > the usual Glivenko translation in affine logic. > So what? Whats your point? That my TNT (I am now dubbing it "triple-negation translation") instead works, and where is some piece of theory to attach to it? > I found only one book that discusses Glivenk > style translations for substructural logics: > Chatpter 8: Glivenko Theorems > Residuated Lattices: an algebraic glimpse at substructural logics > https://www.researchgate.net/publication/235626321 Indeed there is a lot of not much around. But Girard talks about not having and not wanting a separate semantics, it's all purely syntactic. But I still have only a vague intuition about what that means. Anyway, pretty much along that line, I am thinking: could I prove in Prolog the meta-properties I have proved in Coq (so far)? Meta-programming and program-analysis features of Prolog are certainly not lacking... -Julio