Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem

Hugo Herbelin, Danko Ilik

TL;DR

This work applies the Curry-Howard correspondence approach to Henkin’s proof to phrase it as a program which transforms any proof of validity with respect to Tarski semantics into a proof of derivability.

Abstract

G{ö}del's completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of valid formula to the notion of provable formula.We survey a few standard formulations and proofs of the completeness theorem before focusing on the formal description of a slight modification of Henkin's proof within intuitionistic second-order arithmetic.It is standard in the context of the completeness of intuitionistic logic with respect to various semantics such as Kripke or Beth semantics to follow the Curry-Howard correspondence and to interpret the proofs of completeness as programs which turn proofs of validity for these semantics into proofs of derivability.We apply this approach to Henkin's proof to phrase it as a program which transforms any proof of validity with respect to Tarski semantics into a proof of derivability.By doing so, we hope to shed an effective light on the relation between Tarski semantics and syntax: proofs of validity are syntactic objects with which we can compute.

An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem

TL;DR

This work applies the Curry-Howard correspondence approach to Henkin’s proof to phrase it as a program which transforms any proof of validity with respect to Tarski semantics into a proof of derivability.

Abstract

G{ö}del's completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of valid formula to the notion of provable formula.We survey a few standard formulations and proofs of the completeness theorem before focusing on the formal description of a slight modification of Henkin's proof within intuitionistic second-order arithmetic.It is standard in the context of the completeness of intuitionistic logic with respect to various semantics such as Kripke or Beth semantics to follow the Curry-Howard correspondence and to interpret the proofs of completeness as programs which turn proofs of validity for these semantics into proofs of derivability.We apply this approach to Henkin's proof to phrase it as a program which transforms any proof of validity with respect to Tarski semantics into a proof of derivability.By doing so, we hope to shed an effective light on the relation between Tarski semantics and syntax: proofs of validity are syntactic objects with which we can compute.
Paper Structure (13 sections, 20 equations, 1 figure)

This paper contains 13 sections, 20 equations, 1 figure.

Table of Contents

  1. Preliminaries
  2. The completeness theorem
  3. Weak and strong completeness
  4. The standard existing proofs of completeness
  5. Models and truth
  6. Regarding the metalanguage as a formal system
  7. The computational content of completeness proofs for intuitionistic logic
  8. The intuitionistic provability of the different statements of completeness
  9. Chronology and recent related works
  10. The computational content of Henkin's proof of Gödel's completeness
  11. Henkin's proof, slightly simplified
  12. From Henkin's proof to a proof with respect to possibly-exploding models
  13. The computational content of the proof of completeness

Figures (1)

  • Figure 1: Inference rules characterising minimal implicational logic