Профессор Снэйп писал(а):
В схеме индукции не предикаты, а формулы с одной свободной переменной.
Someone писал(а):
К тому же, как писал Профессор Снэйп, в схеме аксиом индукции речь идёт не о предикатах, которых в арифметике Пеано всего один (равенство), а о формулах
Э-ээ... Давайте определимся с терминологией. Разумеется, я говорил о высказывательных формулах с одной свободной переменной. Однако что Вы, господа, называете "предикатом"? Насколько я знаю, предикат - в самом широком смысле это свойство или отношение, определённое для рассматриваемых объектов (одноместный предикат - это именно свойство). В логике предикат - это функция, отображающая объекты теории на логические значения. Правильно ли я понимаю, что Вы имели в виду, что не всякая такая функция записывается формулой теории? Если так, то я такие "предикаты" не рассматриваю, ибо полагаю, что если у функции нет формулы, то этой функции нет (не определена) в теории. Или Вы имели в виду под "предикатом" только такое свойство или отношение, которое является базовым (неопределяемым) понятием теории и для обозначения которого выделен специальный символ (например, равенство в арифметике Пеано или принадлежность в теории множеств)?
Профессор Снэйп писал(а):
Друзья! Вы всегда так бурно развиваете эти темы и такие объёмные сообщения лепите! А я вот всегда вроде и хочу сказать своё веское слово, а потом хоп --- там уже несколько страниц написано и читать их лень. Ну а вдруг там уже написали то, что ты собираешься сказать?
Если хотите сказать, не бойтесь повториться. Не думаю, что если Вы поленились прочитать всё, то это лишает Вас прав комментировать именно то, что привлекло Ваше внимание. Я, например, не обижусь и посылать Вас "прочитать всю тему с начала" не буду: при необходимости всегда можно конкретно сослаться на то место, где имено об этом было сказано.
Профессор Снэйп писал(а):
Странно, откуда такое неравнодушие к математической логике? Причём даже не к самой матлогике, а к философской мути, поднятой вокруг неё.
Не-е, не к философской мути, а именно к самой логике, к основаниям. Даже незначительные возможные изъяны в основаниях здания интересы: а то вдруг строим, строим, а потом всё из-за ма-ахонього изъяна и рухнет. Вероятность маленькая, зато стоимость риска велика.
AGu писал(а):
Но нам все равно не отвертеться от выбора теории, в которой предстоит доказывать это существование.
Бесспорно. Очевидно также, что метатеория на каком-то уровне непременно окажется неформализованной.
AGu писал(а):
А по традиции эта (мета)теория -- теория множеств (ZF или какая-то ее урезанная версия).
А вот традиция эта по-моему неудачная, и к тому же не такая уж давняя. Когда речь идёт об обоснованиях таких фундаментальных вещей, как арифметика, то делать это в рамках более богатой теории как-то странно. Это всё равно что обосновывать равенство 2*2=4 с помощью таблицы умножения.
AGu писал(а):
Математика начинается с неформальной метатеории, в непротиворечивость которой мы попросту верим. (Во всяком случае, других подходов к формализму я не знаю.) И в этой метатеории присутствуют натуральные числа во всей их (не)полноте. Основы столь же зыбки, сколь прочна наша вера в их прочность. И это всем известно. И все (ну, почти все) с этим мирятся.
Наверное, я отношусь к этим "почти". Разумеется, есть какие-то базовые (неопределяемые) понятия, которые мы просто принимаем за очевидные. Просто я считаю, что это надо делать явно, а не маскировать "псевдообоснованиями". Например, понятия "символ", "алфавит" или "строка" по-сути неопределяемы. Если Вы скажете, что "алфавит" - это "множество символов", а символ "принадлежит алфавиту", т.е. попытаетесь определить их с помощью теории множеств, то я, разумеется, напомню Вам, что сама теория множеств формализована с использованием неких символов в некоем алфавите, так что она ни в коем случае не является "первичной" по отношению к этим понятиям.
Так что обоснование арифметики хотелось бы видеть в теории, не содержащей арифметику. Ладно, пусть в теории, вводящей схему индукции, не будет хотя бы аксиом индукции. Только в таком случае обоснование арифметики имеет какой-то смысл. Если такового нет, то, по-моему, и обоснования никакого нет - лучше просто считать понятие "натурального числа" изначальным и неопределяемым.
маткиб писал(а):
Конструктивизм - это прикольно (хотя я в нём и не разбираюсь), но когда ставят его в основание математики, это не есть гут, ИМХО. И причина того, что его пытаются туда ставить, по-моему, как раз в некотором недоверии к классическим теориям, сомнении в их непротиворечивости и адекватности реальному миру.
А что в этом "не гут"? Недоверие к классическим теориям, конечно, где-то есть, но это не есть сомнение в непротиворечивости, а скорее именно в адекватности реальному миру: Похоже, что классические (неконструктивные) теории способны с уверенностью утверждать много всего такого, что в реальном мире принципиально непроверяемо.
Someone писал(а):
Вообще-то, мне встречалось мнение, что и математическую логику невозможно сформулировать, не имея априорного представления о натуральном ряде. Так что всё ещё хуже.
Любопытно, почему это вдруг? Вроде бы из логических тождеств (исчисления предикатов) аксиомы Пеано невыводимы, т.е. нельзя сказать, что в логике уже содержится арифметика?
Someone писал(а):
Сами же в следующей фразе пишете, что не остановились
Но ZFC-то остановилась, в ней понятия класса нет. А NBG, например, это уже другая формальная теория.
Someone писал(а):
Никогда ничего подобного не встречал. Может быть, дадите ссылку?
Да нет, это просто мысль, обоснований не имею. Но теорию множеств, очевидно, можно расширять во многих направлениях (не только в этом). Например, неразрешимость в ней континуум гипотезы доказана, а значит её свободно можно ввести в качестве аксиомы. Или наоборот, ввести нечто противоположное или даже более сложное (что существет ровно одна промежуточная кардинальность, или существует счётная бесконечность промежуточных кардинальностей, или существует не менее чем континуум счётных кардинальностей, или ещё что-нибудь). Всё это - разные варианты расширения теории множеств. И хотя они возможны, но мне непонятно, зачем они нужны.