 Now we are considering the syntactic translation \(\tau\) from the common language of PA and HA into its “negative” fragment that replaces disjunctions \(A\lor B\) by their de Morgan equivalent \(\neg (\neg A\land \neg B)\) and existential statements \(\exists x A(x)\) by \(\neg \forall x \neg A(x)\). The reductive result obtained by Gentzen and Gödel in 1933 is now stated quite easily: