Интуиционистская логика и корень из двух

[alhimikoff]

Можно ли не от противного доказать, что $\sqrt{2}$ иррационален?

[venco]

Сначала дайте не от противного определение иррационального числа.

[slavav]

venco в сообщении #1084228 писал(а):

Сначала дайте не от противного определение иррационального числа.

Число - непрерывная дробь (последовательность неотрицательных целых чисел).
Иррациональное число - непрерывная дробь с бесконечным числом ненулевых членов.

[Anton_Peplov]

slavav в сообщении #1084278 писал(а):

Иррациональное число - непрерывная дробь с бесконечным числом ненулевых членов.

Таки $0.33333...$ иррациональное число?

[grizzly]

slavav в сообщении #1084278 писал(а):

Число - непрерывная дробь (последовательность неотрицательных целых чисел).
Иррациональное число - непрерывная дробь с бесконечным числом ненулевых членов.

Как-то не очень здорово получилось. Вы допускаете числа типа $[0;0,1,0,1]$ или $[0;0,1,0,1, ...]?$ И чему у Вас равны эти числа?

Anton_Peplov
С Вашим числом как раз проблем нет. Речь идёт о непрерывных дробях. Только запись для них принята другая.

[gefest_md]

alhimikoff, Вы считаете, что такое доказательство будет не по-интуиционистки, или Вам не нравится тавтология $(A\to B)\to((A\to\neg B)\to\neg A)$?

[slavav]

Anton_Peplov в сообщении #1084281 писал(а):

slavav в сообщении #1084278 писал(а):

Иррациональное число - непрерывная дробь с бесконечным числом ненулевых членов.

Таки $0.33333...$ иррациональное число?

Я говорил не о десятичных дробях а о непрерывных.
https://ru.wikipedia.org/wiki/%D0%9D%D0%B5%D0%BF%D1%80%D0%B5%D1%80%D1%8B%D0%B2%D0%BD%D0%B0%D1%8F_%D0%B4%D1%80%D0%BE%D0%B1%D1%8C

[Anton_Peplov]

Ах, цепная...

[Someone]

alhimikoff в сообщении #1084219 писал(а):

Можно ли не от противного доказать, что $\sqrt{2}$ иррационален?

Надо аккуратно сформулировать определение иррационального числа и посмотреть, какое получится доказательство иррациональности: "от противного" или не "от противного".

[slavav]

grizzly в сообщении #1084283 писал(а):

slavav в сообщении #1084278 писал(а):

Число - непрерывная дробь (последовательность неотрицательных целых чисел).
Иррациональное число - непрерывная дробь с бесконечным числом ненулевых членов.

Как-то не очень здорово получилось. Вы допускаете числа типа $[0;0,1,0,1]$ или $[0;0,1,0,1, ...]?$ И чему у Вас равны эти числа?

Вы правы.
Нули надо исключить на стадии определения - первое число целое, все последующие - натуральные. Соответственно, последовательность должна быть конечной или бесконечной. Некрасиво.
Или можно ввести эквивалентность на бесконечных последовательностях с нулями - сказать, что две в одном классе, если можно их привести к общему виду удаляя нули (те что после точки с запятой). Немного красивее.
Но это частности. Главная мысль - можно представить иррациональные числа без отрицания.

[whitefox]

$\sqrt2=[1;1+\sqrt2]=[1;2,1+\sqrt2]=[1;2,2,1+\sqrt2]=[1;2,2,2,1+\sqrt2]$
и так далее до бесконечности, следовательно $\sqrt2$ иррационально.

[bot]

slavav в сообщении #1084278 писал(а):

Иррациональное число - непрерывная дробь с бесконечным числом ненулевых членов

То есть процесс выделения целых частей бесконечен. Вот вроде бы whitefox последнее делает очевидным.
Мне так не кажется - отрицание никуда не ушло, оно замаскировалось: процесс очевидно оборвётся в рациональном случае, следовательно будет бесконечным в иррациональном.

[Someone]

Мне непонятно, чем уважаемым участникам обсуждения, включая автора вопроса, не нравится стандартное определение иррационального числа и стандартное доказательство иррациональности $\sqrt{2}$ методом бесконечного спуска. Оно вполне конструктивно, поскольку двойного отрицания там не возникает.

[slavav]

bot в сообщении #1084364 писал(а):

Мне так не кажется - отрицание никуда не ушло, оно замаскировалось: процесс очевидно оборвётся в рациональном случае, следовательно будет бесконечным в иррациональном.

Вы строите непрерывные дроби по вещественным числам. Но я предлагал другую логику - берём бесконечные последовательности неотрицательных целых, на них вводим классы, учимся классы складывать, вычитать, умножать и делить, вводим порядок, доказываем 14 аксиом вещественных чисел. Затем вводим определения:
целое - только первое число не ноль,
рациональное - только конечное число членов не нули,
иррациональное - бесконечное число членов не нули.
И наконец возводим в квадрат $[1; 2(, 2)]^2 = [2;0(, 0)]$.

[whitefox]

bot в сообщении #1084364 писал(а):

отрицание никуда не ушло, оно замаскировалось: процесс очевидно оборвётся в рациональном случае, следовательно будет бесконечным в иррациональном

Мы определили иррациональные числа как числа которые могут быть представлены бесконечными цепными дробями $[a_0;a_1,a_2,\dots],$ где $a_0$ целое, а все остальные элементы — целые положительные.

Приведённое построение показывает, что $\sqrt2$ иррациональное. При этом мы вовсе не доказываем, что оно не рациональное. Так что тут tertium non datur не используется.