Формальные теории

[SomePupil]

Недавно была пара по мат. логике. Преподаватель дала определение формальной теории. Оказываются, формальные теории задаются совокупностью символов. Потом среди наборов из этих символов выделяются формулы, а среди формул $-$ аксиомы (в аксиоматических теориях). Я как услышал это, сразу спросил: "Это говорится про множества символов? " Преподаватель ответила "про совокупности символов". Я переспросил: "Значит, все-таки про множества символов?" После нескольких итераций преподаватель невольно согласилась, что говорится о множествах.

Потом зашла речь про правила вывода. Оказывается, это отношения, заданные на формулах. Я, конечно же, спросил: "А не декартовы ли это произведения?" На что преподаватель решила не отвечать.

Дело вот в чем: без аппарата формальных теорий не будет самогона мы не можем формализовать теорию множеств. И, наоборот, без формальной теории множеств мы не можем строго определить формальные теории! Замкнутый круг, небо вокруг, в общем, рисунок мальчишки.

Это ведь правда, правда? Если это окажется правдой, то моя жизнь станет намного интересней, чем я думал.

[Aritaborian]

Остап Бендер писал(а):

— Только вы, дорогой товарищ из Парижа, плюньте на все это.
— Как плюнуть?
— Слюной, как плевали до эпохи исторического материализма.

[mustitz]

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

[vpb]

SomePupil
Знаете, многие люди, в том числе в пределах форума, слишком шибко интересуются вопросами оснований и формализма, ну и слегка крыша едет. Это в основном чисто схоластика, на уровне "сколько чертей может уместиться на острие иглы". А ведь в математике так много интересного и содержательного! Так что присоединяюсь к совету Aritaborian. Я, как буквы ZFC увижу, так аж дурно становится!

-- 29.03.2018, 17:45 --

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

[mihaild]

(Оффтоп)

Ну а мне дурно становится от формулировок вида "псевдотензоры как-то ведут себя при преобразовании координат". Suum cuique.

Чтобы формализовывать выводы, нам нужна какая-то теория, умеющая описывать работу с конечными строками. Мы ее конечно можем формализовать в самой себе, но изначально строить придется всё равно неформально. Мы начинаем без формализмов, поэтому первые формализым придется вводить неформально:)

[arseniiv]

vpb в сообщении #1300392 писал(а):

А ведь в математике так много интересного и содержательного!

В матлогике тоже. Вон теоремы о компактности не очень-то тривиальны.

vpb в сообщении #1300392 писал(а):

Я, как буквы ZFC увижу, так аж дурно становится!

Прекрасно, но это не ответ на совершенно разумные вопросы ТС.

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

-- Чт мар 29, 2018 20:52:09 --

Ну и к словам mihaild.

-- Чт мар 29, 2018 20:56:03 --

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

[vpb]

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

Вон теоремы о компактности не очень-то тривиальны

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

[epros]

SomePupil в сообщении #1300361 писал(а):

Преподаватель ответила "про совокупности символов". Я переспросил: "Значит, все-таки про множества символов?" После нескольких итераций преподаватель невольно согласилась, что говорится о множествах.

Я бы сказал: "о строках символов".

SomePupil в сообщении #1300361 писал(а):

Дело вот в чем: без аппарата формальных теорий мы не можем формализовать теорию множеств. И, наоборот, без формальной теории множеств мы не можем строго определить формальные теории! Замкнутый круг, небо вокруг, в общем, рисунок мальчишки.

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

[Markiyan Hirnyk]

SomePupil
Обьяснение простое - теория, например, исчисление предикатов, формализована, а ее метатеория - нет. Можно формализовать метатеорию, но тогда метаметатеория не формализована.

[Anton_Peplov]

SomePupil в сообщении #1300361 писал(а):

И, наоборот, без формальной теории множеств мы не можем строго определить формальные теории!

Здесь ошибка.

Как уже неоднократно было сказано выше разными словами, строку $love$ можно, конечно, определить в понятиях теории множеств. Теория множеств это умеет, как и многое другое. Правда, для этого, если представлять кортежи в виде множеств по методу Куратовского, придётся считать строку $love$ множеством $\{\{l\}, \{l, o\}, \{l, o, v\} , \{l, o, v, e\}\}$ (бр-р-р, мамочка! зачем такие извращения, когда нужно просто поговорить о любви!).

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

[epros]

Anton_Peplov в сообщении #1300444 писал(а):

придётся считать строку $love$ множеством $\{\{l\}, \{l, o\}, \{l, o, v\} , \{l, o, v, e\}\}$

А как быть, если буквы повторяются?

[iifat]

epros в сообщении #1300454 писал(а):

как быть, если буквы повторяются?

Странный вопрос. Вообще-то, этот способ работает и с повторяющимися буквами. Я, правда, не уверен, что Anton_Peplov точно его воспроизвёл для кортежа из четырёх элементов.

[Anton_Peplov]

epros в сообщении #1300454 писал(а):

А как быть, если буквы повторяются?

Да это я на ночь глядя запутался в этих извращениях, там нужно аккуратно определение пары Куратовского обобщать, а я неаккуратно. $(l, o, v, e) = ((l, o, v), e)=(((l, o), v), e)$, где скобки означают упорядоченную $n$-ку, а упорядоченная пара определяется по Куратовскому. Теперь как будто всё в порядке. Говорю же, непотребство адское.

[arseniiv]

(Начато перед предыдущим сообщением.)

Давайте не будем отвлекаться на представление кортежей, это же очевидно оффтопный вопрос. Обычно принято определять $(x,y,z) := (x, (y,z))$, $(x,y,z,w) := (x, (y,z,w))$ и т. д., но можно, конечно, выбрать и много других способов таких, чтобы, в отличие от приведённого, $(x,x) \ne (x,x,x,x)$, и разбирательство в них в этой теме вряд ли нужно. Заодно можно было бы поговорить о том, чему принимать равным пустой кортеж (как правило, $() := \varnothing$), считать ли одноэлементные кортежи $(x) = x$, и не лучше ли взять лисповый способ представления списков, определяя $(x) = [x,()]$ и $(x,y) = [x,[y,()]]$, где $[,]$ далее (кроме определения всех остальных кортежей через первый элемент и остаток, как и с первыми двумя здесь) практически не используется.

Anton_Peplov в сообщении #1300462 писал(а):

Говорю же, непотребство адское.

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

[SomePupil]

(Оффтоп)

vpb, давайте не будем затрагивать тему об интересах (и о вкусах фломастеров, поглощающих разные частоты видимого спектра). Все-таки "Свободный полет" $-$ серьезный подфорум, это не какой-нибудь там Пургаторий :)

Огромное спасибо всем ответившим, было интересно. Кстати, физики тоже сказали мне (через ЛС) про метаязык и метатеорию.