Probar de forma constructiva que $\log_2 3$ es irracional.

Question

La prueba habitual de que $\log_2 3$ es irracional es por contradicción. Por ejemplo:

Supongamos la negación: que $\log_2 3 = m/n$ para algunos enteros $m$ y $n$. Entonces, por la propiedad de los logaritmos, $2^{m/n} = 3$, lo que implica que $2^m = 3^n$. Sin embargo, $2^m$ es par y $3^n$ es impar y un número par no puede ser igual a un número impar. Por lo tanto, la suposición de que $\log_2 3$ es racional es incorrecta.

Entiendo que esta forma de prueba por contradicción (suponer la negación y llegar a una contradicción) utiliza la ley del tercero excluido (que probar $\lnot \lnot A$ es lo mismo que probar $A$) y por lo tanto no es una prueba constructiva válida.

Entonces eso me lleva a mi pregunta en dos partes:

• ¿Es la prueba realmente válida como prueba constructiva (es decir, ¿está equivocada mi comprensión) y si es así, por qué es válida?
• Si no es válida, ¿cuál es una prueba constructiva de que $\log_2 3$ es irracional?

Answer 1

$x$ es irracional se define como "$x$ no es racional", por lo que una prueba que muestre que a partir de la suposición de que $x$ es racional derivamos una contradicción es una prueba constructiva válida para "$x$ no es racional", de hecho es la prueba habitual para estas afirmaciones negativas en, por ejemplo, lógica intuicionista.

Answer 2

Comentando sobre la respuesta de Henno Brandsma, es cierto que la irracionalidad puede definirse como la absurdidad de la racionalidad. Otra convención que comúnmente se utiliza para la irracionalidad, por ejemplo en Bishop, es estar alejado de cada número racional. Nótese que esta es una propiedad afirmativa, ya que se debe proporcionar una distancia positiva respecto al número de interés para cada número racional.

En ese sentido, técnicamente ya has hecho la parte más difícil de la prueba al notar que $2^m\neq 3^n$ (en el sentido estricto!) para todos los pares de enteros $n$ y $m$ con $n>0$. El resto solo utiliza la inyectividad fuerte de logaritmos y de la división real: $$n\log_2(3)\neq m,$$ y $$\log_2(3)\neq\frac{m}{n}.$$ Componiendo de esta manera las pruebas que muestran que los logaritmos y la división mapan pares alejados a pares alejados, y que $\lvert 2^m-3^n\rvert>0$ para todos los pares relevantes, esto esquematiza un algoritmo perfectamente válido que toma como entrada un racional $p$ y devuelve, por ejemplo, un natural testigo $k>0$ tal que $\lvert\log_2(3)-p\rvert>\frac{1}{k}$.

Encuentro que esta definición está más en consonancia con el análisis numérico, ya que evita muchas posibles dobles negaciones posteriores, y proporciona información valiosa que es factiblemente exploratoria y refleja lo que intuitivamente es la irracionalidad—en particular, esto hace que el conjunto de irracionales sea un $G_\delta$, como clásicamente lo era, mientras que los racionales siguen siendo un $F_\sigma$.

(*Sin embargo, esto introduce muchos matices en la relación lógica entre racionalidad e irracionalidad. Algunos pueden ver esto como relleno, mientras que otros pueden verlo como simplemente la distinción numérica requerida.)