Creo que dada la negación de la introducción y eliminación, la RAA y la doble negación son equivalentes. Por lo tanto, dada la negación de la introducción o eliminación, en el que los dos sistemas debe ser equivalente, independientemente de que usted toma. Es cierto que esto está fuera de mi área de conocimiento, o más bien ha sido un largo tiempo desde que hice la lógica formal. Pero estoy bastante seguro de que independientemente de que la regla de inferencia que asumir, se puede derivar el otro como un derivado de la regla de inferencia.
Prueba:
Supongamos RAA es una regla de inferencia, a continuación, suponiendo que tenemos conjunción introducción (que en realidad no se da una lista completa de las reglas de inferencia en el texto, así que voy a asumir que usted tiene), de $\neg\neg P, \neg P$, podemos deducir $\neg P \wedge \neg\neg P$, y, por tanto, $\bot$ por la negación de la eliminación. Por lo $\neg\neg P,\neg P \vdash \bot$, lo $\neg\neg P \vdash P$ RAA.
Por otro lado, si el doble negación es elegido, si $\Gamma,\neg P \vdash \bot$, luego por la negación de la introducción, $\Gamma \vdash \neg \neg P$, y por la doble negación, $\Gamma \vdash P$.
