Deciding property for enumerable set

[uzytkownik]

If we can prove ¬ ((n : ℕ) → ¬ P n) for some decidable property P we can get ∃ P

{-# TERMINATING #-}
enumerable : ∀ {p} {P : Pred ℕ p} → Decidable {A = ℕ} P  → ¬ ((n : ℕ) → ¬ P n) → ∃ P
enumerable {P = P} dec f with dec zero
... | yes p[zero] = zero , p[zero]
... | no  ¬p[zero] with enumerable {P = P ∘ suc} (dec ∘ suc) λ n→P[1+n] → f λ {zero → ¬p[zero]; (suc n) → n→P[1+n] n}
...  | n , p[n] = suc n , p[n]

The question becomes if this function terminates:

• According to rules of classical logic it does
• According to rules of intuitionistic logic it is unprovable that it does terminate from what I understand

This property is much weaker than double negation axiom:

• It works only for enumerable sets
• It works only for decidable properties
• It is however 'safer' than double negation in agda as value is not a ⊥

[MatthewDaggitt]

What exactly is your question or your proposal? :smile:

[gallais]

Related idea: Coq's constructive epsilon module.

[uzytkownik]

@MatthewDaggitt

I guess question:

• Should this be in agda?
• If yes where it should be?
• If yes how should it be named?

[MatthewDaggitt]

In theory I have no objections to it. The usual approach is to put the type definition in Axiom.X where X is the name of the axiom that you would like to add to the system. You can then take the axiom in as an assumption to a particular proof in the library and hence remain --safe.

As for the name, I'm sure there's probably an official one somewhere which I'd advocate using. Otherwise I might be tempted to go with something like the super-catchy CountableDecidableExistential? Another question is would we want the type to be over naturals or over any type that is Countable? The latter definition doesn't yet exist in the library...

[gallais]

It's called Markov's Principle