Contents

Propositions as types

6. Propositions as types

In today’s lecture we shall refrain from formalizing anything in Agda and will instead stick to the good old pen & paper mathematics. We shall keep Agda to a minimum. These lecture notes are shorter than usual because they include references to supplementary notes and reading material. There is no lack of written accounts of the topics under consideration.

open import Level
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import Data.Product
import Data.Sum
import Data.Empty
import Data.Unit

module 06-propositions-as-types where

The purpose of doing so is twofold. Firstly, many class projects are directly related to the content of the lecture, and we do not want to detract from the joy of formalizing a topic from scratch. Secondly, we really do want to focus on the mathematical content and the ideas, and less on technique.

Reading material for today’s lecture:

6.1. Revisiting the semantics of propositional calculus

Last time we stated the soundness and completeness of Boolean semantics of classical propositional logic. In the exercises you worked on showing the soundness theorem. Once again it turned out that proving the main result, namely “if \(\phi\) is provable then it is a tautology”, required a generalization to hypothetical judgements that made the induction arguments go through:

\(\newcommand{\sem}[1]{[\![#1]\!]}\)

Theorem

If \(\phi_1, \ldots, \phi_{n} \vdash \phi\) is provable then for all valuations \(\eta : A \to 2\)

\[\sem{\phi_1} \eta \land \cdots \land \sem{\phi_n} \eta \leq \sem{\phi} \eta.\]

Above \(\sem{\phi} : 2^A \to A\) is the semantic meaning of a formula. One should expect such a generalization to appear because proving a formula in the empty context \(\vdash \phi\) leads to a non-empty context by the \(\Rightarrow\)-introduction and \(\lor\)-elimination rules.

The Boolean semanticcs is of course sound for the intuitionistic logic as well, because anything that is provable without excluded middle is also proveable with it. However, if we also wanted completeness, we would have to use Heyting algebras instead. We do not do so here, but rather concentrate on a connection between logic and computation, known as the Curry-Howard correspondence or propositions-as-type.

6.2. The simply typed λ-calculus

The simply typed λ-calculus (STLC) is the fragment of type theory with simple types (non-dependent types), and the constructors \(\to\), \(\times\), \(+\), \(\mathtt{unit}\), \(\mathtt{empty}\), and possibly as a collection of primitive types, constants, and equations.

See a review of \(\lambda\)-calculus for details.

6.3. Propositions as types

Propositions as types or the Curry-Howard correspondence is a fundamental correspondence between logic and computation which reveals, in its basic form, that proofs can be read as programs and vice versa. The connection has inspired the development of logic and programming languages, both in theory and practice. For instance, Agda works by this principle.

In the lecture we shall explain the idea by looking more closely at the correspondence between propositional logic and STLC, and less closely at predicate logic and dependent types.

In order to achieve good understanding and technical proficiency, we recommend reading:

6.4. Propositions as [types]

We shall also discuss a refinement of the idea “propositions as types” which postulates that only some types are propositions, namely those that have at most one element. In other words, under “propositions-as-types” a propositions is understood as the type of its proofs, of which there may be many, whereas in “propositions-as-types-with-at-most-one-elment” a proposition is understood in terms of its truth: its elements do not reveal why the proposition holds, only that it does.

Further reading material:

Below is the begining of an Agda formalization of propositional truncation and the truncated logic, fashioned after IUFMA.

module TruncationLogic where
  open import Axiom.Extensionality.Propositional using (Extensionality)

  postulate fun-ext : ∀ {a b} → Extensionality a b


  is-proposition : {ℓ : Level} → Set ℓ → Set ℓ
  is-proposition A = (x y : A) → x ≡ y

  record truncation-structure : Setω where
    field
      ∥_∥ : {ℓ : Level} → Set ℓ → Set (suc ℓ)
      ∥∥-is-proposition : {ℓ : Level} (A : Set ℓ) → is-proposition ∥ A ∥
      ∣_∣ : {ℓ : Level} {A : Set ℓ} → A → ∥ A ∥
      ∥∥-elim : {ℓ k : Level} {A : Set ℓ} {B : Set k} →
                is-proposition B → (A → B) → ∥ A ∥ → B

    infix 0 ∥_∥

    ∥∥-compute : {ℓ k : Level} {A : Set ℓ} {B : Set k} →
                 (i : (x y : B) → x ≡ y) (p : A → B) (a : A) → ∥∥-elim i p ∣ a ∣ ≡ p a
    ∥∥-compute i p a = i (∥∥-elim i p ∣ a ∣) (p a)


  module _ {ts : truncation-structure} where
    open Data.Product hiding (∃)
    open Data.Sum
    open Data.Empty
    open Data.Unit

    open truncation-structure ts public

    record HProp (ℓ : Level) : Set (suc ℓ) where
      constructor ⟨_,_⟩
      field
        proof : Set ℓ
        is-prop : is-proposition proof


    module _ {k ℓ : Level} where
      open HProp

      infixr 6 _∧ʰ_
      infixr 5 _∨ʰ_
      infixr 4 _⇒ʰ_

      ⊥ʰ : HProp zero
      ⊥ʰ = ⟨ ⊥ , (λ x y → ⊥-elim x) ⟩

      ⊤ʰ : HProp zero
      ⊤ʰ = ⟨ ⊤ , (λ _ _ → refl) ⟩

      _∧ʰ_ : HProp k → HProp ℓ → HProp (k ⊔ ℓ)
      ⟨ p , ξ ⟩ ∧ʰ ⟨ q , ζ ⟩ = ⟨ p × q , θ ⟩
        where
          θ : (x y : p × q) → x ≡ y
          θ (x₁ , y₁) (x₂ , y₂) with ξ x₁ x₂ | ζ y₁ y₂
          ... | refl | refl = refl

      _⇒ʰ_ : HProp k → HProp ℓ → HProp (k ⊔ ℓ)
      ⟨ p , ξ ⟩ ⇒ʰ ⟨ q , ζ ⟩ = ⟨ (p → q) , θ ⟩
        where
          θ : is-proposition (p → q)
          θ f g = fun-ext λ x → ζ(f x) (g x)

      _∨ʰ_ : HProp k → HProp ℓ → HProp (suc k ⊔ suc ℓ)
      ⟨ p , ξ ⟩ ∨ʰ ⟨ q , ζ ⟩ = ⟨ ∥ p ⊎ q ∥ , θ ⟩
        where
          θ : is-proposition ∥ p ⊎ q ∥
          θ = ∥∥-is-proposition _

      ∃ʰ : (A : Set k) → (A → HProp ℓ) → HProp (suc k ⊔ suc ℓ)
      ∃ʰ A ϕ = ⟨ ∥ Σ[ x ∈ A ] proof (ϕ x) ∥ , ∥∥-is-proposition _ ⟩

      ∀ʰ : (A : Set k) → (A → HProp ℓ) → HProp (k ⊔ ℓ)
      ∀ʰ A ϕ = ⟨ (∀ x → proof (ϕ x)) , (λ f g → fun-ext (λ x → is-prop (ϕ x) (f x) (g x))) ⟩

      -- We need to validate the rules of logic, here is a sample

      ∨ʰ-intro₁ : {A : HProp k} {B : HProp ℓ} → proof A → proof (A ∨ʰ B)
      ∨ʰ-intro₁ p = ∣ inj₁ p ∣

      ∃ʰ-elim : {m : Level} {A : Set k} (ϕ : A → HProp ℓ) (ψ : HProp m) →
               ((x : A) → proof (ϕ x) → proof ψ) → proof (∃ʰ A ϕ) → proof ψ
      ∃ʰ-elim ϕ ψ f p = ∥∥-elim (is-prop ψ) (λ { (x , q) → f x q }) p

previous

5. Logic