математика vs метаматематика

[FeelUs]

disclaimer: я дилетант в матлогике, и по этому буду говорить общо, но при этом мне кажется, что при необходимости я смогу перейти к конкретным формальным выражениям (но мне лень). Если это не так - скажите.

В начале я хотел спросить, верно ли мое мировоззрение:

Математика распадается на 2 области:
- алгоритмически невычислимую
- и алгоритмически вычислимую, но экспоненциально сложную

Возьмем какой-нибудь набор (непротиворечивых, или кажущихся таковыми) аксиом, напишем алгоритм, который бы генерировал верные утверждения (сначала все утверждения с доказательствами, длина которых не превышает n, потом длина которых не превышает n+1, потом n+2 и т.д.)
По т.Геделя он не сможет сгенерировать некоторые утверждения (и их отрицания).
Получается математика - искусство подбирать новые (непротиворечивые) наборы аксиом, в которых можно было бы сгенерировать утверждения, которые в предыдущих наборах аксиом были недоказуемыми.
Но какой толк от такого алгоритма с практической точки зрения (даже если не рассматривать недоказуемые утверждения)?
Ведь ни кто не будет просматривать все эти утверждения, да и физической памяти на них ни какой не хватит.
Рациональнее было бы сделать алгоритм, который на вход получал бы некоторое утверждение и искал бы доказательство этого утверждения или его отрицания путем перебора всех доказательств сначала длины n, потом n+1, потом n+2 и т.д.
Такой алгоритм рано или поздно найдет доказательство заданного утверждения, если оно, конечно, доказуемо.
Но количество всевозможных доказательств растет экспоненциально с их длиной, и на классических компьютерах на практике эта затея неосуществима, в результате чего эти задачи приходится решать тоже своей головой.
(Конечно некоторые частные случаи утверждений можно доказать за полиномиальное время на классическом компьютере, такие как проблема 4 красок, но в общем случае мне не известно об алгоритмах поиска произвольного доказательства, работающих быстрее чем за экспоненциальное время.)
Таким образом получается, что математика распадается на 2 области:
- алгоритмически невычислимую(недоказуемую)
- и алгоритмически вычислимую, но экспоненциально сложную

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

Но потом меня чё-то еще пропёрло:

Но изначально для заданного утверждения мы не знаем, в какую область оно попадет.
А как доказывают недоказуемость?
Подбирают новые аксиомы (аксиоматику), в которой предыдущие аксиомы верны (т.е. или являются подмножеством новых аксиом или являются теоремами в новой аксиоматике), и доказывают новое утверждение: что утверждение, которое пытались доказать ранее - недоказуемо в предыдущей аксиоматике.
Но ведь множество наборов(конечных множеств) аксиом - счетно.
И для каждого набора (в котором старые аксиомы верны*) надо доказать новое утверждение.
Т.е. как-будто мы запускаем и запускаем и запускаем счетное количество машин Тьюринга, которые начинают искать доказательство нового утверждения в новом наборе аксиом.
Очевидно мы можем сделать это на одной МТ (псевдо-параллелизм). (Точно так же как декартово произведение N*N счетно)
*Перед доказательством нового утверждения нужно доказать предыдущие аксиомы.
Этот этап опять можно запустить (псевдо)параллельно, и если они все доказуемы, то этот этап рано или поздно будет завершен, и можно будет перейти к поиску доказательства нового утверждения, а если нет, то это просто замедлит работу других (псевдо)параллельно выполняющихся МТ, но нам как-то параллельно.
А т.к. каждое утверждение либо доказуемо либо недоказуемо (в исходной аксиоматике), то мы можем запустить 2 МТ, одна из которых будет пытаться доказать его, а другая - искать аксиоматику, в которой будет доказано, что оно недоказуемо.
Раз уж мы счетное кол-во МТ смогли запустить на одной, то и 2 МТ - тоже сможем.
Если бы мы могли для любого утверждения
- либо его доказать,
- либо найти систему аксиом (в которой верны предыдущие аксиомы), в которой могли бы доказать недоказуемость этого утверждения (в исходной аксиоматике),
то получившаяся МТ гарантированно остановилась бы (для любого исходного утверждения), и ответила бы тем самым на вопрос, доказуемо ли данное утверждение или нет.
А т.к. это эквивалентно ответу на вопрос "остановится ли алгоритм, который пытается доказать исходное утверждение в исходной аксиоматике", то это было бы решением проблемы остановки, а его не существует.

Значит, существуют утверждения, которые не только недоказуемы, но и доказать недоказуемость которых невозможно, причем ни в одной аксиоматике (т.е. в конечном наборе исходно верных утверждений) (в которой верны предыдущие аксиомы).

По моему во всем вышеизложенном доказательстве можно убрать требование того, чтобы в новой аксиоматике были верны старые аксиомы.

Т.е. я просто попытался написать алгоритм, доказывающий недоказуемость

Я хотел было назвать это теоремой о неполноте неполноты,
Но на лицо явное противоречие, т.к. мы к старому набору аксиом можем добавить аксиому о том, что исходное утверждение недоказуемо в исходной аксиоматике
Может я не учел, что аксиоматика должна быть непротиворечивой...

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

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

FeelUs
Предупреждение за нецензурную лексику
// Lia

[mustitz]

Я тоже дилетант в матлогике, пусть меня тоже поправят, но по-моему очень много домысливания «от себя».

Трудно сказать, что математика распадается на две части. Много математиков работает в системе аксиом ZFC и горя не знают. Так что математика большей частью это не искусство подбирать новые системы аксиом, а искусство работы в одной из таких систем. Если учесть интуиционистов, то в двух системах. Обе они алгоритмически неразрешимы.

Ну а так да, если рассмотреть произвольную систему аксиом $\mathfrak T$, то задача «доказуеама ли формула в данной теории» может быть либо алгоритмически разрешимым, либо нет. О какой-то сложности я бы не стал говорить, потому что непонятно как её считать. Если взять противоречивую теорию, то сложность будет вообще $O(1)$, потому как для любой формулы нам надо ответить «да, доказуема».

Ну а дальше абсолютно непонятна цель.

[Sonic86]

FeelUs в сообщении #1165364 писал(а):

Подбирают новые аксиомы (аксиоматику), в которой предыдущие аксиомы верны (т.е. или являются подмножеством новых аксиом или являются теоремами в новой аксиоматике)

Последний случай непонятен: вот есть 2 системы аксиом $A$ и $A'$ - старая и новая. Вы хотите здесь строить доказательство, что $A\to A'$. Тогда проблемы:
1. А в какой системе Вы будете строить доказательство?
2. (главное) А что, если $A'$ невыводима из $A$? Может быть невыводима ровно так же, как невыводимы недоказуемые утверждения в системе аксиом $A$.
3. Как и где Вы докажете, что $A'$ непротиворечива? Например, $A' :=\ A \cup \{1\not = 1\}$

FeelUs в сообщении #1165364 писал(а):

Если бы мы могли для любого утверждения
- либо его доказать,
- либо найти систему аксиом (в которой верны предыдущие аксиомы), в которой могли бы доказать недоказуемость этого утверждения (в исходной аксиоматике),

Я для любого утверждения $X$ могу без запуска счетного числа МТ подобрать систему аксиом, в которой $X$ доказуемо. Только вот если я эту систему аксиом напишу, это вызовет не энтузиазм, а зевоту.

Короче говоря, давайте все заново, поток сознания, как всегда, не проканал

[Deggial]

Тема перемещена из форума «Математика (общие вопросы)» в форум «Дискуссионные темы (М)»
Причина переноса: в соответствующий раздел

FeelUs, для второй части темы Вам предлагается попытаться всё выписать заново. В противном случае тема либо заглохнет, либо поедет в Карантин.

[FeelUs]

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

А еще я когда-то читал Пенроуза "Новый ум короля", и он там во 2й главе основываясь на проблеме остановки МТ говорил, что вот машина ни как не сможет (т.е. не существует алгоритма) определить остановится ли заданная МТ на заданных входных данных или нет, а человек сможет.
Но подождите, откуда мы знаем, что человек(люди) для любого утверждения за конечное время найдут его доказательство?
В полне возможно, что люди, точно так же как механическая(электронная) машина просто перебирают доказательства (это сильно утрировано, но по моему оно действительно так), и тогда существуют вопросы, на которые у нас никогда не получится дать обоснованный ответ (при этом в процессе работы людей будут генерироваться доказательства все новых и новых утверждений).

И развивая эту тему дальше, я стал придумывать алгоритм, который перебирает уже аксиомы, чтобы получить, что и первая область математики - ни какое не искусство, а тоже перебор случаев.

2 Sonic86:
1) В новой.
2) если старая невыводиима из новой, я написал, что это нам по***.
Вот у нас есть счетное кол-во МТ, пронумеруем их 1, 2, 3...
Каждая из них запускается с новой аксиоматикой, и сначала пытается из нее вывести старую аксиоматику (это можно сделать последовательно), после чего начинает доказывать новое утверждение (что в старой аксиоматике старое утверждение невыводимо).
Каждая МТ работает конечными фрагментами во времени (например проверка, доказывает ли очередное доказательство то, что нам нужно).
Порядок их работы такой: 1, 1, 2, 1, 2, 3, 1, 2, 3, 4, 1, 2, 3, 4, 5, 1...
В каждый момент времени начало работать конечное кол-во МТ.
И каждая из них в каждый момент времени использует конечное кол-во памяти.
И если одна из них зациклилась, от этого другие МТ не перестанут работать, и если одна из них завершит свою работу, то МТ-менеджер узнает об этом, и тоже завершит работу всех остальных МТ (уже насильно).
3) вот это главное. И это я не учел. И чтобы доказать, что некоторая аксиоматика непротиворечива по все той же теореме Геделя в рамках самой этой аксиоматики это сделать не удастся за конечное время (можно за бесконечное, просто запустив поиск противоречия). Чтобы это доказать необходимо будет придумать новую аксиоматику, в которой это доказать, а также придумать еще одну аксиоматику, в которой доказать, что придуманная ранее аксиоматика непротиворечива и снова придумать новую аксиоматику, вы уже догадываетесь для чего, и это процесс бесконечный, ...

А вот интересно, допускает(ют) ли теорема(ы) Геделя существование двух систем аксиом, таких что в первой системе можно доказать непротиворечивость второй, а во второй - непротиворечивость первой?

...и надо разобраться в следующем фрагменте, что тут и почему:

Раз уж мы счетное кол-во МТ смогли запустить на одной, то и 2 МТ - тоже сможем.
Если бы мы могли для любого утверждения
- либо его доказать (1я МТ),
- либо найти систему аксиом (в которой верны предыдущие аксиомы), в которой могли бы доказать недоказуемость этого утверждения (в исходной аксиоматике),
то получившаяся МТ гарантированно остановилась бы (для любого исходного утверждения), и ответила бы тем самым на вопрос, доказуемо ли данное утверждение или нет (2я МТ).
А т.к. это эквивалентно ответу на вопрос "остановится ли алгоритм, который пытается доказать исходное утверждение в исходной аксиоматике", то это было бы решением проблемы остановки, а его не существует.
Значит, существуют утверждения, которые не только недоказуемы, но и доказать недоказуемость которых невозможно, причем ни в одной аксиоматике (т.е. в конечном наборе исходно верных утверждений) (в которой верны предыдущие аксиомы).

И это поможет ответь на вопрос: сводится ли первая область математики к перебору (так же как и вторая), который быть может никогда не завершится, или нет?

-- 02.11.2016, 23:19 --

А не существует ли такой теоремы Геделя или просто очевидного факта о том, что если в системе аксиом A я могу доказать непротиворечивость системы аксиом B, то значит в системе аксиом А я могу доказать любое утверждение, которое можно доказать в системе аксиом B?

[FeelUs]

Я в начале делал фактически экспериментально проверяемое предсказание для второй области, что после создания квантового компьютера на котором можно будет выполнять экспоненциально сложные (в зависимости от длины перебираемых объектов) (для классического компьютера) алгоритмы перебора за полиномиальное время, на нем будет доказано много теорем. Т.е. соотношение количества теорем, доказанных компьютерами, и теорем, доказанных людьми резко изменится.
И если первая область на столько же перебираемая как и вторая, то это же предсказание будет справедливо и для первой области - области недоказуемых в классических аксиоматиках утверждений.

[Sonic86]

FeelUs в сообщении #1165561 писал(а):

А еще я когда-то читал Пенроуза "Новый ум короля", и он там во 2й главе основываясь на проблеме остановки МТ говорил, что вот машина ни как не сможет (т.е. не существует алгоритма) определить остановится ли заданная МТ на заданных входных данных или нет, а человек сможет.

ИМХО, это чушь.
Во-первых, человек может не всегда это сделать, а для каких-то конкретных случаев.
Во-вторых, в какой системе аксиом это делает человек и какую систему аксиом предлагают машине? Вот то-то и оно.

FeelUs в сообщении #1165561 писал(а):

Но подождите, откуда мы знаем, что человек(люди) для любого утверждения за конечное время найдут его доказательство?

Ну вот опять же: доказательство утверждения - оно не "вообще", оно доказательство в какой-то системе аксиом. Так теорема Геделя о неполноте нам как раз явно утверждает противоположное, что если мы взяли какую-то непротиворечивую систему аксиом, из которой следуют аксиомы Пеано, то есть конкретное утверждение, которое в рамках этот системы аксиом доказать нельзя. А если нам разрешается произвольно менять систему аксиом, то задача доказательства такого утверждения становится тривиальной.

FeelUs в сообщении #1165561 писал(а):

И развивая эту тему дальше, я стал придумывать алгоритм, который перебирает уже аксиомы, чтобы получить, что и первая область математики - ни какое не искусство, а тоже перебор случаев.

Ну это все давно известно: Вы показываете полуразрешимость задачи о доказательстве утверждения в системе аксиом: ну если оно выводимо, то Вы его выведете. А если недоказуемо или не выводимо?

FeelUs в сообщении #1165364 писал(а):

Подбирают новые аксиомы (аксиоматику), в которой предыдущие аксиомы верны (т.е. или являются подмножеством новых аксиом или являются теоремами в новой аксиоматике), и доказывают новое утверждение: что утверждение, которое пытались доказать ранее - недоказуемо в предыдущей аксиоматике.

Sonic86 в сообщении #1165426 писал(а):

Последний случай непонятен: вот есть 2 системы аксиом $A$ и $A'$ - старая и новая. Вы хотите здесь строить доказательство, что $A\to A'$. Тогда проблемы:
1. А в какой системе Вы будете строить доказательство?
2. (главное) А что, если $A'$ невыводима из $A$? Может быть невыводима ровно так же, как невыводимы недоказуемые утверждения в системе аксиом $A$.
3. Как и где Вы докажете, что $A'$ непротиворечива? Например, $A' :=\ A \cup \{1\not = 1\}$

FeelUs в сообщении #1165561 писал(а):

2 Sonic86:
1) В новой.

Т.е. Вы будете доказывать, что $A'\to A'$? Ну очень интересно

FeelUs в сообщении #1165561 писал(а):

2) если старая невыводиима из новой, я написал, что это нам по***.

Ну программо зациклиццо. Ну м.б. Вас это тоже не интересует...

FeelUs в сообщении #1165561 писал(а):

3) вот это главное. И это я не учел.

И как теперь Вы этот вопрос решаете? Или все, никак?

FeelUs в сообщении #1165561 писал(а):

И это поможет ответь на вопрос: сводится ли первая область математики к перебору (так же как и вторая), который быть может никогда не завершится, или нет?

Как насчет теоремы Геделя о неполноте?
Хотя м.б. ответ выглядит гораздо интереснее, но не так тривиально...

Остальной текст я че-то ниасилил. Out of memory. Написали бы покороче, чего Вы хотите и что утверждаете.

upd:

FeelUs в сообщении #1165561 писал(а):

математика - искусство подбирать новые (непротиворечивые) наборы аксиом, в которых можно было бы сгенерировать утверждения, которые в предыдущих наборах аксиом были недоказуемыми.

Кстати, процедура генерации таких утверждений вроде как даже алгоритмизована конструктивно все в той же теореме Геделя о неполноте

[Someone]

FeelUs в сообщении #1165561 писал(а):

Я просто от одного человека (воодушевленного или пораженного теоремой Геделя) услышал, что "математика - искусство подбирать новые (непротиворечивые) наборы аксиом, в которых можно было бы сгенерировать утверждения, которые в предыдущих наборах аксиом были недоказуемыми."

Это ерунда.

FeelUs в сообщении #1165561 писал(а):

И, зная что много математиков работает в системе аксиом ZFC и горя не знают, попытался свести воедино эти 2 концепции.

Подавляющему большинству математиков в их работе начхать на ZFC и вообще на основания математики. Есть некоторое количество математиков, которые работают в областях, в которых аксиоматика ZFC или другой аналогичной теории может быть необходимой или полезной.

FeelUs в сообщении #1165364 писал(а):

Таким образом получается, что математика распадается на 2 области:
- алгоритмически невычислимую(недоказуемую)
- и алгоритмически вычислимую, но экспоненциально сложную

Есть примерно пара параллельных областей математики, где вопросы вычислимости существенны (рекурсивный анализ и конструктивный рекурсивный анализ, которые занимаются вопросами алгоритмической разрешимости; ещё, может быть, численных методов, но не вся). Для остальной математики на это начхать.

FeelUs в сообщении #1165364 писал(а):

А как доказывают недоказуемость?
Подбирают новые аксиомы (аксиоматику), в которой предыдущие аксиомы верны (т.е. или являются подмножеством новых аксиом или являются теоремами в новой аксиоматике), и доказывают новое утверждение: что утверждение, которое пытались доказать ранее - недоказуемо в предыдущей аксиоматике.

Бред, проистекающий из математической безграмотности.

[FeelUs]

Sonic86 в сообщении #1165642 писал(а):

ИМХО, это чушь.

Я вот сначала в это поверил, а сейчас тоже смотрю - чушь.

FeelUs в сообщении #1165561 писал(а):

определить остановится ли заданная МТ на заданных входных данных или нет

Sonic86 в сообщении #1165642 писал(а):

Во-первых, человек может не всегда это сделать, а для каких-то конкретных случаев.

Заданная МТ (читай заданный алгоритм) на заданных входных данных или остановится или нет не зависимо от того, что думают окружающие, или в какой системе аксиом они думают.
Т.е. например утверждение, что алгоритм Евклида рано или поздно остановится для любых 2 натуральных чисел (и при этом вернет то же число, что и алгоритм, перебирающий все натуральные числа, меньшие или равные минимума двух заданных чисел, и ищущий наибольший общий делитель), - можно считать абсолютной истиной.
Хотя с утверждением, что алгоритм, перебирающий $a,b,c \ge 1,n \ge 3 и останавливающийся, если выполнится равенство $ $a^n+b^n=c^n$, - закончит ли он когда-нибудь работать - не так очевидно.
Кстати возникает еще один, уже другой, вопрос о том, как обстоят дела с такого рода абсолютно истинными утверждениями в разных аксиоматиках, ведь если в формализме существуют натуральные числа, то и утверждения о машинах Тьюринга в этом формализме наверно можно формулировать.

1)

Sonic86 в сообщении #1165642 писал(а):

Т.е. Вы будете доказывать, что $A'\to A'$? Ну очень интересно

Я доказываю что что в новой системе аксиом верны все старые аксиомы, а значит в новой системе аксиом верны все утверждения, которые были верны в старой.

2)

Sonic86 в сообщении #1165642 писал(а):

Ну программо зациклиццо. Ну м.б. Вас это тоже не интересует...

Да пусть хоть все процессы зацикляцца кроме одного. Как только один процесс завершится, другим процессам просто не будет передано управление, а их данные будут стерты из памяти.

3)

Sonic86 в сообщении #1165642 писал(а):

И как теперь Вы этот вопрос решаете? Или все, никак?

Для начала я не знаю ответа на вопрос, допускает(ют) ли теорема(ы) Геделя существование двух систем аксиом, таких что в первой системе можно доказать непротиворечивость второй, а во второй - непротиворечивость первой?
А не существует ли такой теоремы Геделя или просто очевидного факта о том, что если в системе аксиом A я могу доказать непротиворечивость системы аксиом B, то значит в системе аксиом А я могу доказать любое утверждение, которое можно доказать в системе аксиом B?

И вообще я сейчас немного начинаю понимать, чем отличается доказуемость от вычислимости.
Доказуемость - она относительно набора аксиом, а вычислимость - она абсолютная. И вся математика - едина, а вот задание системы аксиом делит ее на доказуемую и недоказуемую. И вот если то, что доказуемая область математики - вычислима - это очевидно (Если утверждение доказуемо (что наперед не известно), то перебором можно найти доказательство); То как связаны недоказуемая область, определение того, в какую область попадет заданное утверждение и вычислимость/невычислимость - мне пока непонятно.

Someone в сообщении #1165734 писал(а):

FeelUs в сообщении #1165561 писал(а):

И, зная что много математиков работает в системе аксиом ZFC и горя не знают, попытался свести воедино эти 2 концепции.

Подавляющему большинству математиков в их работе начхать на ZFC и вообще на основания математики. Есть некоторое количество математиков, которые работают в областях, в которых аксиоматика ZFC или другой аналогичной теории может быть необходимой или полезной.

FeelUs в сообщении #1165364 писал(а):

Таким образом получается, что математика распадается на 2 области:
- алгоритмически невычислимую(недоказуемую)
- и алгоритмически вычислимую, но экспоненциально сложную

Есть примерно пара параллельных областей математики, где вопросы вычислимости существенны (рекурсивный анализ и конструктивный рекурсивный анализ, которые занимаются вопросами алгоритмической разрешимости; ещё, может быть, численных методов, но не вся). Для остальной математики на это начхать.

Ну наверно можно математику разбить на модули, каждый со своими аксиомами и теоремами, и теоремы одних модулей являются аксиомами других. А также еще нужно проследить, что не образовывается порочный круг. И все это можно соединить так, чтобы аксиомами остались только ZFC (если не брать в расчет утверждения, которые недоказуемы в ZFC). Я прав?

Someone в сообщении #1165734 писал(а):

Бред, проистекающий из математической безграмотности.

А что лучше почитать для ликвидации безграмотности: Булос Джеффри Вычислимость и логика, или Манин Доказуемое/недоказуемое и Вычислимое/невычислимое, или может что-то еще?

[Red_Herring]

Очередной бурный поток сознания, падающий вниз стремительным домкратом.

Цитата:

Если у тебя есть фонтан, заткни его; дай отдохнуть и фонтану

[Brukvalub]

FeelUs в сообщении #1165834 писал(а):

Ну наверно можно математику разбить на модули, каждый со своими аксиомами и теоремами, и теоремы одних модулей являются аксиомами других. А также еще нужно проследить, что не образовывается порочный круг. И все это можно соединить так, чтобы аксиомами остались только ZFC (если не брать в расчет утверждения, которые недоказуемы в ZFC). Я прав?

Вы с умным видом рассуждаете о том, в чем ни бельмеса не смыслите. Я прав?

[Sonic86]

FeelUs в сообщении #1165834 писал(а):

Я доказываю что что в новой системе аксиом верны все старые аксиомы, а значит в новой системе аксиом верны все утверждения, которые были верны в старой.

Вот тоже вопрос: вот возьмем вот эту вот аксиоматику исчисление высказываний и например арифметику Пеано. Как в арифметике Пеано доказать аксиомы исчисления предикатов?
Хотя, можно подоказывать разные аксиоматики геометрии одна из другой. Но там есть общий язык для утверждений, из которого берутся аксиомы. В общем случае надо еще какие-то соответствия устанавливать.

FeelUs в сообщении #1165834 писал(а):

Для начала я не знаю ответа на вопрос, допускает(ют) ли теорема(ы) Геделя существование двух систем аксиом, таких что в первой системе можно доказать непротиворечивость второй, а во второй - непротиворечивость первой?
А не существует ли такой теоремы Геделя или просто очевидного факта о том, что если в системе аксиом A я могу доказать непротиворечивость системы аксиом B, то значит в системе аксиом А я могу доказать любое утверждение, которое можно доказать в системе аксиом B?

На 2-й вопрос ответ "похоже, что да", просто для случая, когда $B\subset A$. Но мне так только идейно кажется, поскольку я не могу вообразить себе монстра "система аксиома $A$, где доказываются утверждения о системах аксиом". Т.е. есть конечно метаматематика, но она же не формальная, т.е. тут надо сначала формализовать метаматематику в какой-то 2-метаматематике, и вот тут у меня сразу out of memory происходит, а такой травы, как у Вас, у меня нет Потому я бы предпочел увидеть сильно больше текста, чем 1 абзац, чтобы это вообще хоть как-то пощупать.

FeelUs в сообщении #1165834 писал(а):

Булос Джеффри Вычислимость и логика

Эта вроде как хорошая.

FeelUs в сообщении #1165834 писал(а):

Манин Доказуемое/недоказуемое и Вычислимое/невычислимое

Эту я ниасилил.
Асилил я Мендельсона (но там почти только логика, теорема Геделя о неполноте в простом ее варианте) и Верещагина Шена - вот их порекомендую. Хотя там еще есть Клини, Чень Ли, Мальцев, Катленд например. Списки литературы есть в 3-хтомнике Верещагина и Шеня (по вычислимости - 3-й том). Вообще, много книг. Если травы много, можете Ершова и Палютина почитать.
Литературу по логике можно тупо нагуглить, можно в Вики посмотреть: https://ru.wikipedia.org/wiki/%D0%9C%D0 ... 0%BA%D0%B0, https://ru.wikipedia.org/wiki/%D0%A2%D0 ... 1%82%D0%B8, можно в тему post773882.html#p773882 с литературой посмотреть

[FeelUs]

Brukvalub в сообщении #1165837 писал(а):

FeelUs в сообщении #1165834 писал(а):

Ну наверно можно математику разбить на модули, каждый со своими аксиомами и теоремами, и теоремы одних модулей являются аксиомами других. А также еще нужно проследить, что не образовывается порочный круг. И все это можно соединить так, чтобы аксиомами остались только ZFC (если не брать в расчет утверждения, которые недоказуемы в ZFC). Я прав?

Вы с умным видом рассуждаете

Нет, не правы, иначе бы я в предложении "Я прав?" в конце поставил бы точку, ну или смайлик на худой конец.

Brukvalub в сообщении #1165837 писал(а):

о том, в чем ни бельмеса не смыслите. Я прав?

В этом вы правы, я об этом написал в самом начале первого поста.

Я умею только прогать на МТ, знаю как доказывается невычислимость проблемы остановки, и читал 1ю главу 1го тома Бурбаков,
А как доказывается т. Геделя о неполноте - не знаю,
но подозреваю, что о том, что существует невыводимая формула, доказывается приблизительно тем же методом диагонализации,
а вот о том, что формула, утверждающая непротиворечивость аксиоматики, невыводима - для меня совсем темный лес

[Brukvalub]

Замечательно! Вот программа действий:
1. Вы прекращаете писАть многобуквенные посты со своими фантастическими измышлениями в этом разделе форума, поскольку вряд ли найдутся желающие читать вам здесь лекции по основам мат.логики.
2. Вы запрашиваете в сети интересующие вас термины и понятия и мигом получаете кучи ссылок, двигаясь по которым, можно все понять и во всем разобраться (наличие таких ссылок - гарантирую, поскольку сейчас это модная тематика на волне интереса к CS).
3. Можно начать с 4-хтомника Барвайса, можно порыться в каталоге изданий GTM, я видел там немало книг по этой тематике, можно...много еще чего можно!

[Lia]

Тема закрыта как минимум до выполнения программы.