Метатеоремы

[oleg.k]

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

1. Как можно верить таким нефинитным метатеоремам?
2. Какие нефинитные средства можно использовать при доказательстве этих метатеорем?
3. Где гарантия, что эти нефинитные средства не приведут к парадоксам?

[arseniiv]

Без примеров как-то грустно. Но вообще никакого универсального общего мнения тут нет: есть например ультрафинитисты.

Кроме того если вы хотите для вопросов 2 и 3 чего-то точного, может понадобиться доказывать метаметатеоремы, потому что придётся формализовать метатеорию (чтобы классифицировать её средства и т. п.) и аналогично до бесконечности.

[oleg.k]

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

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

Это бессмысленно. Средства метаметатеории будут неформализованы, поэтому доверия к метатеории (как и к предметной теории) не будет. Как выйти из этого замкнутого круга?

-- 22.11.2019, 14:00 --

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

Кроме того если вы хотите для вопросов 2 и 3 чего-то точного

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


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


По сути мы одни эмпирические соображения заменили другими (тоже эмпирическими). Ради чего?

-- 22.11.2019, 14:04 --

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

Без примеров как-то грустно.

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

[mihaild]

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

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

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

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

Как можно верить этой метатеореме?

Какой метатеореме-то? Со строками обычно работают в рамках теории множеств.
А в исчислении, в котором мы формулируем теорию множеств, никакие бесконечные строки не нужны.

[arseniiv]

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

Это бессмысленно. Средства метаметатеории будут неформализованы, поэтому доверия к метатеории (как и к предметной теории) не будет. Как выйти из этого замкнутого круга?

Никак.

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

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

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

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

Из практики известно, что наивная теория множеств, несмотря на парадоксы, в принципе подходит для многих разделов математики.

Тут кстати может быть недопонимание, потому что многие под наивной теорией понимают такую, где как минимум исторически известных парадоксов нет, потому что «наивная» не обязано значить «с неограниченной схемой аксиом выделения».

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

Ну дак пусть она и будет в основании математики. Математику тогда можно будет считать эмпирической наукой, где основной критерий истинности - соответствие с опытом.

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

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

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

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

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

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

[oleg.k]

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

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

Да я и не против. Но только до тех пор, пока все рассуждения исключительно финитны.


По поводу рассуждений - отдельная история. Вот допустим есть следующее предложение: "если в строке, состоящей из 7 символов некоторого алфавита, заменить каждый экземпляр символа $x$ на символ $y$ и не производить других замен, то получится строка, в которой нету символа $x$". Верно ли я понимаю, что это метатеорема? Если да, то как ее доказать? Можно попытаться например методом от противного. Допустим в получившейся строке на некоторой позиции стоит символ $x$. В исходной строке на этой позиции не мог находиться символ $x$, т.к. после замены в получившейся строке стоял бы символ $y$. Значит в исходной строке на этой позиции стоял символ, отличный от $x$. Но т.к. других замен по условию не было, то на этом месте в получившейся строке должен находиться символ, отличный от $x$. Получили противоречие. Метатеорема доказана. Тогда в связи с этим вопрос: почему я могу пользоваться методом от противного? И что означает "доказательство" по отношению к метатеореме? Есть ли конкретный список приемов (наподобие метода от противного), которыми (и только которыми) можно пользоваться?

-- 22.11.2019, 15:05 --

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

Какой метатеореме-то?

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

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

Со строками обычно работают в рамках теории множеств.

Я думал, что на этом этапе никакой теории множеств еще нету...

-- 22.11.2019, 15:12 --

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

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

Я совсем не против экспериментов. Вот нарисовал я 100500 треугольников, померял в них углы и получил, что сумма углов в каждом из них равна 180 градусов. Отличный эксперимент. Но что такое "доказать в точности"? Доказательство из учебника Атанасяна (про прямую, параллельную одной из сторон треугольника) подойдет?

[arseniiv]

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

По поводу рассуждений - отдельная история. Вот допустим есть следующее предложение: "если в строке, состоящей из 7 символов некоторого алфавита, заменить каждый экземпляр символа $x$ на символ $y$ и не производить других замен, то получится строка, в которой нету символа $x$". Верно ли я понимаю, что это метатеорема?

Быть метатеоремой — свойство не утверждения самого по себе. Пока мы говорим о просто строках, никак не связанных с чем-то ещё, это вполне себе просто теорема.

[mihaild]

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

Верно ли я понимаю, что это метатеорема?

Метатеоремы - это теоремы о какой-то теории. При этом они сами могут быть теоремами формальной или неформальной теории. И рассуждения про строки формализуются в ZF (и даже в PA, хотя там будет много возни с кодированием строк числами).
Метатеорема - это, например, теорема о дедукции: $\Gamma, A \vdash B$ тогда и только тогда, когда $\Gamma \vdash A \rightarrow B$. Доказывается с помощью индукции по построению формулы.

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

Я думал, что на этом этапе никакой теории множеств еще нету

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

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

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

Есть разные мнения по этому вопросу.
Большая часть математики основана, в конечном итоге, на классическом исчислении предикатов, список аксиом и правил вывода которого можно найти, например, в "Языках и исчислениях" Верещагина и Шеня.

[oleg.k]

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

Метатеоремы - это теоремы о какой-то теории.

Допустим, подразумевалось, что есть какой-то алфавит, какие-то строки в нем назвали формулами, и часть формул назвали аксиомами. Рецепт формальной системы готов. Смотрим на строку из 7 символов и формулируем то самое предложение. Оно является метатеоремой?

-- 22.11.2019, 15:47 --

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

-- 22.11.2019, 15:53 --

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

[arseniiv]

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

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

Смотря когда. Мы хотим, чтобы «быть доказательством» было объективным свойством какого-то рассуждения, но рассуждения всегда идут в каком-то контексте.

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

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

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

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

Это и значит «о теории», собственно.

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

-- Пт ноя 22, 2019 18:10:51 --

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

Смотрим на строку из 7 символов и формулируем то самое предложение. Оно является метатеоремой?

Оно ведь не оперирует какими-то вещами, относящимися к формализуемой теории, так что нет, не относится. Это теорема о языках строк, притом если нас интересуют только строки из 7 символов, даже и теоремой о языках её назвать язык не поворачивается.

[oleg.k]

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

отношений (не обязательно бинарных) на формулах.

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

[arseniiv]

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

-- Пт ноя 22, 2019 19:04:17 --

Всё это в конечном счёте вынуждает возможность финитного описания.

[Someone]

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

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

Утверждение об объектах предметной теории является её теоремой. Причём тут метатеория? Она об объектах предметной теории ничего не знает.

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

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

Все перечисленные "предметы" ни в коем случае не являются объектами предметной теории. Они являются объектами той метатеории, в которой мы формализовали предметную теорию. Например, объектами арифметики являются натуральные числа. Даже если в качестве метатеории взята арифметика, в которой объекты тоже называются натуральными числами, нужно не забывать, что это другие натуральные числа.

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

[oleg.k]

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

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

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

[arseniiv]

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