Допускает ли язык логики противоречивые утверждения?

[newtonisa]

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

Я не понимаю, что значит "заранее". В математике времени нет.

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

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

А так.

Возможно это проблемы философских оснований математики.
Система, модель, не может работать, если в нее не внесены ограничения, а формализация -- это и есть ограничения. Если Вы описали систему, значит Вы ее уже формализовали.

-- 03.04.2018, 01:19 --

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

В математике времени нет.

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

[mihaild]

warlock66613 в сообщении #1301332 писал(а):

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

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

newtonisa в сообщении #1301329 писал(а):

Но ведь, положа руку на сердце, "чистой" неформальной системы существовать не может.

Никак не могу согласиться. Готов согласиться, что не может существовать "чистой формально" системы:)

[Pphantom]

newtonisa заблокирован как клон.

[mihaild]

newtonisa в сообщении #1301334 писал(а):

В машине поста-тьюринга времени тоже нет?

Тоже. Сама по себе МТ - это вообще несколько конечных алфавитов и функция. Протокол работы МТ - это тоже функция из начального отрезка натурального ряда или всего ряда в конфигурации.

"Времени нет" в том смысле, что всё что нам нужно "существует" или "не существует" с самого начала. Когда мы неформально говорим о том, что что-то изменяется - формально это означает, что мы рассматриваем какую-то функцию.

[warlock66613]

mihaild в сообщении #1301335 писал(а):

как раз то, что примерно понятно, как формализовывать

Да, потому что эти способы формализации так подогнаны, чтобы более или менее воспроизводить математические рассуждения. Но если содержательная, интересная математическая теория (а Кантор ведь доказал ряд весьма интересных теорем) не формализуема — это не проблема теории, это проблема тех, что хочет эту теорию формализовать. У Додекинда вроде бы не было проблем с пониманием Канторовских рассуждений. Теорию множеств Кантора удалось аксиоматизировать (и одновременно содержательно развить) в виде ZFC-как-обычной-неформальной-аксиоматической-теории, то есть полностью «легализовать» в статусе математической теории, и «формализовать» в виде ZFC-как-формальной-теории-первого-порядка, то есть объекта изучения специального раздела математики, который называется математической логикой.

Нет, разумеется, несмотря на то, что нельзя путать и отождествлять математические теории с формальными теориями (ведь так?), последние могут быть полезны для первых в качестве эвристики. Если у нас есть 1000 теорий, и все формализуемые, и вдруг появляется 1001-я неформализуемая, это можно воспринять как сигнал, что с теорией что-то не то. Но теория множеств Кантора — явно не этот случай.

[arseniiv]

newtonisa в сообщении #1301334 писал(а):

Возможно это проблемы философских оснований математики.
Система, модель, не может работать, если в нее не внесены ограничения, а формализация -- это и есть ограничения.

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

[Aritaborian]

Поинтересовался у Википупии, как поживают Бурбаки, и с некоторым удивлением узнал, что

Вика писал(а):

More importantly, the first four chapters of a completely new book on algebraic topology were published in 2016. The new material from 2012 and 2014 address some references to forthcoming books in the book on Lie Groups and Algebras; there remain other such references (some very precise) to expected additional chapters of the book spectral theory.

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

[mihaild]

warlock66613 в сообщении #1301340 писал(а):

Но если содержательная, интересная математическая теория (а Кантор ведь доказал ряд весьма интересных теорем) не формализуема — это не проблема теории, это проблема тех, что хочет эту теорию формализовать.

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

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

Aritaborian в сообщении #1301461 писал(а):

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

А metamath не этим ли занимается?

[warlock66613]

mihaild в сообщении #1301518 писал(а):

Если у нас есть теория, которую можно формализовать неэквивалентными способами - в том смысле, что разные математики на просьбу расписать строже дадут неэквивалентные формулировки

Это мне совсем непонятно. Математики не занимаются формализациями своих теорий, так что просьба не выглядит осмысленным действием. Разумеется расписать построже можно, но ведь даже после максимального расписывания теория не превратится в формальную теорию. Ведь для построения формальной теории нужно вводить иные, чуждые самой теории понятия — для начала, алфавит, потом понятие формулы — формулы в формальном смысле, то есть выражения, строки, построенной из алфавитных символов, в то время как формулы математической теории являются объектом совсем другого рода.

[mihaild]

Возможно у нас с вами разные понятия либо о "расписать построже", либо о "формальной теории".
Формальная теория - это сигнатура плюс список аксиом (т.е. алфавит и набор строчек в этом алфавите). Можете привести какой-нибудь простой пример неформальной теории?
Или вы про то, что, скажем, теория групп в основном занимается утверждениями, которые нельзя выразить в сигнатуре $(e, \cdot, =)$?

[Aritaborian]

mihaild в сообщении #1301518 писал(а):

А metamath не этим ли занимается?

Да, спасибо за напоминание. Как-то я о них забыл ;-( Да и Вольфрам, например, тоже апологет этого направления. Но это по-любому не мейнстрим, согласитесь.

[warlock66613]

Неформальная ZFC — теория, в которой существует единственный тип объектов — множества и единственный предикат $\in$. Множества и отношение принадлежности подчинены следующим девяти аксиомам ZF1–ZF9.
ZF1 (Аксиома экстенсиональности). Два множества равны, $x = y$, если они содержат одни и те же элементы, т.е. если $z \in x \Leftrightarrow z \in y$.
Определим отношения включения $x \subseteq y$ как $z \in x \Rightarrow z \in y$. В этих обозначениях $x = y$ в том и только том случае, когда $x \subseteq y$ и $x \supseteq y$.
Множество, не содержащее ни одного элемента, называется пустым множеством и обозначается $\varnothing$.
ZF2 (Аксиома существования). Существует пустое множество.
ZF3 (Аксиома неупорядоченных пар). Для любых двух вещей $x$ и $y$ существует множество $\{x, y\}$, единственными элементами которого являются $x$ и $y$.
ZF4 (Аксиома объединения). Для любого множества множеств $x$ существует объединение $\bigcup y, y \in x$.
ZF5 (Аксиома бесконечности). Существует такое множество $\omega$, что $\varnothing \in \omega$ и для любого $x \in \omega$ имеем $\{x, \{x\}\} \in \omega$.
ZF6 (Аксиома подстановки). Допустим, что для любого $x$ существует единственный $y$ такой, что $F (x, y)$. Тогда для любого множества $z$ существует единственное множество $u$, состоящее из всех $y$ таких, что $x \in z$ и $F (x, y)$.
ZF7 (Аксиома степени). Для любого множества $x$ существует множество $z$ такое, что $y \in z$ в том и только том случае, когда $y \subseteq x$.
ZF8 (Аксиома выбора). Пусть $f: X \longrightarrow Y$ — сюръективное отображение. Тогда существует отображение $g: Y \longrightarrow X$ такое, что для любого $y \in Y$ имеет место равенство $f (g(y)) = y$.
ZF9 (Аксиома регулярности). Пусть $y \ne \varnothing$. Тогда существует такой элемент $x \in y$, что для любого элемента $z \in y$ выполняется $z \notin x$.

В отличие от формальной ZFC, здесь нет какого-то фиксированного алфавита и не определены правила построения формул. Вместо этого, предложения формулируются на естественном языке, а единственным критерием правильности формул служит их понятность. Также, теория не содержит логических аксиом и не специфицирует правил вывода — а значит, она не является теорией первого порядка.

[mihaild]

А встречаются ли на практике (в хороших источниках) рассуждения в ZFC, по которым непонятно, как преобразовать их в последовательнсть формул?
Или если попросить разных математиков записать какую-нибудь из аксиом формулой, то я ожидаю, что они напишут примерно одно и то же. Это свойство я имел в виду, говоря, что "понятно, как формализовывать".
(и если определять $\subseteq$, то и $\bigcup$ тогда тоже)

[warlock66613]

mihaild в сообщении #1301575 писал(а):

если попросить разных математиков записать какую-нибудь из аксиом формулой, то я ожидаю, что они напишут примерно одно и то же

Да, но формулы (вообще записи) для математической теории — сугубо вспомогательная вещь. Они нужны только потому, что 1) они служат средством усиления телепатии 2) они служат средством усиления ясности мышления. Если бы люди не были идиотами, не способными ясно мыслить, и могли напрямую передавать из мозга в мозг сложные невербализованные мыслеформы, записи вообще были бы не нужны, и разница между формальными теориями и математическими была бы видна гораздо сильнее.

mihaild в сообщении #1301575 писал(а):

и если определять $\subseteq$, то и $\bigcup$ тогда тоже

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

[mihaild]

warlock66613 в сообщении #1301576 писал(а):

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

Встречается ли на практике в статьях или хороших учебниках использование значков без определения, что они значат?

warlock66613 в сообщении #1301576 писал(а):

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

Или наоборот - если бы люди не были идиотами, неспособными удержать в активной памяти даже несколько килобайт символов, то неформальных теорий не было бы вообще.