Timeline for True by accident (and therefore not amenable to proof)
Current License: CC BY-SA 4.0
5 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Aug 12, 2022 at 7:56 | history | edited | Martin Sleziak | CC BY-SA 4.0 |
http -> https (the question was bumped anyway)
|
Aug 25, 2011 at 12:39 | comment | added | François G. Dorais | You're absolutely right, I just fixed it. | |
Aug 25, 2011 at 12:33 | history | edited | François G. Dorais | CC BY-SA 3.0 |
changed rule to principle
|
Aug 25, 2011 at 12:22 | comment | added | Emil Jeřábek |
What you describe is not Markov’s rule, but Markov’s principle. Markov’s rule is the corresponding derivation rule which states that when $\neg\forall x\neg A(x)$ is provable, then $\exists x\,A(x)$ is provable (under appropriate conditions on $A$). All usual constructive theories (for example, Heyting arithmetic) are closed under this rule, even though they typically do not prove Markov’s principle. Therefore, even in constructive setting, it would suffice to prove that there is no counterexample in order to establish the conjecture.
|
|
Aug 25, 2011 at 12:12 | history | answered | François G. Dorais | CC BY-SA 3.0 |