# Decidability
```
{-# 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
open import Data.Bool hiding (_∨_; _∧_)
open import Function.Definitions using (Injective)
open import Function.Base using (_∘_; flip)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation using (¬_)

module Decidable where
private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Set ℓ
    B : Set ℓ'

```


## Entscheidbarkeit
```
data Dec (A : Set ℓ) : Set ℓ where
  yes : A → Dec A
  no : ¬ A → Dec A
```
In der Standard Library ist `Dec` ein Record aus einem `Bool` und dem
entsprechenden Beweis von `A` oder `¬ A`. Grund dafür ist die Trennung vom
Berechnungsergebnis vom Beweis dessen ([Erklärung in der
stdlib](https://agda.github.io/agda-stdlib/v2.3/README.Design.Decidability.html)).

```
_B≡?_ : ∀ (x y : Bool) → Dec (x ≡ y)
false B≡? false = yes refl
false B≡? true = no λ { () }
true B≡? false = no (λ ())
true B≡? true = yes refl

⊤? : Dec ⊤
⊤? = yes tt
⊥? : Dec ⊥
⊥? = no λ ()

_is-injective : (f : A → B) → Set _
_is-injective f = ∀ {x} {y} → f x ≡ f y → x ≡ y

suc-is-injective : suc is-injective
suc-is-injective {n} {m} refl = refl

_ℕ≡?_ : ∀ (n m : ℕ) → Dec (n ≡ m)
zero ℕ≡? zero = yes refl
zero ℕ≡? suc m = no λ ()
suc n ℕ≡? zero = no λ ()
suc n ℕ≡? suc m with (n ℕ≡? m)
... | yes n≡m = yes (cong suc n≡m)
... | no n≢m = no (n≢m ∘ suc-is-injective)
-- with-abstraction = notation for:
-- suc n ℕ≡? suc m = helper (n ℕ≡? m)
--   where
--   helper : Dec (n ≡ m) → Dec (suc n ≡ suc m)
--   helper (yes n≡m) = yes (cong suc n≡m)
--   helper (no n≢m) = no (n≢m ∘ suc-is-injective)


Dec-map : (A → B) → (B → A) → Dec A → Dec B
Dec-map A→B B→A (yes a) = yes (A→B a)
Dec-map A→B B→A (no ¬a) = no (¬a ∘ B→A)
```

## Entscheidbarkeit von Relationen
```
Decidable₂ : {A : Set ℓ} → (A → A → Set ℓ') → Set _
Decidable₂ _R_ = ∀ x x' → Dec (x R x') 
```

### Beispiele
```
L≡? : Decidable₂ (_≡_ {_} {A}) → Decidable₂ (_≡_ {_} {List A}) 
L≡? dec-A [] [] = yes refl 
L≡? dec-A [] (_ ∷ _) = no λ () 
L≡? dec-A (x ∷ xs) [] = no λ () 
L≡? dec-A (x ∷ xs) (y ∷ ys) with (dec-A x y)
... | yes refl = Dec-map (cong (x ∷_)) ∷-injectiveʳ (L≡? dec-A xs ys)
... | no x≢y = no (λ {refl → x≢y refl})
    --                 ^--- pattern-lambda


_ : ∀ (l1 l2 : List ℕ) → Dec (l1 ≡ l2)
_ = L≡? _ℕ≡?_
```


## Logik
Disjunktion in Agda
```
infixr 1 _∨_
data _∨_ (A : Set ℓ) (B : Set ℓ') : Set (ℓ L.⊔ ℓ') where
  ∨E₁ : A → A ∨ B
  ∨E₂ : B → A ∨ B

```
Negation `¬ B` = `B → ⊥`.
Ist das Gesetz vom ausgeschlossenen Dritten (Law of excluded middle) in Agda herleitbar?
```
LEM : Set → Set _
LEM A = A ∨ ¬ A

¬¬LEM : ∀ (A : Set) → ¬ ¬ (LEM A)
¬¬LEM A ¬LEM = (¬LEM ∘ ∨E₂) (¬LEM ∘ ∨E₁)

contraposition : (A → B) → (¬ B → ¬ A)
contraposition f =  _∘ f

-- what about the other direction?
```
[Ende der Vorlesung am 30.04.2026]


## Stdlib

```
import Relation.Binary.PropositionalEquality using (_≗_) -- pointwise equality
import Relation.Binary using (Decidable) -- Decidable₂
import Relation.Nullary.Decidable using (Dec; map′)
import Function.Base using (case_of_)
import Function.Bundles using (Injection; _↣_; mk↣)
import Relation.Nullary.Negation using (contraposition)
import Data.Sum using (_⊎_) -- disjunction
```

Weitere Referenzen:

* Aktuelles aus der Forschung zu Entscheidbarkeit, Semi-Entscheidbarkeit, etc: de Jong, Kraus, Mohammadzadeh, Forsberg: [Generalized Decidability via Brouwer Trees](https://arxiv.org/abs/2602.10844)