Constructive Analysis

Fengyang Wang

UW Student Seminars

November 1, 2017

(Revised post-talk to correct typos)

Theorem 1

(Formal-ish Statement)
There exist $\{a, b\} ⊆ \mathbf{R}^+ - \mathbf{Q}^+$ such that $a^b ∈ \mathbf{Q}^+$.

(English Language Statement)
An irrational number to an irrational power may be rational.

Proof 1A of Theorem 1

If $\sqrt{2}^\sqrt{2}$ is rational, let $a=b=\sqrt{2}$ ∎

Otherwise, let $a=\sqrt{2}^\sqrt{2}$ and $b=\sqrt{2}$. Then $a^b = {\left(\sqrt{2}^\sqrt{2}\right)}^{\sqrt{2}} = \sqrt{2}^2 = 2$ ∎

Proof 1B of Theorem 1

Let $a = \sqrt{2}$ and $b = \frac{\log{9}}{\log{2}}$.

Then $a^b = \sqrt{2}^{\frac{\log{9}}{\log{2}}} = \sqrt{2^{\frac{\log{9}}{\log{2}}}} = \sqrt{9} = 3$ ∎

Attempted Implementation of Proof 1A

In [2]:
if (2) ^ (2)  𝐐
    a = 2
    b = 2
else
    a = 2
    b = (2) ^ (2)
end
You didn’t tell me how to figure out whether (√2) ^ (√2) ∈ 𝐐...

Stacktrace:
 [1] in(::𝐑, ::Type{𝐐}) at ./In[1]:4

Brouwer-Heyting-Kolmogorov interpretation

  • A proof of $a ∧ b$ is a proof of $a$ and a proof of $b$
  • A proof of $a ∨ b$ is a proof of $a$ or a proof of $b$

Beware!
In classical logic, a proof of $a ∨ b$ could be neither a proof of $a$ nor a proof of $b$. In BHK intuitionistic logic, you must know which one you are proving!

Brouwer-Heyting-Kolmogorov interpretation

  • A proof of $∀ x P(x)$ is an algorithm that given any $x$, creates a proof of $P(x)$
  • A proof of $∃ x P(x)$ is a witness $x$ and a proof of $P(x)$

Beware!
In classical logic, a proof of $∃ x P(x)$ might not have a witness.

Brouwer-Heyting-Kolmogorov interpretation

  • A proof of $a ⇒ b$ is an algorithm that given a proof of $a$ creates a proof of $b$
  • A proof of $¬a$ is an algorithm that given a proof of $a$ creates a contradiction

Beware!
In the BHK interpretation, $¬¬a$ is not the same as $a$.

Limited Principle of Omniscience (LPO)

(Formal-ish Statement)
$$ ∀𝐱∈\{0, 1\}^𝐍 (𝐱 = 𝟎 ∨ 𝐱 ≠ 𝟎) $$

(English Language Statement)
An infinitely tall haystack has no needles or it has a needle.

Lesser Limited Principle of Omniscience (LLPO)

(Formal-ish Statement)
$$ ∀𝐱∈\{0, 1\}^𝐍 (¬∃i∈𝐍,j∈𝐍(i≠j ∧ x_i = y_i = 1) ⇒ (∀i∈𝐍(x_{2i} = 0) ∨ ∀i∈𝐍(x_{2i-1} = 0))) $$

(English Language Statement)
Given two infinitely tall haystacks, if you know that there is at most one needle among them both, then either the left haystack has no needles or the right haystack has no needles.

Markov Principle (MP)

(Formal-ish Statement)
$$∀𝐱∈\{0, 1\}^𝐍 (¬(𝐱 = 𝟎) ⇒ 𝐱 ≠ 𝟎)$$

(English Language Statement)
If a haystack cannot have no needles, then it has a needle.

Brouwerian Counterexamples

  • For some $P$, suppose $P ⇒ (\mathsf{LEM} ∨ \mathsf{LPO} ∨ \mathsf{LLPO})$ or even $P ⇒ \mathsf{MP}$
  • This is evidence that $P$ cannot be proven constructively

Real Numbers

  • Time to construct the real numbers $\mathbf{R}$!
  • Each $\mathbf{x}\in\mathbf{R}$ is a set of rational intervals $(q, q') \in \mathbf{Q}^2$ such that:
    • $q \le q'$
    • $\forall (q, q') \in \mathbf{x}~(\forall (p, p') \in \mathbf{x}~(q \le p' \wedge p \le q'))$
    • $\forall \varepsilon\in\mathbf{Q}^+~ (\exists (q, q') \in \mathbf{x} ~(q' - q < \varepsilon))$

(English Language Statement)
A real number is a set of rational intervals such that any two intervals overlap, and there are intervals shorter than any given positive rational.

Equality

The equivalence relation of $\mathbf{R}$ is the natural one:

$\mathbf{x} = \mathbf{y}$ if each interval $(p, p') \in \mathbf{x}$ overlaps with each interval $(q, q') \in \mathbf{y}$

The Denial Inequality

  • In classical logic, $\lnot \lnot (x = y) \Leftrightarrow (x = y)$ for all $x$, $y$
  • Brouwerian Counterexample: Markov Principle
  • Hence the $\lnot (x = y)$ inequality is called the denial inequality, and is not often written $x \ne y$

Order

  • $\mathbf{x} < \mathbf{y}$ if there are intervals $(p, p') \in \mathbf{x}$ and $(q, q') \in \mathbf{y}$ that satisfy $p' < q$
  • $\mathbf{x} \le \mathbf{y}$ if all intervals $(p, p') \in \mathbf{x}$ and $(q, q') \in \mathbf{y}$ satisfy $p \le q'$
  • $\mathbf{x} > \mathbf{y}$ if there are intervals $(p, p') \in \mathbf{x}$ and $(q, q') \in \mathbf{y}$ that satisfy $p > q'$
  • $\mathbf{x} \ge \mathbf{y}$ if all intervals $(p, p') \in \mathbf{x}$ and $(q, q') \in \mathbf{y}$ satisfy $p' \ge q$

Decidability of Order

  • In classical logic, $\mathbf{x} \ge 0 \Rightarrow \mathbf{x} > 0 \vee \mathbf{x} = 0$ for all $\mathbf{x}$
  • Brouwerian Counterexample: Limited Principle of Omniscience
  • In classical logic, $\mathbf{x} \ge 0 \vee \mathbf{x} \le 0$ for all $\mathbf{x}$
  • Brouwerian Counterexample: Lesser Limited Principle of Omniscience

Convergence

$(\mathbf{x}_n) \in \mathbf{R}^\mathbf{N}$ converges to $\mathbf{x}$ if for all $\varepsilon > 0$ there exists $N\in\mathbf{N}$ after which any term $\mathbf{x}_n$ ($n \ge N$) is within $\varepsilon$ of $\mathbf{x}$

(We also write $\lim_{n\to\infty}\mathbf{x}_n = \mathbf{x}$)

$(\mathbf{x}_n) \in \mathbf{R}^\mathbf{N}$ is Cauchy if for all $\varepsilon > 0$ there exists $N\in\mathbf{N}$ after which any two terms $\mathbf{x}_n$, $\mathbf{x}_m$ ($n \ge m > N$) are within $\varepsilon$ of each other

Theorem 2

(Informal Statement)
If $(\mathbf{x}_n)\in\mathbf{R}^\mathbf{N}$ is Cauchy, then there is $\mathbf{x}_\infty$ such that $\lim_{n\to\infty}\mathbf{x}_n = \mathbf{x}_\infty$

(English Language Statement)
The real numbers are complete.

Lemma

(Informal Statement)
If $x > 0$, there exists a positive integer $n$ such that $x > 1/n$.

Proof:
Take a interval $(q, q') \in x$ that does not contain $0$. Take $n > 1/q$ (rational operations).

Proof of Theorem 2

Let $(\mathbf{x}_n)$ be a Cauchy sequence of real numbers.

Compute an integer function $k \mapsto n_k$ such that each $n_k$ satisfies for all $m\ge n_k$, $n\ge n_k$, $|\mathbf{x}_m - \mathbf{x}_n| < 2^{-k}$.

For each $k$, construct a sequence of intervals $(q_k, q'_k) \in \mathbf{x}_{n_k}$ such that $q'_k - q_k < 2^{-k}$.

Consider $r_k = q_k - 2^{-k}$, $r'_k = q'_k + 2^{-k}$. For all $n\ge n_k$, we have

$$ r_k \le \mathbf{x}_{n_k} - 2^{-k} < \mathbf{x}_n < \mathbf{x}_{n_k} + 2^{-k} \le r_k$$

So actually for all $j \ge k$

$$ \mathbf{x}_{n_j} \in [r_j, r'_j] \cap [r_k, r'_k]$$

So the real number $\mathbf{x}_\infty$ defined by $\{(r_k, r'_k) : k \ge 1\}$ is in fact a real number.

Proof of Theorem 2

From our construction, we have $\mathbf{x}_n \in [r_k, r'_k]$ for all $n \ge n_k$. That means that

$$ \forall k \forall n\ge n_k~(|\mathbf{x}_n - \mathbf{x}_\infty| \le r'_k - r_k < 2^{-k+2}) $$

By Lemma, we therefore have $\lim_{n\to\infty} \mathbf{x}_n = \mathbf{x}_\infty$.

It was proven by Cantor that a good math joke exists. Unfortunately, his proof was entirely non-constructive.

Jon