```
open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
open import Lang.dataStructures using (
; true; false;
Bool; List;
ℕ; two; three; four; five; six; seven; eight; nine; ten; zero; succ;
one_::_; [])
open import Logic.logicBasics using (
; ⊤; ⟂-elim; ¬;
⟂; contradiction; contrapos;
not_then_else_)
open import Types.relations using (Rel; REL)
open import Types.equality using (_≡_)
module Logic.decidability where
```

Relations can de defined either as an inductive data type − the existence of the type implies that the relation
exists. We say that the data type provides a **witness** that the relation is valid. The other way is to
define relations as functions that compute whether the relation holds.

Consider the relation `_<=_`

. If we have to prove that `2 <= 4`

, we can do that in two
ways:

The Inductive relation:

```
data _<=_ : ℕ → ℕ → Set where
: {n : ℕ} → zero <= n
ltz : {m : ℕ} → {n : ℕ} → m <= n → (succ m) <= (succ n) lt
```

Proof that 2 ≤ 4:

```
: two <= four
2≤4 = lt (lt ltz) 2≤4
```

Relation as a Function type:

```
infix 4 _≤_
_≤_ : ℕ → ℕ → Bool
= true
zero ≤ n = false
succ m ≤ zero = m ≤ n succ m ≤ succ n
```

Proof that 2 ≤ 4:

```
open import Types.equational
open ≡-Reasoning
: (two ≤ four) ≡ true
twoLessThanFour = begin
twoLessThanFour
two ≤ four
≡⟨⟩
one ≤ three
≡⟨⟩
zero ≤ two
≡⟨⟩
true ∎
```

We can always connect such forms of representation of the same underlying mathematical structures from the Computation based to evidence based:

```
: Bool → Set
T = ⊤
T true = ⟂ T false
```

Like we saw for the proposition `2 ≤ 4`

, for any proposition `P`

to be decidable, either we can
compute `P`

or `¬ P`

, i.e. either proposition `P`

has a proof or it can been disproved.
In the words of logic, a true/false decision problem is decidable if there exists an effective method for deriving the
correct answer.

For representing this idea we use an inductive data type which has two constructors.

```
data Dec {p} (P : Set p) : Set p where
: ( p : P) → Dec P
yes : (¬p : ¬ P) → Dec P no
```

The computational equivalent of decidable relations would be:

```
: ∀ {a b ℓ} {A : Set a} {B : Set b} → REL A B ℓ → Set _
Decidable _∼_ = ∀ x y → Dec (x ∼ y) Decidable
```

Decidability can be computed into a boolean value. We write that and some other useful machinery:

```
_⌋ : ∀ {p} {P : Set p} → Dec P → Bool
⌊_ ⌋ = true
⌊ yes _ ⌋ = false ⌊ no
```

```
: ∀ {p} {P : Set p} → Dec P → Set
True = T ⌊ Q ⌋ True Q
```

```
: ∀ {p} {P : Set p} → Dec P → Set
False = T (not ⌊ Q ⌋) False Q
```

```
record Lift {a} ℓ (A : Set a) : Set (a ⊔ ℓ) where
constructor lift
field lower : A
module _ {p} {P : Set p} where
: Dec P → Set p
From-yes (yes _) = P
From-yes (no _) = Lift p ⊤ From-yes
```

We can now use this machinery to prove that the relation `<=`

is decidable for all
`x, y ∈ ℕ`

:

```
: ∀ {x : ℕ} → ¬ (succ x <= zero)
nothingIsLessThanZero ()
nothingIsLessThanZero
: ∀ {x y : ℕ} → ¬ (x <= y) → ¬ (succ x <= succ y)
successionsAreLessToo (lt x≤y) = ¬x≤y x≤y
successionsAreLessToo ¬x≤y
_≤isDecidable_ : ∀ (m n : ℕ) → Dec (m <= n)
= yes ltz
zero ≤isDecidable n = no nothingIsLessThanZero
succ m ≤isDecidable zero with m ≤isDecidable n
succ m ≤isDecidable succ n ... | yes m≤n = yes (lt m≤n)
... | no ¬m≤n = no (successionsAreLessToo ¬m≤n)
```

We have used the `with`

abstraction above. It lets you pattern match on the result of an intermediate
computation by effectively adding an extra argument to the left-hand side of your function. Refer to more documentation
here.

A theory is a set of formulas, often assumed to be closed under logical consequence. Decidability for a theory concerns whether there is an effective procedure that decides whether the formula is a member of the theory or not, given an arbitrary formula in the signature of the theory. The problem of decidability arises naturally when a theory is defined as the set of logical consequences of a fixed set of axioms.

Every consistent theory is decidable, as every formula of the theory will be a logical consequence of, and thus a member of, the theory. First-order logic is not decidable in general; in particular, the set of logical validities in any signature that includes equality and at least one other predicate with two or more arguments is not decidable. Logical systems extending first-order logic, such as second-order logic and type theory, are also undecidable.

Decidability and undecidability of an entire theory can be proven, one of the more famous proofs being Gödel’s incompleteness theorems. The machinery we defined here form the basis of a larger set of structures required to prove the above facts, including problems like prime number generation. In light of the complexity associated with such a task, we choose to move on instead.