Re: Andrej Bauer is a red flag (Was: How to prove this theorem with intuitionistic natural deduction?)

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.

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