>>536
Aの部分論理式として
¬Aも、¬¬Aも認めないのであれば成り立たないですよね

で、¬¬Aを部分論理式として認めると、その帰結としては背理法・対偶を使わない正規形が存在しない、ということは言えませんよね
ということです

正規化定理⇒(修正された)部分論理式原理はいえても
部分論理式原理⇒正規形に間接証明を用いているものがない
は言えないと思う、ということなのですが…