Метатеоремы

[oleg.k]

arseniiv
Спасибо, про объекты понял.

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

Читаю Шенфилда - у него функции и отношения, когда еще и $ZFC$ близко нету.

Или про алфавит. Вот есть алфавит. Что это такое? Конченый или счетный набор каких-то различных символов. А что такое счетный? Натуральных чисел же нету пока еще.

И так во всем.

Вобщем, мне бы почитать что-нибудь, где с самого начала объяснялись бы элементарные вещи, причем строго. Я уже поднимал вопрос про литературу, но там я его слишком широко поставил. У меня основное желание - разобраться с основаниями. Причем меня интересует то, что идет либо "до" $ZFC$, либо "параллельно" с $ZFC$. Сама $ZFC$ не очень интересует.

[arseniiv]

oleg.k в сообщении #1427356 писал(а):

Тем не менее я так и не разобрался, где дно и как оно выглядит...

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

-- Сб ноя 23, 2019 21:48:59 --

oleg.k в сообщении #1427356 писал(а):

Или про алфавит. Вот есть алфавит. Что это такое? Конченый или счетный набор каких-то различных символов. А что такое счетный? Натуральных чисел же нету пока еще.

А почему нету? Вас пугают нестандартные модели арифметики? Вы ведь вряд ли разойдётесь с другими людьми (математически подкованными, а не теми, кто объявляет 0 ни чётным, ни нечётным) в базовых операциях и отношениях от конкретных натуральных чисел. Почему бы и не принять тогда, что они даны. Нам всё равно приходится доверять вещам просто так, никакая наука без этого не обходится. И потом, как уже заметил mihaild, результаты обосновывают нам, почему нам стоило довериться исходным положениям.

oleg.k в сообщении #1427356 писал(а):

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

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

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

-- Сб ноя 23, 2019 21:50:24 --

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

-- Сб ноя 23, 2019 21:51:47 --

Хотя наверно не в такой степени как я тут несколько раз наблюдал. Из-за программирования или чего у меня всегда была какая-то уверенность в свойствах конечных строк или подобных структур.

[oleg.k]

arseniiv в сообщении #1427358 писал(а):

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

И пусть она будет неформальной. Ничего страшного. Именно эти соглашения мне и хочется узнать. Я их вижу так:

1. Мы можем отличить какой-то конкретный символ некоторого алфавита от кота.
2. Мы можем считать до ста (натуральных чисел мы не знаем) (вместо 100 можно взять число и побольше если потребуется, но конечное)
3. Если перед нами два символа, то мы способны сказать, различны они или совпадают.
... и т.д.

Никаких натуральных чисел, счетных алфавитов, булевых функций и т.д.

Об этом вообще где-нибудь написано?

[arseniiv]

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

Кстати гляньте Манина, например перевод (нескольких книг разом, насколько понимаю) на английский с дополнениями:

Yu. I. Manin, Neal Koblitz, B. Zilber. A Course in Mathematical Logic for Mathematicians

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

[oleg.k]

arseniiv в сообщении #1427358 писал(а):

Вы ведь вряд ли разойдётесь с другими людьми (математически подкованными, а не теми, кто объявляет 0 ни чётным, ни нечётным) в базовых операциях и отношениях от конкретных натуральных чисел. Почему бы и не принять тогда, что они даны.

Брауэр и Гильберт тоже вроде математически подкованными были Если серьезно, то я не понимаю, какие правила рассуждений приемлимы... На меня неслабо так парадокс Рассела подействовал. Я бы был удовлетворен, например, такой ситуацией. Есть конечная корзина способов рассуждений. Выбирается набор приемлимых рассуждений. Одна группа людей может выбрать один набор, другая группа - другой набор. Получили две (или $n$) нетождественные математики. Далее строим формальные системы, выбираем аксиомы, что-то доказываем и т.д. Но все это после декларации "правил игры".

[arseniiv]

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

oleg.k в сообщении #1427366 писал(а):

Если серьезно, то я не понимаю, какие правила рассуждений приемлимы... На меня неслабо так парадокс Рассела подействовал.

Но ведь он не логический: мы можем из логики вытащить всё, что его вызывает, в собственно теоретико-множественные аксиомы.

Вообще я бы предполагал, что классическое исчисление высказываний (не предикатов) должно бы быть можно спокойно принимать как данность. Там ничего страшного возникнуть ну просто не может (в каком-то смысле). Интуиционистское — в ту же коробку, хотя оно может настораживать людей; однако оно на деле ещё менее рискованная затея чем классическое исчисление (вот посмотрите на странный закон Пирса — он там не выводится). Логики первого порядка уже наверно имеют полное право немного настораживать. Логики второго порядка обычно пытаются без нужды никому не показывать (зато там можно определить равенство логически; с другой стороны это не «зато», а «ибо»).

oleg.k в сообщении #1427366 писал(а):

Но все это после декларации "правил игры".

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

[oleg.k]

arseniiv в сообщении #1427369 писал(а):

Там ничего страшного возникнуть ну просто не может (в каком-то смысле).

Не могли бы Вы расшифровать этот фрагмент?

-- 23.11.2019, 20:51 --

Я просто где-то видел про какие-то сильные теоремы об исчислении высказываний, которые доказаны исключительно финитными методами. Вы об этом?

[arseniiv]

oleg.k в сообщении #1427376 писал(а):

Не могли бы Вы расшифровать этот фрагмент?

Это в том смысле, что пока мы не начинаем рассматривать совсем хитрые задачи, там ничего внезапного и неочевидного (и бесконечного) вылезать не должно. Например мы можем проверить любую формулу от $n$ пропозициональных переменных на то, тавтология она или нет, за $O(2^n)$ времени. Это конечно, хотя на практике обычно и неудовлетворительно.

oleg.k в сообщении #1427376 писал(а):

Я просто где-то видел про какие-то сильные теоремы об исчислении высказываний, которые доказаны исключительно финитными методами. Вы об этом?

Изначально нет, но навскидку я кстати сейчас не вспомню, какие бы из полезных теорем там требовали чего-нибудь нефинитного: выводы конечны, оценки переменных — конечные функции и т. д., выводы обычно конструктивно получаются, если например взять теорему о дедукции и другие теоремы о выводимости чего-то, если выводится что-то.

[Someone]

oleg.k в сообщении #1427349 писал(а):

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

Утверждение об объектах предметной теории является её теоремой.

А разве теорема предметной теории - это не последняя строка в доказательном тексте?

Да, конечно, это последняя строка в формальном доказательстве. Но только само это доказательство, как и всякий текст, является объектом метатеории.

[oleg.k]

А можно определить операции и отношения, не определяя функций и множеств?

[Someone]

Можно. Посмотрите на арифметику Пеано. В ней нет множеств. Однако операции и функции благополучно есть.
А вообще, читайте учебники. Форум не предназначен для пересказа учебников.

[oleg.k]

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

Можно.

Это слово закрывает большую часть моих вопросов. Теперь читать учебники станет гораздо проще.

[epros]

arseniiv в сообщении #1427369 писал(а):

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

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

[arseniiv]

Разве в классическом?

[warlock66613]

oleg.k в сообщении #1427361 писал(а):

Об этом вообще где-нибудь написано?

Я знаю одно место (я выделил жирным курсивом):

Н. Вавилов в Не совсем наивной теории множеств писал(а):

Потрясает наивность людей, которые считают, что понятия элемента, множества, функции, бесконечности, числа требуют дальнейшего анализа и обоснования, в то время как понятия символа, текста, конструктивного объекта, правильно составленной формулы, формального языка, выводимости, доказуемости, истинности ясны сами по себе. В действительности это иллюзия, обоснование математики с помощью логики - это обоснование прозрачного с помощью туманного.
<...>
Конструктивная математика опирается на тысячи неявных предположений, подразумеваемых, но не сформулированных аксиом. Кто может гарантировать, что за ночь в тексте не появляются новые символы и не исчезают старые, что мы в состоянии отличить один символ от другого.

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