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? 😄

[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

[jamesmckinna]

Is it --safe to add an Axiom (qua definition...) which depends on the {-# TERMINATING ... #-} pragma?

[gallais]

Axioms are never safe

[jamesmckinna]

Axioms are never safe

Well... yes, but the stdlib approach to 'axiom's is (usually) pure Searleian 'if-then-ism'. What makes this one different is the use of (external) appeal to the termination checker to justify a definition. The question was a technical one about whether the use of {-# TERMINATING #-} is compatible with --safe. But my instinct tells me it can't be?

[gallais]

My reponse was purely technical: it cannot be accepted by --safe.

That being said, I am more than happy to have it in the stdlib (together with its properties).

[jamesmckinna]

My reponse was purely technical: it cannot be accepted by --safe.

🎉 thanks!

[jamesmckinna]

That being said, I am more than happy to have it in the stdlib (together with its properties).

So, could we imagine an 'if-then-ism' factorisation, with Axiom.MarkovPrinciple stating the property, and its consequence (which would be --safe?), and an unsafe implementation using the {-# TERMINATING #-} proof given above?