# 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
```