Path: ...!3.eu.feeder.erje.net!feeder.erje.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: Re: Andrej Bauer is a red flag (Was: How to prove this theorem with
 intuitionistic natural deduction?)
Date: Sun, 1 Dec 2024 12:08:16 +0100
Message-ID: <vihg30$8rfi$1@solani.org>
References: <vhgdq0$19evr$1@dont-email.me> <vihfd2$8qss$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 1 Dec 2024 11:08:16 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="290290"; 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:OlXGsfAESDnM2u6SwrQtGjQ7PkI=
X-User-ID: eJwNwokRwDAIA7CV+OzQcQiU/UdodYJT2ScIBhZrm1n2r2ibuxElQjFIyvpRsxudNVwlL9JL+aBF581B5wc/dxTu
In-Reply-To: <vihfd2$8qss$1@solani.org>
Bytes: 2878
Lines: 55

Yeah, they impose a "level" on questions:

> Now if you want to join cstheory.stackexchange.com it
> says Anybody can ask a question Anybody can answer
> The best answers are voted up and rise to the top
> 
> But if you do that, they slap their policy into your face:
> It allows only questions that "can be discussed between
> two professors or between two graduate students working
> on Ph.D.'s, but not usually between a professor and a
> typical undergraduate student".
> https://meta.stackexchange.com/questions/79351/should-research-level-only-sites-be-allowed
> 
> I am not lying when I say even Andrej Bauer did
> that. But how do you want to launch a proof assistants
> site, I assume for everybody? if you cannot divert
> cs theory questions to another stackexchange?
> 
> proof assistants are full of cs theory stuff. 

Very problematic behaviour!

Mostowski Collapse - 29.11.2021, 00:19:03
https://groups.google.com/g/sci.logic/c/12DNbf3QI5I/m/V_Yal3wBBgAJ

Mild Shock schrieb:
> 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
>