Skip to content

Abstracts.2021.NbE.STLC

Jump to bottom
Fabian edited this page Nov 26, 2021 · 16 revisions

On Consistency, Models, and Normalization for Intuitionistic Propositional Logic (IPL)

With Application to Normalization for the Simply-Typed Lambda Calculus (STLC)

by Andreas Abel

Abstract

TL;DR We demonstrate normalization-by-evaluation (NbE) for STLC, i.e., how to get a normalization function from an implementation of a Kripke model for IPL in Agda.

The discipline of logic, in its foundational flavor, is concerned with formalizing reasoning, by identifying a formal language of propositions and a set of inference rules that allow us to prove propositions. Thus formed logical systems should enjoy certain properties; their study is often referred to as meta-theory. Of utmost importance is the property of consistency, stating that not every proposition is provable.

We shall focus on the logical system of intuitionistic propositional logic (IPL) where propositions are constructed from propositional variables P and the atomic proposition ⊤ (truth) and ⊥ (falsity/absurdity) via the logical connectives ∧ (conjunction), ∨ (disjunction) and ⇒ (implication). Consistency there means that absurdity ⊥ is unprovable.

A direct stab at consistency for IPL, by analysing all potential proofs of ⊥, must unfortunately fail. For instance, a potential proof could conclude by the modus ponens rule, given proofs of A ⇒ ⊥ and A for some proposition A which can be arbitrarily complex. Even for the simple case of A=⊤ we are now left with refuting ⊤ ⇒ ⊥ which is no more simple then ⊥.

Gerhard Gentzen solved this problem in the 1930s by normalization[1]. In the case of IPL, this states that every provable proposition also has a proof in normal form. And normal forms are much more suited to analysis; it is easy to argue that there is no normal proof of ⊥.

But consistency can also be shown model-theoretically. In the case of classical propositional logic, one model is the Tarski semantics which assigns to each proposition its truth value (basically, truth-table semantics). For IPL, this model is sound but not adequate as it validates e.g. the law of excluded middle which is not provable in IPL.

Instead, IPL is interpreted in Kripke models. A Kripke model is parametrized by a preorder W of worlds where w' ≤ w can be thought of as "w' is a future of w" and formulas A are interpreted as truth values ⟦A⟧w relative to a world w. The interpretation is monotone in the sense that ⟦A⟧w implies ⟦A⟧w' when w' ≤ w, so "knowledge does not disappear", or "statements can only become more true in the future". Implication A ⇒ B is interpreted as ⟦A⇒B⟧w = ∀w'≤w. ⟦A⟧w' ⇒ ⟦B⟧w', giving implication its intuitionistic flavor and refuting excluded middle. Absurdity ⊥ is interpreted as "false" in any world. The fundamental theorem states that any provable formula is true in all worlds of all Kripke models; thus consistency follows since ⟦⊥⟧w is never true.

Models give us a concept of truth of a proposition, and allow us to study the completeness of our logical system: Is every true formula also provable? IPL is actually complete for Kripke models1. So if a proposition A is valid in all Kripke models, then also in the model where the set W of worlds are lists Γ of hypotheses (i.e., contexts), and Γ' ≤ Γ holds if Γ is a sublist of Γ'. By induction on the proposition A, we can extract an even normal proof of A from ⟦A⟧.

By formulating the soundness and completeness proofs for Kripke models in a constructive meta theory, such as Agda, we can obtain a normalization procedure by composition of the soundness and completeness arguments: From a proof of A we get an element of ⟦A⟧ from which we extract a normal proof of A. This procedure is called NbE. By the Curry–Howard correspondence between IPL and STLC, we obtain a normalizer for STLC.

In the lecture I want to spell out the argument for the negative fragment of IPL first (⊤, ∧, ⇒), and time-permitting also for the positive connectives (⊥, ∨).

  1. ^ The completeness proof of IPL for Kripke models is constructive for the negative fragment, but requires classical arguments for the positive connectives. The concept of Kripke model can be refined to Beth model by adding a cover relation between world sets. The completeness proof of IPL for Beth models can be carried out constructively. Consequently, when implementing NbE for full IPL, we need to use a Beth model or an equivalent formulation of coverage in our semantics.

Lecture material

Exercises

  • Solve one of the 19 exercises on the handout
  • Solve the exercise and question in the notes in section "Application of Kripke models: IPL is non-classical"
  • Give a Kripke model that refutes the law of excluded middle, double-negation elimination, and Peirce's law ((A ⇒ B) ⇒ A) ⇒ A)
  • Give a Kripke model that refutes the Gödel–Dummett law (A ⇒ B) ∨ (B ⇒ A)
  • Show that IPL has the finite-model property and conclude that IPL is decidable
  • Show that IPL has the disjunction property and conclude (again) that the law of excluded middle is not a theorem of IPL
  • Show that evaluation in the universal model followed by the completeness proof produces βη-equal proof terms, that is norm t =βη t

References

  1. ^ Gerhard Gentzen, Untersuchungen über das logische Schließen, Mathematische Zeitschrift, 1935. English translation PDF: https://www.cs.cmu.edu/~crary/819-f09/Gentzen35.pdf

Other resources

Related ITC talks:

Related implementations:

Bibliography

Clone this wiki locally