G\"odel's Natural Deduction

TL;DR

This paper explores G"odel's natural deduction system, based on his unpublished notes and its relation to his philosophical views and proof theory, providing historical and technical insights.

Contribution

It presents a detailed analysis of G"odel's natural deduction system using Gentzen's sequents, which was previously not well documented.

Findings

G"odel's natural deduction system aligns with Jaśkowski's 1934 system.

Historical notes clarify G"odel's interest in sequents.

The paper offers a reexamination of G"odel's approach in light of his unpublished notes.

Abstract

This is a companion to a paper by the authors entitled "G\"odel on deduction", which examined the links between some philosophical views ascribed to G\"odel and general proof theory. When writing that other paper, the authors were not acquainted with a system of natural deduction that G\"odel presented with the help of Gentzen's sequents, which amounts to Ja\'skowski's natural deduction system of 1934, and which may be found in G\"odel's unpublished notes for the elementary logic course he gave in 1939 at the University of Notre Dame. Here one finds a presentation of this system of G\" odel accompanied by a brief reexamination in the light of the notes of some points concerning his interest in sequents made in the preceding paper. This is preceded by a brief summary of G\"odel's Notre Dame course, and is followed by comments concerning G\"odel's natural deduction system.