/sci/ - Science & Math

>>11772089
It's about how strict you interpret "[math] \exists x [/math]".

Example: Let [math] O(T, X) [/math] be the basic predicate that says that T is an total ordering relation on the set X.
The set theory ZFC proves (mostly via axiom of choice) that all sets can be ordered, and in particular it proves
[math] \exists t. \, O(t, {\mathbb R} ) [/math]
But that's icky, since it's also provable that we can't describe an ordering on [math] {\mathbb R} [/math].

That's an extremely non-constructive theory in that sense, the existence [math] \exists x [/math] in this theory is super weak.

There's those at least 3 schools of conservatism in mathematical logic for mathematics, distinguished by what they still allow to be valid principles of inference. (Most of their principle will be valid in classical math.)

E.g. the Russian school of Markov Jr. (the son), adopts the arguably non-constructive Markov's principle
https://en.wikipedia.org/wiki/Markov%27s_principle
for decidable predicates of numbers:
If
[math] \forall n. \ P(n)\lor \neg P(n) [/math],
then
[math] \neg \forall n\, \neg P(n) \implies \exists m\, P(m) [/math]

In words:
>For decidable P, if it's not the case that for all n in N, we have that P(n) is false, then there exists an m such that P(m) is true.

I.e. if you know P(n) can be evaluated (to true of false) for any n, and if you know - by whatever means - that there has to be an example m, then (even if you don't know it), the math and logic is such that you're allowed to conclude [math] \exists m\, P(m) [/math].

The idea behind allowing this, is that if you got a decidable (i.e. computable) predicate over the (inductive) set of natural numbers, then you know that in principle you can turn on a computer and run through all n till you find m. Markov's principle is a promise principle in that sense.

Pic related are properties that would be nice to have of a theory T (but something like ZF if far away from having those)