agda
Deciding property for enumerable set
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
I guess question:
- Should this be in agda?
- If yes where it should be?
- If yes how should it be named?
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...
Is it --safe to add an Axiom (qua definition...) which depends on the {-# TERMINATING ... #-} pragma?
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?
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).
My reponse was purely technical: it cannot be accepted by
--safe.
🎉 thanks!
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?