**LQ**of weak excluded middle (also known as Jankov's logic). (See my earier post on the subject.) The idea is, simply, to replace the usual Felscher rule D10, which says

toPcan assert an atomponly ifOhas already assertedp

Chris Fermüller has kindly provided a counterexample to the claim that the usual rules for intutionistic logic, with D10 replaced by this modified version of it, generatesPcan assert an atomponly ifOhas either already assertedpor already asserted ¬p.

**LQ**: the formula ¬

*p*→

*p*is valid in this setting! The idea is that

**O**asserts ¬

*p*, then

**P**can assert

*p*and win the game. That ¬

*p*→

*p*is not valid in

**LQ**is clear because the formula is not classically valid, and

**LQ**is an intermediate logic. Back to the drawing board…

Sounds like a very obvious counterexample.

ReplyDelete