Skip to main content
deleted 506 characters in body
Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

You make an erroneous assumption in your question, as already in dimension 1 you need LLPO to know that the maximum is actually attained at some point.

We work constructively.

Theorem: IfLLPO is equivalent to the statement that every affine map $[0,1] \to \mathbb{R}$ attains its maximum then LLPO shows.

Proof. The general form of an affine map on $[0,1]$ is $f_{a,b}(x) = a \cdot (1 - x) + b \cdot x$. Suppose then that for every such $f_{a,b}$ there exists $x_0 \in [0,1]$ such that $f_{a,b}(x) \leq f_{a,b}(x_0)$ for all $x \in [0,1]$.

NoteLet us first show that LLPO implies attainment of maximum. Given any $f_{a,b}$, by LLPO either $a \leq b$ or $b \leq a$:

  • If $a \leq b$ then the maximum of $f_{a,b}$ is attained at $x_0 = 1$.
  • If $b \leq a$ then the maximum of $f_{a,b}$ is attained at $x_0 = 0$.

The converse is more interesting. First note that the following holds: if $f_{a,b}(0) \leq f_{a,b}(t)$ for some $t > 0$ then $f_{a,b}(0) \leq f_{a,b}(1)$. Similarly, if $f_{a,b}(t) \geq f_{a,b}(1)$ for some $t < 1$ then $f_{a,b}(0) \geq f_{a,b}(1)$.

Consider any two reals $a, b \in \mathbb{R}$. We shall decide $a \leq b \lor b \leq a$, which implies LLPO. By assumption, the map $f_{a,b}$ attains its maximum at some $x_0 \in [0,1]$. Either $x_0 < 2/3$ or $x_0 > 1/3$:

  • If $x_0 > 1/3$ then from $f(0) \leq f(x_0)$ it follows that $a = f(0) \leq f(1) = b$.
  • If $x_0 < 2/3$ then from $f(x_0) \geq f(1)$ it follows that $a = f(0) \geq f(1) = b$. $\Box$

Of course, since affine maps are very simple, the maximal value of $f_{a,b}$ exists, but the above argument shows it takes LLPO to know where it is attained.

You make an erroneous assumption in your question, as already in dimension 1 you need LLPO to know that the maximum is actually attained at some point.

We work constructively.

Theorem: If every affine map $[0,1] \to \mathbb{R}$ attains its maximum then LLPO shows.

Proof. The general form of an affine map on $[0,1]$ is $f_{a,b}(x) = a \cdot (1 - x) + b \cdot x$. Suppose then that for every such $f_{a,b}$ there exists $x_0 \in [0,1]$ such that $f_{a,b}(x) \leq f_{a,b}(x_0)$ for all $x \in [0,1]$.

Note that the following holds: if $f_{a,b}(0) \leq f_{a,b}(t)$ for some $t > 0$ then $f_{a,b}(0) \leq f_{a,b}(1)$. Similarly, if $f_{a,b}(t) \geq f_{a,b}(1)$ for some $t < 1$ then $f_{a,b}(0) \geq f_{a,b}(1)$.

Consider any two reals $a, b \in \mathbb{R}$. We shall decide $a \leq b \lor b \leq a$, which implies LLPO. By assumption, the map $f_{a,b}$ attains its maximum at some $x_0 \in [0,1]$. Either $x_0 < 2/3$ or $x_0 > 1/3$:

  • If $x_0 > 1/3$ then from $f(0) \leq f(x_0)$ it follows that $a = f(0) \leq f(1) = b$.
  • If $x_0 < 2/3$ then from $f(x_0) \geq f(1)$ it follows that $a = f(0) \geq f(1) = b$. $\Box$

Of course, since affine maps are very simple, the maximal value of $f_{a,b}$ exists, but the above argument shows it takes LLPO to know where it is attained.

You make an erroneous assumption in your question, as already in dimension 1 you need LLPO to know that the maximum is actually attained at some point.

We work constructively.

Theorem: LLPO is equivalent to the statement that every affine map $[0,1] \to \mathbb{R}$ attains its maximum

Proof. The general form of an affine map on $[0,1]$ is $f_{a,b}(x) = a \cdot (1 - x) + b \cdot x$. Suppose then that for every such $f_{a,b}$ there exists $x_0 \in [0,1]$ such that $f_{a,b}(x) \leq f_{a,b}(x_0)$ for all $x \in [0,1]$.

Let us first show that LLPO implies attainment of maximum. Given any $f_{a,b}$, by LLPO either $a \leq b$ or $b \leq a$:

  • If $a \leq b$ then the maximum of $f_{a,b}$ is attained at $x_0 = 1$.
  • If $b \leq a$ then the maximum of $f_{a,b}$ is attained at $x_0 = 0$.

The converse is more interesting. First note that the following holds: if $f_{a,b}(0) \leq f_{a,b}(t)$ for some $t > 0$ then $f_{a,b}(0) \leq f_{a,b}(1)$. Similarly, if $f_{a,b}(t) \geq f_{a,b}(1)$ for some $t < 1$ then $f_{a,b}(0) \geq f_{a,b}(1)$.

Consider any two reals $a, b \in \mathbb{R}$. We shall decide $a \leq b \lor b \leq a$, which implies LLPO. By assumption, the map $f_{a,b}$ attains its maximum at some $x_0 \in [0,1]$. Either $x_0 < 2/3$ or $x_0 > 1/3$:

  • If $x_0 > 1/3$ then from $f(0) \leq f(x_0)$ it follows that $a = f(0) \leq f(1) = b$.
  • If $x_0 < 2/3$ then from $f(x_0) \geq f(1)$ it follows that $a = f(0) \geq f(1) = b$. $\Box$

Of course, since affine maps are very simple, the maximal value of $f_{a,b}$ exists, but the above argument shows it takes LLPO to know where it is attained.

deleted 506 characters in body
Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

You make an erroneous assumption in your question, as already in dimension 1 you need LLPO to know that the maximum is actually attained at some point.

We work constructively.

Theorem: If every affine map $[0,1] \to \mathbb{R}$ attains its maximum then LLPO shows.

Proof. The general form of an affine map on $[0,1]$ is $f_{a,b}(x) = a \cdot (1 - x) + b \cdot x$. Suppose then that for every such $f_{a,b}$ there exists $x_0 \in [0,1]$ such that $f_{a,b}(x) \leq f_{a,b}(x_0)$ for all $x \in [0,1]$.

Note that the following holds: if $f_{a,b}(0) \leq f_{a,b}(t)$ for some $t > 0$ then $f_{a,b}(0) \leq f_{a,b}(1)$. Similarly, if $f_{a,b}(t) \geq f_{a,b}(1)$ for some $t < 1$ then $f_{a,b}(0) \geq f_{a,b}(1)$.

Consider any two reals $a, b \in \mathbb{R}$. We shall decide $a \leq b \lor b \leq a$, which implies LLPO. By assumption, the map $f_{a,b}$ attains its maximum at some $x_0 \in [0,1]$. Either $x_0 < 2/3$ or $x_0 > 1/3$:

  • If $x_0 > 1/3$ then from $f(0) \leq f(x_0)$ it follows that $a = f(0) \leq f(1) = b$.
  • If $x_0 < 2/3$ then from $f(x_0) \geq f(1)$ it follows that $a = f(0) \geq f(1) = b$. $\Box$

Assuming that the maximum is attained in a vertex gets you to LPO.

Theorem: If every affine map $[0,1] \to \mathbb{R}$ attains its maximum at $0$ or $1$, then LPO holds.

Proof. Continuing with the same notation as in the previous proof, we may decide for any $a \geq 0$ whether $a = 0$ or $a > 0$, which suffices to establish LPO. By assumption the map $f_{0,a}$ attains its maximum $x_0$ which is either $0$ or $1$:

  • If $x_0 = 0$ then $a = 0$.
  • If $x_0 = 1$ then $a > 0$. $\Box$

P.S. Of course, since affine maps are very simple, the maximal value of $f_{a,b}$ exists, but the above arguments showargument shows it takes LLPO to know where it is attained.

You make an erroneous assumption in your question, as already in dimension 1 you need LLPO to know that the maximum is actually attained at some point.

We work constructively.

Theorem: If every affine map $[0,1] \to \mathbb{R}$ attains its maximum then LLPO shows.

Proof. The general form of an affine map on $[0,1]$ is $f_{a,b}(x) = a \cdot (1 - x) + b \cdot x$. Suppose then that for every such $f_{a,b}$ there exists $x_0 \in [0,1]$ such that $f_{a,b}(x) \leq f_{a,b}(x_0)$ for all $x \in [0,1]$.

Note that the following holds: if $f_{a,b}(0) \leq f_{a,b}(t)$ for some $t > 0$ then $f_{a,b}(0) \leq f_{a,b}(1)$. Similarly, if $f_{a,b}(t) \geq f_{a,b}(1)$ for some $t < 1$ then $f_{a,b}(0) \geq f_{a,b}(1)$.

Consider any two reals $a, b \in \mathbb{R}$. We shall decide $a \leq b \lor b \leq a$, which implies LLPO. By assumption, the map $f_{a,b}$ attains its maximum at some $x_0 \in [0,1]$. Either $x_0 < 2/3$ or $x_0 > 1/3$:

  • If $x_0 > 1/3$ then from $f(0) \leq f(x_0)$ it follows that $a = f(0) \leq f(1) = b$.
  • If $x_0 < 2/3$ then from $f(x_0) \geq f(1)$ it follows that $a = f(0) \geq f(1) = b$. $\Box$

Assuming that the maximum is attained in a vertex gets you to LPO.

Theorem: If every affine map $[0,1] \to \mathbb{R}$ attains its maximum at $0$ or $1$, then LPO holds.

Proof. Continuing with the same notation as in the previous proof, we may decide for any $a \geq 0$ whether $a = 0$ or $a > 0$, which suffices to establish LPO. By assumption the map $f_{0,a}$ attains its maximum $x_0$ which is either $0$ or $1$:

  • If $x_0 = 0$ then $a = 0$.
  • If $x_0 = 1$ then $a > 0$. $\Box$

P.S. Of course, since affine maps are very simple, the maximal value of $f_{a,b}$ exists, but the above arguments show it takes LLPO to know where it is attained.

You make an erroneous assumption in your question, as already in dimension 1 you need LLPO to know that the maximum is actually attained at some point.

We work constructively.

Theorem: If every affine map $[0,1] \to \mathbb{R}$ attains its maximum then LLPO shows.

Proof. The general form of an affine map on $[0,1]$ is $f_{a,b}(x) = a \cdot (1 - x) + b \cdot x$. Suppose then that for every such $f_{a,b}$ there exists $x_0 \in [0,1]$ such that $f_{a,b}(x) \leq f_{a,b}(x_0)$ for all $x \in [0,1]$.

Note that the following holds: if $f_{a,b}(0) \leq f_{a,b}(t)$ for some $t > 0$ then $f_{a,b}(0) \leq f_{a,b}(1)$. Similarly, if $f_{a,b}(t) \geq f_{a,b}(1)$ for some $t < 1$ then $f_{a,b}(0) \geq f_{a,b}(1)$.

Consider any two reals $a, b \in \mathbb{R}$. We shall decide $a \leq b \lor b \leq a$, which implies LLPO. By assumption, the map $f_{a,b}$ attains its maximum at some $x_0 \in [0,1]$. Either $x_0 < 2/3$ or $x_0 > 1/3$:

  • If $x_0 > 1/3$ then from $f(0) \leq f(x_0)$ it follows that $a = f(0) \leq f(1) = b$.
  • If $x_0 < 2/3$ then from $f(x_0) \geq f(1)$ it follows that $a = f(0) \geq f(1) = b$. $\Box$

Of course, since affine maps are very simple, the maximal value of $f_{a,b}$ exists, but the above argument shows it takes LLPO to know where it is attained.

Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

You make an erroneous assumption in your question, as already in dimension 1 you need LLPO to know that the maximum is actually attained at some point.

We work constructively.

Theorem: If every affine map $[0,1] \to \mathbb{R}$ attains its maximum then LLPO shows.

Proof. The general form of an affine map on $[0,1]$ is $f_{a,b}(x) = a \cdot (1 - x) + b \cdot x$. Suppose then that for every such $f_{a,b}$ there exists $x_0 \in [0,1]$ such that $f_{a,b}(x) \leq f_{a,b}(x_0)$ for all $x \in [0,1]$.

Note that the following holds: if $f_{a,b}(0) \leq f_{a,b}(t)$ for some $t > 0$ then $f_{a,b}(0) \leq f_{a,b}(1)$. Similarly, if $f_{a,b}(t) \geq f_{a,b}(1)$ for some $t < 1$ then $f_{a,b}(0) \geq f_{a,b}(1)$.

Consider any two reals $a, b \in \mathbb{R}$. We shall decide $a \leq b \lor b \leq a$, which implies LLPO. By assumption, the map $f_{a,b}$ attains its maximum at some $x_0 \in [0,1]$. Either $x_0 < 2/3$ or $x_0 > 1/3$:

  • If $x_0 > 1/3$ then from $f(0) \leq f(x_0)$ it follows that $a = f(0) \leq f(1) = b$.
  • If $x_0 < 2/3$ then from $f(x_0) \geq f(1)$ it follows that $a = f(0) \geq f(1) = b$. $\Box$

Assuming that the maximum is attained in a vertex gets you to LPO.

Theorem: If every affine map $[0,1] \to \mathbb{R}$ attains its maximum at $0$ or $1$, then LPO holds.

Proof. Continuing with the same notation as in the previous proof, we may decide for any $a \geq 0$ whether $a = 0$ or $a > 0$, which suffices to establish LPO. By assumption the map $f_{0,a}$ attains its maximum $x_0$ which is either $0$ or $1$:

  • If $x_0 = 0$ then $a = 0$.
  • If $x_0 = 1$ then $a > 0$. $\Box$

P.S. Of course, since affine maps are very simple, the maximal value of $f_{a,b}$ exists, but the above arguments show it takes LLPO to know where it is attained.