Non-constructive but weaker than the law of excluded middle

lesser_non_constructive_princople.txt

This is the text accopaning the video here:

https://youtu.be/RusPpTVyNPw

# Notation
p ... Proposition
P ... Predicate

∃P      := ∃x. P(x)               # P satisfiable (here, constructively)
∀P      := ∀x. P(x)               # P always satisfied
DEC(P)  := ∀x. [P(x) ∨ ¬P(x)]     # P decidable

In this text we may assume x in N.

Then we may also express the principles in terms of decidable binary sequences,
using P(n) := a_n==0.
Then, due to a_n being decidable, ¬(a_n==0) means a_n==1.

More abstract now, below we'll use P, Q and R as predicate variables. So
forall P. ...
may be taken to be a scheme.

# Implications of having a counterexample
∃(¬P) ⇒ ¬∀P
∃x. ¬P(x) ⇒ ¬(∀x. P(x))

Clear, as ∃(¬P) and ∀P is contradictory.

# Markov's Rule
DEC(P), ¬¬∃P  |-  ∃P

Double negation as a rule for existential claims.
(Admissable in intuitionistic theories)
Embodies principle of unbounded search that terminates.

Questions:
Does rejection of impossibility of a satisfied case
always give an / lead to / come from a concrete example?

# Statement of LPO
forall P. DEC(P) ⇒
∃P ∨ ¬∃P

Questions:
If we positively decides a particular case in a search, then ∃P is clear.
But otherwise (no search becomes practical positive, even if all are decided),
what are means of proving absurdity of existence?
What would be mathematical principle upon which _we_ may judge ∃P impossible,
as we find no practical search is positive?
Infinite-time Turing machine (infinite search) would do the trick for any P with DEC(P).
What are conditions on the form of P and the framework to constructively
validate cases of LPO?

Notes:
The LPO + disjunctive syllogism then gives us Markov's rule:
∃P ∨ ¬∃P, ¬(¬∃P)  |-  ∃P.

# Discussion
# Statement of WLPO
forall P. DEC(P) ⇒
∀P ∨ ¬∀P

Questions:
As discussed, finding a counter-example makes us reject ∀P, i.e. shows ¬∀P.
But what are ways in which confirmations of ∀P can come about?
But what structural condition on a decidable property P (or sequence definition)
makes us see that it is a necessity _for all_ n.
Infinite-time Turing machine remark above applies here too.

# Statement of LLPO
forall P. forall Q. DEC(P) ⇒ DEC(Q) ⇒
¬(∃P ∧ ∃Q) ⇒ (¬∃P ∨ ¬∃Q)

Notes:
¬(∃P ∧ ∃Q) ... "_at most_ one of the properties P and Q can be satisfied."

A variant of LLPO endings in ... ⇒ (∀(¬P) ∨ ∀(¬Q))
and is, at least when we have Markov's principle, provably equivalent to it.

Question:
What are ways in which knowledge of joint propositions could arise that can't
be taken apart in knowledge of the separate cases?

Notes:
A variant of LLPO endings in ... ⇒ ¬∀¬P ⇒ ∃P
This is simpler to read: Us knowing that there's some x for which ¬P doesn't
apply makes said x to a candidate for P.

# Statement MP (Markov principle)
forall P. DEC(P) ⇒
¬∀P ⇒ ∃(¬P)

Questions:
What's the nature of a proof of ¬∀P?
Does having a rejections of ∀P always mean we have a concrete counterexample?
Would this principle, given other assumptions that give us ∀P in another way,
sneak in non-constructivism?

# Weak Markov's Rule
Something something finding satisfied cases via rejecting simultanous
impossibilities of predicates.

A classical reading in analysis would be something like
"Any real p which is bigger than any other real q - except those q that are
  strictly positive - is strictly positive."

## Thoughts
For one or more P's, it may not be necessary at all to adopt some principles
of the form
∃x. P(x) ⇒ R
when, in the given framework, all those instances are provable anyway.
LLPO and MP are of this form.

# References
https://arxiv.org/abs/1804.05495

https://en.wikipedia.org/wiki/Universal_quantification
https://en.wikipedia.org/wiki/Existential_quantification

https://ncatlab.org/nlab/show/principle+of+omniscience
https://ncatlab.org/nlab/show/Markov%27s+principle

https://en.wikipedia.org/wiki/Limited_principle_of_omniscience
https://en.wikipedia.org/wiki/Markov%27s_principle
https://en.wikipedia.org/wiki/Disjunctive_syllogism
https://en.wikipedia.org/wiki/List_of_undecidable_problems
https://en.wikipedia.org/wiki/Church%27s_thesis_(constructive_mathematics)