KURT GÖDEL’S FIRST STEPS IN LOGIC: FORMAL PROOFS IN ARITHMETIC AND SET THEORY THROUGH A SYSTEM OF NATURAL DEDUCTION

Abstract What seem to be Kurt Gödel’s first notes on logic, an exercise notebook of 84 pages, contains formal proofs in higher-order arithmetic and set theory. The choice of these topics is clearly suggested by their inclusion in Hilbert and Ackermann’s logic book of 1928, the Grundzüge der theoretischen Logik . Such proofs are notoriously hard to construct within axiomatic logic. Gödel takes without further ado into use a linear system of natural deduction for the full language of higher-order logic, with formal derivations closer to one hundred steps in length and up to four nested temporary assumptions with their scope indicated by vertical intermittent lines.