Path: ...!news.mixmin.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Andrej Bauer is a red flag (Was: How to prove this theorem with
 intuitionistic natural deduction?)
Date: Sun, 1 Dec 2024 11:56:34 +0100
Message-ID: <vihfd2$8qss$1@solani.org>
References: <vhgdq0$19evr$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 1 Dec 2024 10:56:34 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="289692"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:x7Lx/jxBxTCDJumrFRXRedYBdhU=
In-Reply-To: <vhgdq0$19evr$1@dont-email.me>
X-User-ID: eJwFwYEBwCAIA7CXRCjYc4qO/09YAk/LW5HIwGB29WwGnolqLsoscErxpU3rurikruNgnXV3+oun8W6N+ANOsBXp
Bytes: 1761
Lines: 26

Hi,

 > Meanwhile, you might have seen it, I have also asked on SE:
 > 
<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>

Sorry, but I must quite. Anything where Andrej Bauer is
a red flag. I remember he was censoring some post of mine,
don't remember exactly where it was.

You can try searching here:

https://groups.google.com/g/sci.logic/search?q=Andrej%20Bauer%20


Julio Di Egidio schrieb:
> Dear logicians,
> 
> How to prove the following theorem with natural deduction in 
> intuitionistic propositional logic (namely, no classical inference rules)?
> 
>    `(P -> Q -> R) |- (P /\ Q -> R)`
> 
> Thanks for any help.
> 
> -Julio