Verificación de la prueba en análisis constructivo

Question

Quiero una prueba de que algo en análisis constructivo, que significa que sin la ley de medio excluido (o, si se prefiere esta interpretación, en intuitionistic lógica).

Primero algunas definiciones:

$C(x_1,x_2) = \{ \sum_{i=1}^{2} \lambda_i x_i : \lambda_i \in [0,1]\wedge \lambda_1 + \lambda_2 = 1 \}$.

Una métrica es la misma que en "estándar" de análisis.

Para algún subconjunto $Y$a de un espacio métrico $X$ definimos la distancia de $x \in X$ a $Y$ por $d(x,Y) = \inf \{d(x,y) : y \in Y \}$.

Ahora el problema: tengo un número real $\neg(x=0)$ y definen los vectores $x_1 = (1,x)$ e $x_2 = (x,0)$ en $\mathbb{R}^2$. Quiero mostrar que la $\neg(0= d(0,C(x_1,x_2))$.

Para ello quiero utilizar la siguiente regla: Si bajo la hipótesis de $b$ las declaraciones $a$ e $\neg a$ ambos conducen a $\bot$, luego me $\neg b$ (este no tiene en intuitionistic lógica). Así que asumo $0= d(0,C(x_1,x_2) = \inf \{d(0,\lambda x_1 + (1-\lambda)x_2 : \lambda \in [0,1] \} $. Deje $\lambda_n$ ser una secuencia tal que, en el límite alcanzamos el infimum arriba. Entonces tengo dos casos: i) $\lambda_n \rightarrow 0$ o ii) $\lambda_n \rightarrow t \in (0,1]$. En el primer caso se consigue $0 = \lim_{n\rightarrow \infty}d(0,\lambda_n x_1 + (1-\lambda_n) x_2) = d(0, x_2) $ e lo $x_2 = 0$, por lo tanto $x = 0$; una contradicción. En el último caso llego $0 = \lim_{n\rightarrow \infty}d(0,\lambda_n x_1 + (1-\lambda_n) x_2) = d(0,t x_1 + (1-t) x_2 )= d(0,t(1,x) + t(x,0))$. En particular, $tx = 0$, una contradicción. En total puedo conseguir el resultado deseado.

Entre otras cosas, tengo las siguientes preguntas: ¿se Puede definir una secuencia $\lambda_n$?. Puedo concluir de manera constructiva a partir de $tx= 0$ que cualquiera de las $t = 0$ o $x =0$?. Gracias de antemano.

Answer 1

Creo que he encontrado la respuesta: mi prueba tiene algunas fallas, en particular, de una secuencia no puede ser definido de manera constructiva. Sin embargo, me vino con la siguiente prueba:

Asumir
\begin{align}\label{eq11} 0=d(0,C(a_1,a_2)). \end{align} llamamos a esta ecuación * . Observe que $d(0,C(a_1,a_2)) = \inf \{d(0,\lambda a_1 + (1-\lambda)a_2) : \lambda \in [0,1]\}$. Vamos a demostrar que (*) implica $x=0$, lo que estaría en contradicción con $\neg(x=0)$. Suponga que $\vert x \vert > 0$. Tenemos dos casos:

Caso 1 $(x > 0)$: tendremos a $\lambda > 1/2$ o $ \lambda < 2/3$. En el primer caso obtenemos $ \lambda + (1-\lambda)x > 1/2 > 0$ y en el último caso, $\lambda + (1-\lambda) x > x/3 > 0$. Por lo tanto, contradicen (*).

Caso 2 $(x < 0)$: suponemos $\vert x \vert < 1/2$. Tendremos a $\lambda > -x /3$ o $\lambda < -x/2$. En el primer caso obtenemos $\lambda x < - x^2/3 < 0$. En este último caso obtenemos $ \lambda + (1-\lambda)x < \lambda +x/2 < 0$. Por lo tanto, contradicen (*).

En total, observamos $x =0$. Por lo tanto $(*)$ implica $\bot$, es decir, obtenemos $\neg(0=d(0,C(a_1,a_2))$.

Answer 2

Necesito leer tu post con más cuidado lo que voy a hacer mañana. Usted está leyendo acerca de análisis constructivo a partir de un determinado libro de texto?

Yo sé que la declaración de $\forall x,y \in \mathbb R \left(xy = 0 \implies \left(x=0 \lor y=0\right)\right)$ es equivalente a la menor limitada principio de la omnisciencia (LLPO) que se sabe que no constructiva (pero más débil que LEM). Voy a probar el pertinente (hacia adelante), la dirección de esta citada equivalencia mañana.

---

Menor limitada principio de la omnisciencia (LLPO): Para cada secuencia binaria $\{a_n\}_{n=1}^\infty$ con más de un término igual a $1$, $a_{2n-1}=0$ para todos los $n$ o de lo $a_{2n}=0$ para todos los $n$.

---

Supongamos que la declaración de $\forall x,y \in \mathbb R \left(xy = 0 \implies \left(x=0 \lor y=0\right)\right)$ sostiene. Deje $\{a_n\}_{n=1}^\infty$ ser una secuencia binaria con más de un término igual a $1$. Se definen dos secuencias de $\{x_n\}_{n=1}^\infty$ e $\{y_n\}_{n=1}^\infty$por \begin{equation}x_n:= \begin{cases} \frac{1}{k} & \text{ if } \, 2k-1 \leq n \text{ and } \, a_{2k-1}=1, \\ 0 & \text{ otherwise} \end{casos} \end{equation} y \begin{equation}y_n:= \begin{cases} \frac{1}{k} & \text{ if } \, 2k \leq n \text{ and } \, a_{2k}=1, \\ 0 & \text{ otherwise}. \end{casos} \end{equation} Poner $x=\lim_{n \to \infty} x_n$ e $y=\lim_{n \to \infty} y_n$. Aviso de $xy=0$, desde el $x_ny_n = 0$ por cada $n \in \mathbb N$. Además, $x=0$ fib $a_{2n-1}=0$ para todos los $n$, e $y=0$ fib $a_{2n}=0$ para todos los $n$.

Answer 3

Creo que puedo responder el siguiente problema: $xy = 0$ entonces $x = 0$ o $y = 0$. Primero algunas definiciones:

Un número real es un subconjunto x de a$\mathbb{Q} \times \mathbb{Q}$ tales que

i) para todos los $(q,q')$ en $x$ tenemos $ q \le q'$,

ii) para todos los $(q,q')$ e $(r,r')$ en $x$, el cierre de los intervalos de $[q,q']$ e $[r,r']$ en $\mathbb{Q}$ se intersecan en los puntos en $\mathbb{Q}$,

iii) para todos los positivos racionales $\varepsilon$ no sale de $(q,q')$ en $x$ tal que $ q' - q < \varepsilon$.

Decimos que dos números reales $x$ e $y$ son igual si para todas las $(q,q') \in x $ y todos los $(r,r') \in y$ cerrado intervalos de $[q,q']$ e $[r,r']$ tiene un punto racional en común.

El producto $xy$ se define como el conjunto de todos racional de los pares de $(s,s')$ que no existe $ (q,q') \in x$ e $(r,r') \in y$con \begin{align*} s = \min\left\{qr,qr',q'r,q'r'\right\}, \quad s' = \max\left\{qr,qr',q'r,q'r'\right\}. \end{align*}

Ahora el problema: Primer aviso de que el caso distinción es permitido al considerar los números racionales.

Deje $(q,q') \in x$ e $(r,r') \in y$. Elija $(0,0) \in 0$. Set $s = \min\left\{qr,qr',q'r,q'r'\right\}$ e $s' = \max\left\{qr,qr',q'r,q'r'\right\}$. Deje $(u,u') \in 0$. Por definición, obtenemos $ u \le 0 \le u'$ e lo $0 \in [u,u']$. Ahora es suficiente para mostrar $0 \in [q,q']$ o $0 \in [r,r']$. Note primero que no vamos a considerar los casos donde $q > q'$ o $r > r'$, ya que esto no es posible debido a la definición. Por supuesto, tenemos $ 0 \in [s,s']$.

Caso 1(existe un elemento $a \in \left\{qr,qr',q'r,q'r'\right\}$ tal que $a = 0$): w.l.o.g asumen $a = qr$. Con esto queremos conseguir, bien $q = 0$ o $r = 0$. En el primer caso obtenemos $ 0 \in [q,q']$ y en el último llegamos $ 0 \in [r,r']$.

Caso 2(existen elementos $a,b \in \left\{qr,qr',q'r,q'r'\right\}$ tal que $a < 0 < b$).

Caso 2.1($a = qr$ e $b = q'r$): por esto conseguimos $q < 0$ e $r > 0$. Por lo tanto, $q' > 0$ e lo $0 \in [q,q']$.

Caso 2.2($a = qr$ e $b = q'r'$).

Caso 2.2.1($q < 0$ e $r > 0$): a continuación, llegamos $r' > 0$ e lo $ 0 \in [r,r']$.

Caso 2.2.2($q > 0$ e $r < 0$): a continuación, llegamos $q' > 0$ e lo $ 0 \in [q,q']$.

Caso 2.3($a = q'r$ e $b = qr'$): esto implica $q' > 0$ e $r < 0$.

Caso 2.3.1($q >0$ e $r '> 0$): a continuación, llegamos $ 0 \in [r,r']$.

Caso 2.3.2($q < 0$ e $r ' < 0$): a continuación, llegamos $ 0 \in [q,q']$.