Logic
Botschaft: Intuitionistische Logik = Klassische Logik um eine zweite Art von Disjunktion erweitert.
{-# OPTIONS --allow-unsolved-metas --without-K #-} open import Level using (Level) import Level as L open import Data.Nat open import Data.Unit open import Data.List hiding ([_]) open import Data.List.Properties as List open import Data.Empty open import Data.Product open import Data.Sum as ⊎ open import Data.Bool hiding (_∨_; _∧_) open import Function.Definitions using (Injective) open import Function.Base using (_∘_; flip; case_of_; _∋_) open import Relation.Binary.PropositionalEquality open import Relation.Nullary.Negation using (¬_; contraposition; contradiction) module Logic where private variable ℓ ℓ' ℓ'' : Level A : Set ℓ B : Set ℓ' C : Set ℓ''
Do-Notation
Um die Übersetzung von klassischer zu intuitionistischer lesbarer zu machen,
nutzen wir die do-Notation:
module Maybe-Redefinition where data Maybe (A : Set ℓ) : Set ℓ where Nothing : Maybe A Just : A → Maybe A -- Example: partial functions A ⇀ B ≡ total functions A → Maybe B Maybe₂-explicit : (Maybe A) → (Maybe B) → Maybe (A × B) Maybe₂-explicit Nothing _ = Nothing Maybe₂-explicit (Just a) Nothing = Nothing Maybe₂-explicit (Just a) (Just b) = Just (a , b) _>>=_ : Maybe A → (A → Maybe C) → Maybe C Nothing >>= f = Nothing Just a >>= f = f a Maybe₂->>= : (Maybe A) → (Maybe B) → Maybe (A × B) Maybe₂->>= ma mb = ma >>= λ a → (mb >>= λ b → Just (a , b)) Maybe₃->>= : (Maybe A) → (Maybe B) → Maybe C → Maybe (A × B × C) Maybe₃->>= ma mb mc = ma >>= λ a → mb >>= λ b → mc >>= λ c → Just (a , b , c)
Dieses wiederkehrende Muster lässt sich in Agda wie folgt umschreiben,
unabhängig davon, ob _>>=_ eine Monade ist oder nicht:
Maybe₃-do : (Maybe A) → (Maybe B) → Maybe C → Maybe (A × B × C) Maybe₃-do ma mb mc = do a ← ma -- ma >>= λ a → b ← mb -- mb >>= λ b → c ← mc -- mc >>= λ c → Just (a , b , c)
Formeln
data Formula ℓ : Set (L.suc ℓ) where [_] : ∀ (A : Set ℓ) → Formula ℓ _∧ˢ_ : ∀ (ϕ ψ : Formula ℓ) → Formula ℓ _∨ˢ_ : ∀ (ϕ ψ : Formula ℓ) → Formula ℓ ¬ˢ_ : ∀ (ϕ : Formula ℓ) → Formula ℓ _→ˢ_ : ∀ (ϕ ψ : Formula ℓ) → Formula ℓ LEMˢ : Set ℓ → Formula ℓ LEMˢ A = [ A ] ∨ˢ (¬ˢ [ A ])
Intuitionistische Semantik
⟦_⟧ⁱ : Formula ℓ → Set ℓ ⟦ [ A ] ⟧ⁱ = A ⟦ ϕ ∧ˢ ψ ⟧ⁱ = ⟦ ϕ ⟧ⁱ × ⟦ ψ ⟧ⁱ ⟦ ϕ ∨ˢ ψ ⟧ⁱ = ⟦ ϕ ⟧ⁱ ⊎ ⟦ ψ ⟧ⁱ ⟦ ¬ˢ ϕ ⟧ⁱ = ¬ ⟦ ϕ ⟧ⁱ ⟦ ϕ →ˢ ψ ⟧ⁱ = ⟦ ϕ ⟧ⁱ → ⟦ ψ ⟧ⁱ _ : ∀ (A : Set ℓ) → ⟦ LEMˢ A ⟧ⁱ ≡ (A ⊎ ¬ A) _ = λ _ → refl ¬¬LEM : ∀ (A : Set ℓ) → ⟦ ¬ˢ ¬ˢ (LEMˢ A) ⟧ⁱ ¬¬LEM = λ A ¬d → (¬d ∘ inj₂) (¬d ∘ inj₁)
Klassischen Semantik
⟦_⟧ᶜ : Formula ℓ → Set ℓ ⟦ [ A ] ⟧ᶜ = A ⟦ ϕ ∧ˢ ψ ⟧ᶜ = ⟦ ϕ ⟧ᶜ × ⟦ ψ ⟧ᶜ ⟦ ¬ˢ ϕ ⟧ᶜ = ¬ ⟦ ϕ ⟧ᶜ ⟦ ϕ ∨ˢ ψ ⟧ᶜ = ¬ (¬ ⟦ ϕ ⟧ᶜ × ¬ ⟦ ψ ⟧ᶜ) ⟦ ϕ →ˢ ψ ⟧ᶜ = ¬ (⟦ ϕ ⟧ᶜ × ¬ ⟦ ψ ⟧ᶜ) -- ¬ ϕ ∨"ᶜ" ψ data Formulaᶜ ℓ : Set (L.suc ℓ) where [_] : ∀ (A : Set ℓ) → Formulaᶜ ℓ _∧ˢ_ : ∀ (ϕ ψ : Formulaᶜ ℓ) → Formulaᶜ ℓ ¬ˢ_ : ∀ (ϕ : Formulaᶜ ℓ) → Formulaᶜ ℓ
Übersetzung
module ¬¬-do where _>>=_ : ¬ ¬ A → (A → ¬ ¬ C) → ¬ ¬ C _>>=_ ¬¬a a⇒¬¬c ¬c = ¬¬a (λ a → a⇒¬¬c a ¬c) ¬¬⊥ : ¬ ¬ ⊥ → ⊥ ¬¬⊥ f = f λ x → x return : ∀ {A : Set ℓ} → A → ¬ ¬ A return x = λ y → y x ¬¬¬ϕ→¬ϕ : ∀ {A : Set ℓ} → ¬ ¬ ¬ A → ¬ A ¬¬¬ϕ→¬ϕ ¬¬¬a a = ¬¬¬a λ ¬a → ¬a a interleaved mutual open ¬¬-do int⇒classic : ∀ (ϕ : Formula ℓ) → ⟦ ϕ ⟧ⁱ → ⟦ ϕ ⟧ᶜ classic⇒int : ∀ (ϕ : Formula ℓ) → ⟦ ϕ ⟧ᶜ → ¬ ¬ ⟦ ϕ ⟧ⁱ int⇒classic [ A ] ⟦A⟧ⁱ = ⟦A⟧ⁱ int⇒classic (ϕ ∧ˢ ψ) (⟦ϕ⟧ⁱ , ⟦ψ⟧ⁱ) = (int⇒classic ϕ ⟦ϕ⟧ⁱ) , (int⇒classic ψ ⟦ψ⟧ⁱ) int⇒classic (ϕ ∨ˢ ψ) (inj₁ ⟦ϕ⟧ⁱ) = λ { (x , _) → x (int⇒classic ϕ ⟦ϕ⟧ⁱ) } int⇒classic (ϕ ∨ˢ ψ) (inj₂ ⟦ψ⟧ⁱ) = λ { (_ , x) → x (int⇒classic ψ ⟦ψ⟧ⁱ) } int⇒classic (¬ˢ ϕ) ¬⟦ϕ⟧ⁱ ⟦ϕ⟧ᶜ = (classic⇒int ϕ ⟦ϕ⟧ᶜ) ¬⟦ϕ⟧ⁱ int⇒classic (ϕ →ˢ ψ) ⟦ϕ⟧ⁱ→⟦ψ⟧ⁱ (⟦ϕ⟧ᶜ , ¬⟦ψ⟧ᶜ) = ¬¬⊥ (do ⟦ϕ⟧ⁱ ← classic⇒int ϕ ⟦ϕ⟧ᶜ let ⟦ψ⟧ⁱ = ⟦ϕ⟧ⁱ→⟦ψ⟧ⁱ ⟦ϕ⟧ⁱ return (¬⟦ψ⟧ᶜ (int⇒classic ψ ⟦ψ⟧ⁱ)))
Ende der Vorlesung am 04.05.2026
classic⇒int [ A ] ⟦A⟧ = return ⟦A⟧ classic⇒int (ϕ ∧ˢ ψ) (⟦ϕ⟧ᶜ , ⟦ψ⟧ᶜ) = do ⟦ϕ⟧ⁱ ← classic⇒int ϕ ⟦ϕ⟧ᶜ ⟦ψ⟧ⁱ ← classic⇒int ψ ⟦ψ⟧ᶜ return (⟦ϕ⟧ⁱ , ⟦ψ⟧ⁱ) -- equivalently without 'do': -- (classic⇒int ϕ ⟦ϕ⟧ᶜ) >>= λ ⟦ϕ⟧ⁱ → -- (classic⇒int ψ ⟦ψ⟧ᶜ) >>= λ ⟦ψ⟧ⁱ → -- return (⟦ϕ⟧ⁱ , ⟦ψ⟧ⁱ) classic⇒int (ϕ ∨ˢ ψ) ⟦ϕ∨ψ⟧ᶜ ⟦ϕ⟧ⁱ⊎⟦ψ⟧ⁱ→⊥ = ⟦ϕ∨ψ⟧ᶜ (contraposition (classic⇒int ϕ) (return ¬⟦ϕ⟧ⁱ) , contraposition (classic⇒int ψ) (return ¬⟦ψ⟧ⁱ)) where ¬⟦ϕ⟧ⁱ : ¬ ⟦ ϕ ⟧ⁱ ¬⟦ϕ⟧ⁱ = ⟦ϕ⟧ⁱ⊎⟦ψ⟧ⁱ→⊥ ∘ inj₁ ¬⟦ψ⟧ⁱ : ¬ ⟦ ψ ⟧ⁱ ¬⟦ψ⟧ⁱ = ⟦ϕ⟧ⁱ⊎⟦ψ⟧ⁱ→⊥ ∘ inj₂ classic⇒int (¬ˢ ϕ) ¬⟦ϕ⟧ᶜ = return (contraposition (int⇒classic ϕ) ¬⟦ϕ⟧ᶜ) classic⇒int (ϕ →ˢ ψ) ⟦ϕ→ψ⟧ᶜ ⟦ϕ⟧ⁱ↛⟦ψ⟧ⁱ = ¬¬⊥ (do -- if the implication ⟦ϕ⟧ⁱ → ⟦ψ⟧ⁱ does not hold, -- then ¬ ¬ ⟦ϕ⟧ⁱ holds, so ⟦ϕ⟧ⁱ holds classically: -- ⟦ϕ⟧ⁱ ← λ ¬⟦ϕ⟧ⁱ → ⟦ϕ⟧ⁱ↛⟦ψ⟧ⁱ (λ ⟦ϕ⟧ⁱ → ⊥-elim (¬⟦ϕ⟧ⁱ ⟦ϕ⟧ⁱ)) ⟦ϕ⟧ⁱ ← ⟦ϕ⟧ⁱ↛⟦ψ⟧ⁱ ∘ (⊥-elim ∘_) let ⟦ϕ⟧ᶜ = int⇒classic ϕ ⟦ϕ⟧ⁱ -- ⟦ψ⟧ᶜ ← λ ¬⟦ψ⟧ᶜ → ⟦ϕ→ψ⟧ᶜ (⟦ϕ⟧ᶜ , ¬⟦ψ⟧ᶜ) ⟦ψ⟧ᶜ ← ⟦ϕ→ψ⟧ᶜ ∘ (⟦ϕ⟧ᶜ ,_) ⟦ψ⟧ⁱ ← classic⇒int ψ ⟦ψ⟧ᶜ return (⟦ϕ⟧ⁱ↛⟦ψ⟧ⁱ ((⟦ ϕ ⟧ⁱ → ⟦ ψ ⟧ⁱ) ∋ (λ _ → ⟦ψ⟧ⁱ))) ) c↪i : Formulaᶜ ℓ → Formula ℓ c↪i [ A ] = [ A ] c↪i (ϕ ∧ˢ ψ) = c↪i ϕ ∧ˢ c↪i ψ c↪i (¬ˢ ϕ) = ¬ˢ (c↪i ϕ) ¬¬c↪i : Formula ℓ → Formulaᶜ ℓ ¬¬c↪i [ A ] = [ A ] ¬¬c↪i (ϕ ∧ˢ ψ) = ¬¬c↪i ϕ ∧ˢ ¬¬c↪i ψ ¬¬c↪i (¬ˢ ϕ) = ¬ˢ ¬¬c↪i ϕ ¬¬c↪i (ϕ ∨ˢ ψ) = ¬ˢ ((¬ˢ ¬¬c↪i ϕ) ∧ˢ (¬ˢ ¬¬c↪i ψ)) ¬¬c↪i (ϕ →ˢ ψ) = ¬ˢ (¬¬c↪i ϕ ∧ˢ (¬ˢ ¬¬c↪i ψ)) ¬¬ʳ : Formula ℓ → Formula ℓ ¬¬ʳ ϕ = c↪i (¬¬c↪i ϕ) -- The following statement proves the equality between to *sets* ⟦Formula-¬¬⟧ⁱ : ∀ (ϕ : Formula ℓ) → ⟦ ϕ ⟧ᶜ ≡ ⟦ ¬¬ʳ ϕ ⟧ⁱ ⟦Formula-¬¬⟧ⁱ [ A ] = refl ⟦Formula-¬¬⟧ⁱ (ϕ ∧ˢ ψ) = cong₂ _×_ IH₁ IH₂ where IH₁ : ⟦ ϕ ⟧ᶜ ≡ ⟦ ¬¬ʳ ϕ ⟧ⁱ IH₁ = ⟦Formula-¬¬⟧ⁱ ϕ IH₂ : ⟦ ψ ⟧ᶜ ≡ ⟦ ¬¬ʳ ψ ⟧ⁱ IH₂ = ⟦Formula-¬¬⟧ⁱ ψ ⟦Formula-¬¬⟧ⁱ (¬ˢ ϕ) = cong (λ X → (X → ⊥)) (⟦Formula-¬¬⟧ⁱ ϕ) ⟦Formula-¬¬⟧ⁱ (ϕ ∨ˢ ψ) = begin ⟦ ϕ ∨ˢ ψ ⟧ᶜ ≡⟨⟩ ¬ (¬ ⟦ ϕ ⟧ᶜ × ¬ ⟦ ψ ⟧ᶜ) ≡⟨ IH ⟩ ¬ (¬ ⟦ ¬¬ʳ ϕ ⟧ⁱ × ¬ ⟦ ¬¬ʳ ψ ⟧ⁱ) ≡⟨⟩ ⟦ ¬ˢ ((¬ˢ (¬¬ʳ ϕ)) ∧ˢ (¬ˢ (¬¬ʳ ψ))) ⟧ⁱ ≡⟨⟩ ⟦ ¬¬ʳ (ϕ ∨ˢ ψ) ⟧ⁱ ∎ where open ≡-Reasoning IH = cong₂ (λ x y → ¬ (¬ x × ¬ y)) (⟦Formula-¬¬⟧ⁱ ϕ) (⟦Formula-¬¬⟧ⁱ ψ) ⟦Formula-¬¬⟧ⁱ (ϕ →ˢ ψ) = cong₂ ((λ x y → ¬ (x × ¬ y))) (⟦Formula-¬¬⟧ⁱ ϕ) (⟦Formula-¬¬⟧ⁱ ψ)
Ende der Vorlesung am 07.05.2026
Stdlib
import Data.Maybe