Skip to main content
3 of 3
I edited after a comment by Andreas Blass

Representing modus ponens in a Polish propositional logic with NAND as the only connective

In a base for propositional logic using the Polish connective $\uparrow$ for not both, J. Nicod isolated one axiom as sufficient:

$\uparrow\uparrow p\uparrow q r\uparrow\uparrow t\uparrow tt\uparrow\uparrow s q\uparrow\uparrow p s\uparrow ps$

J. Nicod used the somewhat odd inference rule $r$ if $\uparrow p\uparrow q r$ and $p$. May we use $\uparrow p\uparrow r r$ and $p$ instead of Nicod's rule, or is there some deeper reason for including $q$?