6
$\begingroup$

Markov's principle is a statement of constructive arithmetic that allows classical reasoning on formulas of the shape $\exists x P$ when $P$ is a recursive predicate: $\neg \neg \exists x P \to \exists x P$

Its formulation is well known in the context of arithmetic, and it is well known that adding it to Heyting Arithmetic gives rise to a constructive system: when $A \lor B$ is provable, either $A$ is provable or $B$ is provable; when $\exists x \, A(x)$ is provable, there is a $t$ such that $A(t)$ is provable.

However I think it is not clear how one could formulate it in the context of pure intuitionistic first order logic (if it does make sense at all).

Various sources ([1], [2]) state it as "$\neg \neg \exists x P \to \exists x P$ for $P$ $\forall, \to$-free". Another tempting formulation would be $\forall x (P \lor \neg P) \to \neg \neg \exists x P \to \exists x P$ for any propositional $P$. As far as I can see, these two formulations are not comparable. Both these axioms, though, share the property that if we add them to pure intuitionistic first order logic we still obtain a constructive system (this is proved in [1] for the first axiom; I couldn't find references for the second axiom, but a proof can be obtained with a very similar argument).

Is there a more general analog of Markov's rule for first-order logic which preserves the disjunction property and other proof-theoretic properties of constructive systems? Or alternatively, is there some other source justifying the choice of the formalization used in [1,2] for Markov's principle?

[1] H. Herbelin, An intuitionistic logic that proves Markov's principle https://hal.inria.fr/inria-00481815/ [2] U. Berger, A Computational Interpretation of Open Induction http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=1319627

$\endgroup$
  • $\begingroup$ "Here are two non-arithmetic analogs of the arithmetic Markov's principle; which if either deserves the title of 'Markov's principle for first-order logic'?" Is that all you're asking, or do you want more than justification for a name? $\endgroup$ – Matt F. Nov 30 '16 at 17:37
  • $\begingroup$ @MattF. Yes, that's what I am asking. However having two uncomparable principles makes me think that there should be a more general form, and that neither of the two should be really acceptable. $\endgroup$ – Matteo Dec 1 '16 at 13:58
  • $\begingroup$ So I would revise the question by 1) reminding people that the disjunction property means "when $A \vee B$ is provable, then $A$ is provable or $B$ is provable", and 2) asking: "What is the most general analog of Markov's rule for first-order logic which preserves the disjunction property and other proof-theoretic properties of constructive systems?" $\endgroup$ – Matt F. Dec 1 '16 at 16:54
  • $\begingroup$ @MattF. Thank you for the suggestion, I tried to improve the question accordingly $\endgroup$ – Matteo Dec 2 '16 at 13:57
  • $\begingroup$ Can you give an idea how you prove admissibility of the second scheme? I also think it helps if you specify even more. Two variants of your question: 1)Is there a more general class MR of first-order propositions, such that for a constructive first-order theory T (with disjunction and existence property) and a P(x) in MR: if T proves $\neg\neg\exists$x[P(x)], then T proves $\exists$xP(x)? 2)Is there such a class MR that when added to intuitionistic first-order logic as axioms, preserves the constructivity of any constructive theory T? To me 1) and 2) are not equivalent. $\endgroup$ – Frank Waaldijk Dec 3 '16 at 8:59
4
$\begingroup$

This is not an answer to the question, but rather a comment which benefits from proper formatting.

For me personally, Markov's principle is specifically associated with the natural numbers and not with some other set. By that I mean that I don't think of $$ \neg\neg \exists x \in X{:}\ P(x) \quad\Longrightarrow\quad \exists x \in X{:}\ P(x) $$ (with $P$ restricted in some form, as you detailed) as a reasonable constructive principle, if $X$ is some arbitrary set.

Recall that there is a concrete reason why some schools of constructive mathematics accept Markov's principle: consider the algorithmic interpretation. The property $P$ is such that we can test in some finite way, for any natural number $n$, whether $P(n)$ holds or not. The assumption that $\neg\neg\exists n \in \mathbb{N}{:}\ P(n)$ means that there is some number $n$ such that $P(n)$ holds, but we do not know such a number (we are not given a witness of the existential statement). But we can find such a number on our own, thereby providing a witness of the statement $\exists n \in \mathbb{N}{:}\ P(n)$, by checking $P(0)$, $P(1)$, $P(2)$, and so on. This algorithm terminates (but we couldn't provide an upper bound for its runtime).

For an arbitrary set $X$ in place of $\mathbb{N}$, no analogous approach is possible. Therefore I can't quite fathom what you're driving at. (Markov's principle certainly works for some relatives of $\mathbb{N}$, for instance $\mathbb{N}^2$, which we can too search in a sequential manner.)

$\endgroup$
  • $\begingroup$ I understand your point, and indeed I have no doubts about the state of Markov's principle as a statement of arithmetic, or other similar/related theories. However, as noted in the first paper I cite in the question, one can also state constructivity results about a pure first order system, extended with some restricted form of the double negation elimination (by constructive I mean that one can have provable witnesses for existential statements). [1] actually calls this "Markov's principle", while I provide a similar statement which is also constructive, hence my question. $\endgroup$ – Matteo Nov 30 '16 at 13:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.