-
Notifications
You must be signed in to change notification settings - Fork 251
Open
Description
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 ⊥
Activity
MatthewDaggitt commentedon Dec 8, 2020
What exactly is your question or your proposal? 😄
gallais commentedon Dec 8, 2020
Related idea: Coq's constructive epsilon module.
uzytkownik commentedon Dec 9, 2020
@MatthewDaggitt
I guess question:
MatthewDaggitt commentedon Dec 9, 2020
In theory I have no objections to it. The usual approach is to put the type definition in
Axiom.X
whereX
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 isCountable
? The latter definition doesn't yet exist in the library...gallais commentedon Dec 9, 2020
It's called Markov's Principle
jamesmckinna commentedon Feb 6, 2025
Is it
--safe
to add anAxiom
(qua definition...) which depends on the{-# TERMINATING ... #-}
pragma?gallais commentedon Feb 7, 2025
Axioms are never safe
jamesmckinna commentedon Feb 7, 2025
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 commentedon Feb 7, 2025
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 commentedon Feb 7, 2025
🎉 thanks!
jamesmckinna commentedon Feb 7, 2025
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?