Are there propositions that can be proved in classical logic but not in Agda

Question

Unless I'm mistaken, there is no proof for

∀ {A : Set} → ¬ (¬ A) → A

in Agda.

This means you cannot use proofs by contradiction.

Many Maths textbooks use those kinds of proofs, so I was wondering: is it always possible to find an alternative constructive proof? Could you write, e.g., an Algebra textbook using only constructive logic?

In case the answer is no. Does this mean constructive logic is in some sense less powerful then classical logic?

Answer 1

Indeed, double negation elimination (and other statements which are logically equivalent to that) cannot be proven in Agda.

-- Law of excluded middle
lem : ∀ {p} {P : Set p} → P ⊎ ¬ P

-- Double negation elimination
dne : ∀ {p} {P : Set p} → ¬ ¬ P → P

-- Peirce's law
peirce : ∀ {p q} {P : Set p} {Q : Set q} →
  ((P → Q) → P) → P

(If you want, you can show that these are indeed logically equivalent, it's an interesting exercise). But this is a consequence we cannot avoid - one of the important things about constructive logic is that proofs have a computational context. However, assuming law of excluded middle basically kills any computational context.

Consider for example the following proposition:

end-state? : Turing → Set
end-state? t = ...

simulate_for_steps : Turing → ℕ → Turing
simulate t for n steps = ...

Terminates : Turing → Set
Terminates machine = Σ ℕ λ n →
  end-state? (simulate machine for n steps)

So, a Turing machine terminates if there exists a number n such that after n steps, the machine is in an end state. Sounds reasonable, right? What happens when we add excluded middle in the mix?

terminates? : Turing → Bool
terminates? t with lem {P = Terminates t}
... | inj₁ _ = true
... | inj₂ _ = false

If we have excluded middle, then any proposition is decidable. Which also means that we can decide whether a Turing machine terminates or not and we've solved the halting problem. So we can either have computability or classical logic, but not both! While excluded middle and other equivalent statements help us with proofs, it comes at the cost of computational meaning of the program.

---

So yes, in this sense, constructive logic is less powerful than classical. However, we can simulate classical logic via double negation translation. Notice that doubly negated versions of the previous principles hold in Agda:

¬¬dne : ∀ {p} {P : Set p} → ¬ ¬ (¬ ¬ P → P)
¬¬dne f = f λ g → ⊥-elim (g (f ∘ const))

¬¬lem : ∀ {p} {P : Set p} → ¬ ¬ (P ⊎ ¬ P)
¬¬lem f = f (inj₂ (f ∘ inj₁))

If we were in classical logic, you would then use double negation elimination to get the original statements. There's even a monad dedicated to this transformation, take a look at the double negation monad in the Relation.Nullary.Negation module (in the standard library).

What this means is that we can selectively use the classical logic. From certain point of view, constructive logic is more powerful than classical precisely because of this. In classical logic, you cannot opt out of these statements, they just are there. On the other hand, constructive logic doesn't force you to use these, but if you need them, you can "enable" them in this way.

---

Another statement which cannot be proven in Agda is function extensionality. But unlike with classical statements, this one is desirable in constructive logics.

ext : ∀ {a b} {A : Set a} {B : A → Set b}
  (f g : ∀ x → B x) → (∀ x → f x ≡ g x) → f ≡ g

However, this doesn't mean that it doesn't hold in constructive logic. It's just a property of the theory on which Agda is based (which is mostly intensional type theory with axiom K), there are other flavors of type theory where this statement holds, for example the usual formulations of extensional type theory or Conor McBride's and Thorsten Altenkirch's observational type theory.