If not rational implies irrational, then <some constructive taboo>

[jkingdon]

My conjecture is:

|- (  A. x e. ( RR \ QQ ) A. q e. QQ x =//= q  -> _om e. Markov )

To be honest I don't remember what I read which made me think the antecedent here implies a taboo, or that Markov's principle (maybe analytic?) might be the right taboo. Perhaps I was going on nothing more than https://us.metamath.org/ileuni/neapmkv.html or perhaps I read something suggestive.

Background:

• https://ncatlab.org/nlab/show/irrational+number which uses "weakly irrational" for x e. ( RR \ QQ ) and "strongly irrational" for A. q e. QQ x =//= q
• https://en.wikipedia.org/wiki/Irrational_number#In_constructive_mathematics although this doesn't go beyond the basic definition

[digama0]

Suppose that every non-rational is apart from every rational. Let $f:\omega\to 2$ such that $\neg\forall n, f(n)=1$. Define $x=\sup\left\{\sqrt{2}/n\mid n\mid f(n)=0\right\}$. Suppose $x$ is rational, and consider some $n$. If $f(n)=0$ then we can take $m$ to be the minimum value such that $f(m)=0$, and then $x=\sqrt{2}/m$ which is a contradiction. Therefore, $\forall n, f(n)=1$, which is also a contradiction. Thus $x$ is not rational, so by the assumption $x$ is apart from every rational, so since $x\ge 0$ we also have $x&gt;0$. So $x&gt;\sqrt{2}/n$ for some $n$, and $f(m)=0$ for some $m\le n$. Thus $\omega\in\mbox{Markov}$.

[jkingdon]

Sorry I'm having trouble following this especially the following notation:

Define $x=\sup\left\{\sqrt{2}/n\mid n\mid f(n)=0\right\}$.

I might have some follow up questions about things like showing the supremum exists and decidability of various propositions involved, but I'm having trouble even figuring out what to look into until I get the definition of x clear (iset.mm notation would be one way to be clear, in case it is unclear why I'm having trouble).

[benjub]

$x=\sup\left\{\sqrt{2}/n\mid n\mid f(n)=0\right\}$

It may be easier to add zero to the set on the right, to make sure it is always inhabited, and not merely nonempty. For explicitness, define

A = ( { 0 } u. { x e. RR | E. n e. ( _om \ (/) ) ( ( f ` n ) = 0 /\ x = ( ( sqrt ` 2 ) / n ) ) }

(well... as an argument of f, n is considered a natural number ordinal, but in the denominator, it is considered a natural number, so you'll need to use the canonical injection of _om into NN0). Then, you define x = sup ( A , RR , < ).

Then, you need https://us.metamath.org/ileuni/ax-pre-suploc.html

To prove that the set $A$ is located, note that if $a &lt; b$ are given, then you need to compute $f(n)$ for only a finite number of values of $n$ to know if $b$ is an upper bound of $A$ or $a$ is not an upper bound of $A$. That part may be long and tedious to formalize... (edit: well, I'm not even sure now... I'll check that tomorrow.)

[digama0]

Sorry I'm having trouble following this especially the following notation:

Define $x=\sup\left\{\sqrt{2}/n\mid n\mid f(n)=0\right\}$.

The intended interpretation of that expression is "the set of values $\sqrt{2}/n$, taken over all $n\in\mathbb{N}$ such that $f(n)=0$". Sometimes people write such a set without the central $\mid n\mid$ part, although in that case it is ambiguous what the bound variable is. Written as an explicit metamath-style set builder it is $\{z\mid \exists n, (f(n)=1\wedge z=\sqrt{2}/n)\}$, as @benjub says.

@benjub is absolutely right though that you should also throw $0$ into the set, the idea is that $x$ is equal to $0$ iff all of the $f(n)$'s are 1.

You don't need to use ax-pre-suploc to prove this x exists, you can also use ax-caucvg because it is the limit of the cauchy sequence $x_k=\sup(\{0\}\cup\{\sqrt{2}/n\mid n\mid n&lt;k\wedge f(n)=0\})$. I was hoping there was just a general theorem establishing the existence of limits, sums and suprema, I don't think the side conditions here should be hard.

You can prove the set is located though as follows: Let $x=\sup S$ where $S=(\{0\}\cup\{\sqrt{2}/n\mid n\mid f(n)=0\})$ is the set in question. Suppose $a&lt;b$. If $a&lt;0$, then $0\in S$ is an element of the set above $a$. If $0&lt;b$, then $\sqrt{2}/n&lt;b$ for some $n$, and it is decidable whether $\exists m&lt;n,f(m)=0$.

• If true, take the minimum $m&lt;n$ with $f(m)=0$.
  • If $a&lt;\sqrt{2}/m$ then $a$ is below an element of $S$
  • If $\sqrt{2}/m&lt;b$ then $b$ is an upper bound of $S$.
• Otherwise, $b&gt;\sqrt{2}/n$ is an upper bound of $S$.

[jkingdon]

The intended interpretation of that expression is "the set of values sqrt(2) / n , taken over all n ∈ N such that f ( n ) = 0 "

Ah, thanks. I figured it must be something like that but I don't know whether I've this this exact variation before.

I was hoping there was just a general theorem establishing the existence of limits, sums and suprema, I don't think the side conditions here should be hard.

Hmm, not sure what kind of generality you have in mind but a few that we have are:

• https://us.metamath.org/ileuni/cvg1n.html
• https://us.metamath.org/ileuni/cvgcmp2n.html
• https://us.metamath.org/ileuni/dedekindeu.html
• https://us.metamath.org/ileuni/suplociccreex.html
• https://us.metamath.org/ileuni/infssuzcldc.html
• https://us.metamath.org/ileuni/nnmindc.html

Most of these are for situations which are different from what we need for this proof, though. I have been operating under the assumption that we'll need a whole family of these for different kinds of side conditions.

[benjub]

By the way: I have added a few weeks ago the construct { A | x | ph } to set.mm. I recall that @digama0 had already proposed something like that / exactly that some time ago. See https://us.metamath.org/mpeuni/df-bj-gab.html.

In the associated PR (#4272) I pinged you because the new construct was messing up the metamath swiss-knife parser. I eventually used new tokens {{ and }} but it may still be worth having a full LALR parser.

[digama0]

@jkingdon I think the easiest proof might be the one using cvg1n, since it is the limit of a natural cauchy sequence, where $x_k$ is 0 until the first f(n) = 0 and then $\sqrt{2}/n$ thereafter.