E. Nelson, ๐ผ๐๐ผ๐๐ผโ๐๐
The Hilbert-Ackermann consistency theorem implies that there is no proof of a contradiction, even with quantifiers, in $ @\mathsf{Q}. This theorem can be only partially established in $ \mathsf{Q}^*. The crucial new insight is that it can be proved provided there are bounds on features of the proof (called rank and level) but emphatically not depending on the length of the proof. These bounds on rank and level cannot be proved in $ \mathsf{Q}^*, but for each specific proof, $ \mathsf{P}๏ผPeano็ฎ่ก๏ผ proves that $ \mathsf{Q}^* proves them! This opens the way to exploit the stunning proof without self-reference of Gรถdelโs second incompleteness theorem by Kritchman and Raz (Notices of the American Mathematical Society, December 2011). The upshot is that $ \mathsf{P} proves that $ \mathsf{Q} is inconsistent. But, as is well known, $ \mathsf{P} also proves that $ \mathsf{Q} is consistent. Therefore Peano Arithmetic $ \mathsf{P} is inconsistent.