Попытки выйти на RH

[mihaild]

Andrei_Tiumentsev в сообщении #1734128 писал(а):

квантор $\forall x\in M$ заменяется на $\forall x\in M_i$; - каждый шаг вывода, где используется условие $x\in M$, заменяется на использование условия $x\in M_i$.

Вторая часть - это пояснение, или часть определения?
Если пояснение, то несложно показать, что для любого доказуемого утверждения вида $\forall x: P(x) \rightarrow Q(x)$, и набора формул $P_1, \ldots, P_n$, таких, что $P_i(x) \rightarrow P(x)$ доказуемо для любого $i$, существует доказательство, такое, что если в нём заменить последнюю строчку на $\forall x: P_i(x) \rightarrow Q(x)$, то получится верное доказательство.

Не получится у Вас никак разумно формально определить "доказательство принципиально разбирает случаи", это неформальная категория. Формальные доказательства (в исчислении предикатов) используют всего лишь два правила вывода, и (для нетривиальных утверждений) никакой разумной интерпретации не поддаются.

[Andrei_Tiumentsev]

Хорошо. Допустим что: "существенно разбирает случаи" не формализуется как свойство формального вывода. По второму определению соглашусь, но тут возникает другое следствие. Вы говорите: формальный вывод не имеет разумной интерпретации. Если так, то математическое содержание - не в формальном выводе, а на уровне математической практики. Давайте спросим там. Формальный вывод не различает случаи - согласен. А вот математические аргументы различают.
Ну, например: Теорема Дирихле о простых в арифметических прогрессиях. Для разных классов вычетов - разные аргументы, разные L-функции, разные технические шаги. Формально это один вывод. Содержательно - вовсе не один. Стирание в представлении не отменяет различия в содержании.
То же с нулями $\zeta(s)$. Тривиальные нули лежат на вещественной оси - доказательство элементарное, из полюсов $\Gamma(s)$. Нетривиальные - доказательства нет вообще. Различие не формальное, а содержательное.
Тут хорошо бы спросить, на каком уровне вы работаете, когда говорите "Риман"? Если формальный вывод - единственный уровень, то утверждение бессодержательно. Если есть уровень содержания - мой вопрос законен.
Это не спор о формализме. Это вопрос, где локализовано математическое содержание. Ваш ответ "формальный вывод не имеет интерпретации" сам указывает на второй уровень.
Одно замечание перед тем как, наверное, разойдёмся. Вы сами отделяете тривиальные нули от нетривиальных по происхождению - из полюсов $\Gamma(s)$. Это не мой базис, это ваш.
Вопрос внутри вашего базиса: на каком основании это различение применяется один раз, на границе, и не применяется дальше? Если внутри нетривиальных нулей происхождение однородно - это содержательное утверждение, и его можно проверить. Если происхождение не рассматривается - тогда вопрос о локализации содержания остаётся открытым.
Это не спор. Это вопрос о последовательности метода.