Что такое метаматематика?

[LaTeXScience]

Хочу разобрать что же такое ТОЧНО метаматематика.
Вроде бы оно так определяется:

Цитата:

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

Цитата:

Мета-теория - теория, предметом которой является какая-то другая теория.

Но это все не точные определения. Они не дают ответов на следующие вопросы.
Сколько метаматематик у математики?
Какие понятие входят в метаматематику? Какие теоремы? Какие аксиомы?
Какая мета-теория у теории множеств? Может ли теория множеств быть мета-теорией самой себя? Может ли лямбда-исчисление быть мета-теорией теории множеств? Будет ли отличаться теория множеств у которой мета-теория - теория множеств от теории множеств у которой мета-теория - лямбда-исчисление?
Метаматематика это религия? Почему мы верим, что она верна?
Если теория множеств мета-теория самой себя, то разве мы не получим "порочный круг"? Чтобы в первый раз определить теорию множеств, мы не можем ее использовать, потому что она еще не создана.

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

[Dan B-Yallay]

Метаматематика

[LaTeXScience]

Dan B-Yallay в сообщении #461975 писал(а):

Метаматематика

Там одна "вода" и нет ответов на мои вопросы.

[Dan B-Yallay]

# Энгелер Э. Метаматематика элементарной математики. — М.: Мир, 1987. — 128 с.
# Клини С. К. Введение в метаматематику / Пер. с англ. — М.: Иностранная литература, 1957. — 526 с.

[LaTeXScience]

Dan B-Yallay в сообщении #461978 писал(а):

# Энгелер Э. Метаматематика элементарной математики. — М.: Мир, 1987. — 128 с.
# Клини С. К. Введение в метаматематику / Пер. с англ. — М.: Иностранная литература, 1957. — 526 с.

Здесь тоже нету.

-- 24.06.2011, 23:44 --

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

[Someone]

Метатеория - это теория, которая используется для описания языка предметной теории. Чаще всего в такой роли выступает естественный язык. Выбор метатеории достаточно произволен, лишь бы в ней было достаточно средств для такого описания. Годится и арифметика, и теория множеств. На предметную теорию выбор метатеории никак не влияет. Вполне допустимо использовать арифметику как метатеорию для арифметики или теорию множеств как метатеорию для теории множеств, но нужно помнить, что метатеория и предметная теория - это разные теории, даже если они одинаково называются и имеют "одинаковые" наборы аксиом.

[AlexNew]

Цитата:

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

Не все верят. Кое кто занимается конструктивной математикой, однако некоторыми теоремами приходится пожертвовать.

[Someone]

AlexNew в сообщении #461992 писал(а):

Не все верят.

Во что? В метаматематику? А зачем в неё верить?

AlexNew в сообщении #461992 писал(а):

Кое кто занимается конструктивной математикой, однако некоторыми теоремами приходится пожертвовать.

Конструктивная математика - это тоже математика. Я только не понял, почему конструктивная математика противопоставляется метаматематике. Никто не запрещает использовать, например, конструктивный рекурсивный анализ в качестве метатеории.

[LaTeXScience]

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

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

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

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

Чаще всего в такой роли выступает естественный язык.

Что Вы имеете в виду? Язык и теория - разные вещи.

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

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

Так значит нужно в определении мета-теории написать, что в ней обязательно должно хватать средств. Кстати, что это означает "лишь бы было достаточно средств"? Как мы это можем определить для какой-то теории, что в ней хватает или не хватает средств для определения какой-то еще не созданной теории? Мы же не можем это определить для еще не существующей исследуемой теории.
Хорошо, если я хочу определить какую-то новую теорию и использовать ее же в качестве мета-теории (для ее же определения), то как я это смогу сделать?
Вы знаете что такое bootstrapping в программировании? Это, например, когда язык программирования пишут на сомом себе. Так вот, это можно сделать (сам писал когда-то интерпретатор лиспа на лиспе), но первая реализация, выходит, должна быть написана на каком-то другом языке. Вообще, корректна ли подобная аналогия? Если да, то понятие "мета-теория" должно определяться более точно, учитывая невозможность определить "первую реализацию" теории с помощью самой себя.

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

На предметную теорию выбор метатеории никак не влияет.

Откуда это следует? Я интуитивно понимаю, что не влияет, но почему так?

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

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

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

-- 25.06.2011, 02:15 --

Кстати, и в каком смысле "разные", если они, допустим, одинаковые? Как это утверждение точно сформулировать?

[AlexNew]

Someone писал(а):

Конструктивная математика - это тоже математика.

ну да, она такая разная )) зависит от того как определить это слово. Например этим словом "математика" можно назвать форму психического растройства.

В вопросе был фраза про веру, на эту фразу и было оставлено замечание. Не все верят в бесконечности.

[LaTeXScience]

AlexNew в сообщении #461992 писал(а):

Кое кто занимается конструктивной математикой, однако некоторыми теоремами приходится пожертвовать.

Насколько я понимаю, конструктивная математика - это та же математика, но в которой помимо непротиворечивости теорий существует еще одно дополнительное требование - "конструктивность". У конструктивной математики разве нет мета-теории? А как там тогда?

[Someone]

LaTeXScience в сообщении #462099 писал(а):

У конструктивной математики разве нет мета-теории?

Ну почему же нет?

LaTeXScience в сообщении #462001 писал(а):

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

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

Е.Расёва, Р.Сикорский. Математика метаматематики."Наука", Москва, 1972.

Там Вы, в частности, обнаружите, что язык формализованной теории включает алфавит, термы и формулы (правила образования термов и формул, собственно, и образуют синтаксис). Понятие "верной" (истинной?) формулы связано с интерпретацией языка, а интерпретация не является частью языка формализованной теории (противоположный подход фактически запрещает рассматривать какие-либо интерпретации теории, кроме изначально заданной, что не есть хорошо). Формализованная теория включает язык, операцию присоединения следствий (вместе это даёт дедуктивную систему) и множество математических аксиом.

LaTeXScience в сообщении #462001 писал(а):

Что Вы имеете в виду? Язык и теория - разные вещи.

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

LaTeXScience в сообщении #462001 писал(а):

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

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

LaTeXScience в сообщении #462001 писал(а):

Почему допустимо?

Потому что арифметика (и, тем более, теория множеств) достаточно богата для этого. А кто может запретить Вам взять арифметику и описать в ней, например, арифметику, теорию множеств или любую другую формализованную теорию?

LaTeXScience в сообщении #462001 писал(а):

Вы знаете что такое bootstrapping в программировании? Это, например, когда язык программирования пишут на сомом себе.

Что пишут-то? Компилятор? Ну да, если какой-то компилятор языка уже есть, то можно на этом языке написать новый компилятор этого же языка. Или откомпилировать его вручную (http://en.wikipedia.org/wiki/Bootstrapping_%28compilers%29). Да Вы же сами об этом пишете. Вы попробуйте на ещё не существующем языке описать его же (не компилятор, а алфавит, синтаксис и т.д.).

LaTeXScience в сообщении #462001 писал(а):

Откуда это следует? Я интуитивно понимаю, что не влияет, но почему так?

Предметная теория ведь "не имеет ни малейшего понятия" о том, в какой метатеории она описана. У предметной теории свои объекты, аксиомы и правила вывода, у метатеории - свои. Ну, если использовать Вашу аналогию с языками программирования: язык программирования "не знает", на каком языке написан его компилятор.

LaTeXScience в сообщении #462001 писал(а):

Кстати, и в каком смысле "разные", если они, допустим, одинаковые? Как это утверждение точно сформулировать?

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

[LaTeXScience]

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

Ну почему же нет?

Не знаю. Может AlexNew знает?

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

Там Вы, в частности, обнаружите, что язык формализованной теории включает алфавит, термы и формулы (правила образования термов и формул, собственно, и образуют синтаксис).

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

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

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

Какие именно теории в нем описаны, у них есть название, можете привести пример?

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

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

А если бы человечество разговаривало на каком-нибудь формальном языке с какими-нибудь формальными теориями? Кстати, может в будущем так и будет.

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

Потому что арифметика (и, тем более, теория множеств) достаточно богата для этого.

А можно посмотреть в живую как это делается (использование только арифметики в качестве описания арифметики), чтобы я лучше понял?
Интересно, а сможет ли человек, не знающий теории множеств, понять ее по описанию, в котором мета-теория есть теория множеств? Сколько ему нужно будет сделать циклов чтения чтобы что-то понять (допустим, что он очень сообразительный человек)?

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

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

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

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

язык программирования "не знает", на каком языке написан его компилятор.

Да, теперь я понял, что не влияет.

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

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

Т.е. мы не можем, например, в теории множеств ZF определить следующие множества:
$\{n\in\mathbb{N}:n<K\}$, где $K$ - число аксиом в ZF;
$2^M$, где $M$ - множество аксиом ZF;
множество имен всех множеств;
множество всех формул ZF;
множество, состоящее из символов первой аксиомы ZF;
множество известных доказательств равномощности $\mathbb{N}$ и $\mathbb{Q}$.
Я правильно понял?

[Someone]

LaTeXScience в сообщении #462213 писал(а):

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

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

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

LaTeXScience в сообщении #462213 писал(а):

Какие именно теории в нем описаны, у них есть название, можете привести пример?

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

LaTeXScience в сообщении #462213 писал(а):

А можно посмотреть в живую как это делается (использование только арифметики в качестве описания арифметики), чтобы я лучше понял?

Ну, это будет жутко кропотливое и громоздкое дело. Сначала нужно определить алфавит предметной теории, то есть, указать натуральные числа, которые будут играть роль символов. Затем построить нумерацию слов в этом алфавите, и построить функции, позволяющие по номеру слова определять входящие в него символы. Построить функции, определяющие, какие из слов являются термами и формулами. Построить функции, осуществляющие всякие необходимые манипуляции с формулами (например, по кодам формул $\varphi$ и $\psi$ определить коды формул $\neg\varphi$, $\varphi\vee\psi$ и т.п., и наоборот, по коду "сложной" формулы определить коды её компонентов). То же сделать для правил вывода. Указать список кодов аксиом (определить функцию, которая по номеру аксиомы будет определять её код). Закодировать последовательности формул и построить функции, определяющие, является ли последовательность формул доказательством, и чего именно. И, вероятно, ещё много чего, поскольку я вряд ли вспомнил всё, что может потребоваться.

LaTeXScience в сообщении #462213 писал(а):

Т.е. мы не можем, например, в теории множеств ZF определить следующие множества:
$\{n\in\mathbb{N}:n<K\}$, где $K$ - число аксиом в ZF;
$2^M$, где $M$ - множество аксиом ZF;
множество имен всех множеств;
множество всех формул ZF;
множество, состоящее из символов первой аксиомы ZF;
множество известных доказательств равномощности $\mathbb{N}$ и $\mathbb{Q}$.
Я правильно понял?

Правильно.