Есть ли синтаксис в математике?

[errnough]

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

Xaositect в сообщении #302437 писал(а):

1.Буквами $p$ c индексами будем обозначать атомарные высказывания. Атомарные высказывания являются высказываниями.
2. Буквой $\mathrm{t}$ будем обозначать тождественно истинное высказывание.

1. Нет определения высказыванию.
2. Неопределяемые высказывания, тем не менее, делятся на атомарные и истинные.
3. Из рассмотрения исключены неопределенные высказывания (атомарные?) и ложные.
4. Тождественно — если не указана пара в тождестве, то подразумевается тождественность самому себе.

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

Xaositect в сообщении #302437 писал(а):

Интерпретацией $I$ назовем отображение, приписывающее каждому высказыванию $\varphi$ его истинностное значение $\varphi_I$, которое может быть равным $\mathbf{True}$ или $\mathbf{False}$.

Уточню, заменяем "$p$ суть ложное высказывание" на "припишем $p$ ложное значение"?

[Xaositect]

errnough в сообщении #302602 писал(а):

1. Нет определения высказыванию.

Там внизу, в определении интерпретации, пояснения.

errnough в сообщении #302602 писал(а):

3. Из рассмотрения исключены неопределенные высказывания (атомарные?) и ложные.

Высказываниями называется только те предложения, которые могут являться истинными либо ложными. "Эталонно" ложным является $\neg\mathrm{t}$.

errnough в сообщении #302602 писал(а):

Может, тождественность подразумевается между "высказыванием" и "значением" истина?

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

errnough в сообщении #302602 писал(а):

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

Существуют ложные в конкретной интерпретации высказывания, а также ложные в любой интерпретации (их обычно называют противоречивыми, примером такого является $\neg\mathrm{t}$).

Содержательно, интерпретация есть некоторое "состояние" того, о чем мы говорим. Пусть у нас есть высказывание "Цезарь умер". Соответственно, в теории они соответствуют какому-то атомарному высказыванию $p_1$. Сейчас оно истинно - это одна интерпретация теории, а до смерти Цезаря оно было ложно - это другая интерпретация. Высказывания, которые истинны в любой интерпретации, например, $p_1\equiv p_1$, важны потому, что они выражают некоторый логический закон, истинный всегда. Это и есть, как я уже замечал, asserted propositions в Principia Mathematica.

-- Пт мар 26, 2010 13:15:50 --

errnough в сообщении #302602 писал(а):

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

Контекст тот же, я просто понимаю его через призму "Введения в метаматематику" и университетского курса логики.

[errnough]

Нет, всё равно не понимаю. Попробовал поиграться в уме в терминах предложенного. На мой взгляд, это работать не будет.

Пусть $\varphi$ и $\psi$ — высказывания, тогда учитывая Ваше "Никакие другие формулы высказываниями не являются", формула $\varphi(\psi)$ высказыванием не является.

Это означает, что по поводу одного высказывания другие высказывания не допускаются. Это бессмыслица не только для практики, но даже внутри самой теории. Полный запрет на вывод заключений. И невозможность выполнить действия, декларируемые в теории дальше:

Пусть $\psi$ = "электрон суть частица" — атомарное высказывание. Рассматривая Ваше: "атомарным высказываниям припишем истинностные значения произвольно", убеждаемся, что это невозможно сделать в рамках Вашей же теории, ведь придется сказать: «"электрон суть частица" это истинное высказывание». А это есть формула вида $\varphi(\psi)$.

В реальности: кто мне может запретить один трехполюсный переключатель поставить после другого или перед другим? Какое дело последнему переключателю, сколько раз до него переключалось? Вся цифровая логика выпадает из рассмотрения.

Предложение заменить слова "$\psi$ это истинное высказывание" словами "интерпретируем" или "припишем $\psi$ истинностное значение «истина»" выглядит как попытка что-то скрыть, поскольку конструктивных мотивов для этого не видно.

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

---

Здесь вот какой момент странно выглядит. Сначала мы пользуемся роскошью аксиоматики не определять основные понятия, а именно, понятие "высказывание", обозначим его для ясности, $P$. А затем попробуй докажи, что еще одно вводимое в середину теории, тоже неопределяемое понятие, "интерпретация" $I$, не есть полное тождество по всем признакам внутри теории для неопределяемого "высказывания" $P$. Одно и то же обозначив разными буквами, можно много наворотить... Такая вольность позволительна только благодаря пресечению всяких попыток внутри аксиоматических теорий получить определения для неопределяемых понятий.

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

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

[Xaositect]

errnough в сообщении #302688 писал(а):

Нет, всё равно не понимаю. Попробовал поиграться в уме в терминах предложенного. На мой взгляд, это работать не будет.

Это работает. То есть не это, а более сложные теории, представленные в похожей форме.

Цитата:

Пусть $\varphi$ и $\psi$ — высказывания, тогда учитывая Ваше "Никакие другие формулы высказываниями не являются", формула $\varphi(\psi)$ высказыванием не является.

Да. Эта модель не для произвольных пропозициональных функций, а только для $\neg$ и $\equiv$. При желании ее можно расширить.

Цитата:

Пусть $\psi$ = "электрон суть частица" — атомарное высказывание. Рассматривая Ваше: "атомарным высказываниям припишем истинностные значения произвольно", убеждаемся, что это невозможно сделать в рамках Вашей же теории, ведь придется сказать: «"электрон суть частица" это истинное высказывание». А это есть формула вида $\varphi(\psi)$.

Это есть формула $\psi\equiv\mathrm{t}$, т.е. "$\psi$ имеет ту же истинность, что и истинное высказывание", иными словами "$\psi$ истинно".

Цитата:

В реальности: кто мне может запретить один трехполюсный переключатель поставить после другого или перед другим? Какое дело последнему переключателю, сколько раз до него переключалось? Вся цифровая логика выпадает из рассмотрения.

Для логики у нас есть константа $\mathrm{t}$ и связки $\neg$ и $\equiv$

Цитата:

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

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

Цитата:

Здесь вот какой момент странно выглядит. Сначала мы пользуемся роскошью аксиоматики не определять основные понятия, а именно, понятие "высказывание", обозначим его для ясности, $P$. А затем попробуй докажи, что еще одно вводимое в середину теории, тоже неопределяемое понятие, "интерпретация" $I$, не есть полное тождество по всем признакам внутри теории для неопределяемого "высказывания" $P$. Одно и то же обозначив разными буквами, можно много наворотить... Такая вольность позволительна только благодаря пресечению всяких попыток внутри аксиоматических теорий получить определения для неопределяемых понятий.

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

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

Я же говорю, что мне нравится, как Вы думаете.
Вы пришли к очень важной вещи - разделению теории и метатеории. Высказывание как формула - это объект нашей теории, но он там не имеет смысла, это просто символы $\mathrm{t}$, $p_1\equiv p_1$ и т.д.
В принципе, это просто игра с символами. Но мы же хотим изучать что-то осмысленное. Поэтому мы придаем символам теории смысл с помощью интерпретаций.
Интерпретация - это объект метатеории, т.е. другой теории, с помощью которой мы можем изучать нашу "маленькую" теорию. В этой метатеории у нас есть $\mathbf{True}$ и $\mathbf{False}$, понятия общезначимости и синонимичности и т.п. Именно понятие интерпретации дает значение и смысл нашим эквивалентностям.

[errnough]

Xaositect в сообщении #302758 писал(а):

Эта модель не для произвольных пропозициональных функций, а только для $\neg$ и $\equiv$. При желании ее можно расширить.

Да, я понял, что это модель, но из нее вырезали очень существенный механизм, наследования. На мой взгляд, если модель расширять, всё это сведется к Principia Mathematica.

Стоит только единственный раз упомянуть концепцию метаязыка, как мы получим следующую бесконечную последовательность:

Пусть $\psi$ начальное высказывание. Тогда уточняющее высказывание $\phi$ (истина-ложь) запишется как $\phi(\psi)$. Уточняющее на метаязыке высказывание $\theta$ о высказывании $\psi$ запишется как $\psi(\theta)$.

Если мы будем за один шаг итерации считать два уточнения в обе стороны, то для первых трех шагов получим:

$\begin{matrix} \phi(\psi(\theta))\\ \phi_1(\phi(\psi(\theta(\theta_1))))\\ \phi_2(\phi_1(\phi(\psi(\theta(\theta_1(\theta_2)))))) \end{matrix}$

Скорее всего, испугавшись столь удручающей картины с бесконечными уточнениями в обе стороны, и был общепринят аксиоматический метод, т.е. остановиться на определенных $\psi$-высказываниях. Однако боятся здесь нечего. У нас всего 33 буквы алфавита, а описать можно всё. Причина? Никто не ограничил количество связей от образующихся терминов. Аксиоматический метод это попытка термины теории сделать алфавитом, и отказаться от уточнений в сторону метаязыка. Тяжелейшая ошибка. Если мы одной связью назовем отношение одного термина к одному другому термину, то в сторону метаязыка количество связей растет иначе, чем в сторону уточняющих следствий и заключений теории.

Наглядный образ — растение озимой ржи, четырех месяцев вегетации. Если корни это связи терминов метаязыка, а стебель это следствия из терминов теории, то стебель растет вверх древообразной структурой, а корень вниз перекрестно-древовидной системой связей, по большей части с горизонтальными связями. При этом наша начальная $\psi$ это семя.

За четыре месяца у ржи образуется около 10 млн. больших и маленьких корешков, имеющих общую длину более 500 км. При этом количество корневых волосков достигает астрономической величины – 14 млрд с общей длиной свыше 10 тыс. км. Получается, ежедневно у растения ржи появляется до 4–5 км новых корней. При столь внушительных числах само растение (как образ теории) вполне обозримо и непротиворечиво.

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

Xaositect в сообщении #302758 писал(а):

"$\psi$ имеет ту же истинность, что и истинное высказывание"

Давайте я поставлю рядом два высказывания:
«"электрон суть частица" это истинное высказывание».
«"электрон суть частица" имеет ту же истинность, что и истинное высказывание"».

Разве второе не сводится к первому через закон транзитивности?

[Xaositect]

errnough в сообщении #303020 писал(а):

Разве второе не сводится к первому через закон транзитивности?

Я это и хочу сказать. "$\psi$ есть истинное высказывание" переводится на язык теории как $\psi\equiv\mathrm{t}$.

errnough в сообщении #303020 писал(а):

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

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

[errnough]

Еще одна сомнительная ситуация в Вашей модели логики, со знаками "равно" и "тождественно".

Xaositect в сообщении #303172 писал(а):

"$\psi$ есть истинное высказывание" переводится на язык теории как $\psi\equiv\mathrm{t}$.

Если «"электрон суть частица" это истинное высказывание» записывается как $\psi\equiv\mathrm{t}$, тогда $\psi=$"электрон суть частица" и $t=$"истинное высказывание".
Учитывая, что $\psi \equiv t$ — само по себе новое высказывание, обозначим его $\phi=(\psi \equiv t)$. Очевидно, что $\psi$ и $\phi$ различные высказывания.

Если возражений против использования знака равно "$=$" нет, тогда непонятно, что следует из этой аксиомы:

Xaositect в сообщении #302437 писал(а):

T.$(\varphi\equiv\mathrm{t})\equiv\varphi$

неужели $\psi \neq \phi$ и $\psi\equiv\phi$ ?

Напомню, как Вы сами используете "$=$" и "$\equiv$":

Xaositect в сообщении #302437 писал(а):

4. Если $I(\varphi) = I(\psi)$, то $I(\varphi\equiv\psi) = \mathbf{True}$, иначе $\mathbf{False}$.

----------------------

Xaositect в сообщении #303172 писал(а):

не слишком сложный, но и не тривиальный пример такой структуры

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

Уточню, что получается не база знаний предсуществующих знаний, вложенная в заранее продуманную структуру, а запись новых образований: связей терминов, и новых рассуждений. Структура вырастет сама, автоматически, так, как это получается у семени растения. Или у морозной снежинки на стекле.

[Xaositect]

errnough в сообщении #303491 писал(а):

Еще одна сомнительная ситуация в Вашей модели логики, со знаками "равно" и "тождественно".

Xaositect в сообщении #303172 писал(а):

"$\psi$ есть истинное высказывание" переводится на язык теории как $\psi\equiv\mathrm{t}$.

Если «"электрон суть частица" это истинное высказывание» записывается как $\psi\equiv\mathrm{t}$, тогда $\psi=$"электрон суть частица" и $t=$"истинное высказывание".
Учитывая, что $\psi \equiv t$ — само по себе новое высказывание, обозначим его $\phi=(\psi \equiv t)$. Очевидно, что $\psi$ и $\phi$ различные высказывания.

Если возражений против использования знака равно "$=$" нет, тогда непонятно, что следует из этой аксиомы:

Xaositect в сообщении #302437 писал(а):

T.$(\varphi\equiv\mathrm{t})\equiv\varphi$

неужели $\psi \neq \phi$ и $\psi\equiv\phi$ ?

Напомню, как Вы сами используете "$=$" и "$\equiv$":

Xaositect в сообщении #302437 писал(а):

4. Если $I(\varphi) = I(\psi)$, то $I(\varphi\equiv\psi) = \mathbf{True}$, иначе $\mathbf{False}$.

Да, $\phi$ и $\psi$ - это разные высказывания, но они синонимичны, и аксиома T именно это и утверждает.
Равенство - это абсолютная тождественность, а эквивалентность - это тождественность истинностных значений.

Цитата:

Xaositect в сообщении #303172 писал(а):

не слишком сложный, но и не тривиальный пример такой структуры

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

Уточню, что получается не база знаний предсуществующих знаний, вложенная в заранее продуманную структуру, а запись новых образований: связей терминов, и новых рассуждений. Структура вырастет сама, автоматически, так, как это получается у семени растения. Или у морозной снежинки на стекле.

Можно новую тему создать или даже в ПМ.

[errnough]

Еще раз о знаках "$=$" и "$\equiv$": по всей видимости, в Вашей модели они означают совсем не то, что в остальной математике.
Вернемся к примеру: «"электрон суть частица" это истинное высказывание».

Цитата:

Xaositect в сообщении #303172 писал(а):
"$\psi$ есть истинное высказывание" переводится на язык теории как $\psi\equiv\mathrm{t}$.

Эквивалентность, кроме транзитивности, обладает еще свойством симметричности. То есть, должно пройти проверку вот такое: $\mathrm{t}\equiv\psi$. Однако, «истинное высказывание это "электрон суть частица"» уже бессмыслица. У Рассела сотоварищи было введено несимметричное отношение "влечет". Вы его не используете, и Ваша модель, увы, не отражает действительных отношений в высказываниях, которые собирается описывать. Либо что-то не так с термином эквивалентность.

Еще раз, вот прежние высказывания:
«"электрон суть частица" это истинное высказывание».
«"электрон суть частица" имеет ту же истинность, что и истинное высказывание"».

Если второе сводится к первому через закон транзитивности, то перестает выполняться свойство симметричности.
Поэтому так странно выглядят скобки в Вашей аксиоме:
T. $(\varphi\equiv\mathrm{t})\equiv\varphi$
Скобки означают порядок действий. Но закрыв скобками правый знак эквивалентности, как раз и получим абсурд, поскольку вычислив в скобках на первом проходе синтаксического выражения, на втором проходе обязаны применить правило: читать слева направо.

Рассел был прав, введя под символом $\supset$ несимметричное отношение «$\varphi$ влечет $\psi$», $\varphi \supset \psi$.

Но и этого будет мало. Утверждать о чем либо, это устанавливать для данного высказывания, через новое высказывание, отношение к {истина,ложь}. Вы переобозначили "утверждение" через интерпретацию: «Интерпретацией $I$ назовем отображение, приписывающее каждому высказыванию $\varphi$ его истинностное значение $\varphi_I$, которое может быть равным $\mathbf{True}$ или $\mathbf{False}$.»

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

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

[Xaositect]

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

errnough в сообщении #303882 писал(а):

Но и этого будет мало. Утверждать о чем либо, это устанавливать для данного высказывания, через новое высказывание, отношение к {истина,ложь}. Вы переобозначили "утверждение" через интерпретацию: «Интерпретацией $I$ назовем отображение, приписывающее каждому высказыванию $\varphi$ его истинностное значение $\varphi_I$, которое может быть равным $\mathbf{True}$ или $\mathbf{False}$.»

Principia - это первый большой труд по мат.логике. Понятно, что некоторые вещи там изложены неудобно, недооценена важность некоторых деталей и т.д.
В частности, плохо прослеживается разделение между теорией и метатеорией. Высказывания вида $\vdash p \supset \vdash q$ используются в примерах без опасений, и т.п.

Цитата:

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

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

Цитата:

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

Ну, меня интересовал не результат, а алгоритм. Или хотя бы сам процесс поиска результата.

[errnough]

Xaositect в сообщении #303947 писал(а):

Цитата:

Выкидывание некоторых частей из логики Рассела, чтобы уйти от парадокса ...

Я их выкинул, не чтобы уйти от парадокса (которого нет).

Парадокса нет? Прислушайтесь к Вейлю: "Гёдель показал следующее: если игра, в которую играет математика, действительно непротиворечива, то формула непротиворечивости в этой игре вообще не может быть доказана." [Г.Вейль. Полвека математики. М., 1969. стр.44]

Цитата:

Ну, меня интересовал не результат, а алгоритм. Или хотя бы сам процесс поиска результата.

Если Вы вдруг не поверите в истинность результата, который выдал алгоритм, зачем тратить силы на изучение алгоритма? Я предложил "невероятный, абсурдный" результат. Абсурдный (дословно: неслыханный). Спросите себя, Вы собираетесь верить/не_верить результату, или доказывать его противоречивость, истинность, или что-то третье?

Фактически, я даю дилемму: если верим алгоритму, верим ли результату?

[Xaositect]

errnough в сообщении #303953 писал(а):

Парадокса нет? Прислушайтесь к Вейлю: "Гёдель показал следующее: если игра, в которую играет математика, действительно непротиворечива, то формула непротиворечивости в этой игре вообще не может быть доказана." [Г.Вейль. Полвека математики. М., 1969. стр.44]

Нет парадокса. Теорема Геделя - это не парадокс, а факт. Весьма интересный и глубокий.

errnough в сообщении #303953 писал(а):

Если Вы вдруг не поверите в истинность результата, который выдал алгоритм, зачем тратить силы на изучение алгоритма? Я предложил "невероятный, абсурдный" результат. Абсурдный (дословно: неслыханный). Спросите себя, Вы собираетесь верить/не_верить результату, или доказывать его противоречивость, истинность, или что-то третье?

Фактически, я даю дилемму: если верим алгоритму, верим ли результату?

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

[Xaositect]

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

0. Рекурсивно-перечислимые множества. Формальные системы.

Алфавитом называется конечный набор символов. Конечные цепочки символов алфавита - слова в этом алфавите. Множество всех слов в алфавите $A$ обозначается $A^*$. Пустое слово обозначается буквой $\Lambda$.

Языком в алфавите $A$ называется произвольное множество слов $L\subset A^*$.

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

Удобно задавать перечисляющий алгоритм в виде формальной грамматики. Формальная грамматика над алфавитом $A$ задается следующими тремя компонентами:
1. Алфавитом нетерминалов $N$, не пересекающимся с $A$.
2. Начальным нетерминалом $S\in N$.
3. Множеством продукций вида $r\to s$, где $r, s\in(A\cup N)^*$, причем $\alpha$ содержит хотя бы один нетерминал.

Слово $v\in (A\cup N)^*$ называется непосредственно выводимым из слова $u\in (A\cup N)^*$ (обозначение $u\Rightarrow v$), если существует продукция $r \to s$ такая, что $u=u_1 r u_2$, $v = u_1 s u_2$, т.е. $v$ получается из $u$ заменой подстроки, являющейся левой частью продукции, на соотв. правую часть. Слово $v$ называется выводимым из слова $u$ ($u\Rightarrow\!* v$), если существует цепочка непосредственных выводимостей $u\Rightarrow w_1 \Roghtarrow w_2 \Rightarrow \dots \Rightarrow v$

Грамматика задает язык $L = \{w\in A^*| S\Rightarrow\!* w\}$.

Примеры.
1. Алфавит $A=\{|\}$, нетерминалы $N = \{S\}$. Продукции: $S\to\Lambda, S\to ||S$.
Языком соответствующем этой грамматике, является язык $N_2 = \{|^{2n}|n\in\mathbb{N}\}$, так как выводимыми из $S$ строками являются только строки вида $|^{2n}S$ и $|^{2n}$.
2. Язык Дика. $A = \{(, )\}$, $N = \{S\}$. Продукции: $S\to\Lambda, S\to (S), S\to SS$.
Словами этого языка являются сбалансированные скобочные последовательности, например $()$, $(()())((()))$ и т.п.
3. $A = \{a,b,=\}$, $N=\{S, A, B\}$. Продукции: $S\to ASA, S\to BSB, S\to =, AB\to BA, BA\to AB, A\to a, B\to b$.
Словами этого языка являются слова вида $w_1=w_2$, где $w_1$ и $w_2$ не содержат знаков равенства и имеют одинаковое количество букв $a$ и $b$ в своем составе.
4. $A = \{|, =, +\}$, $N = \{S, N, R\}$. Продукции $S\to N=R, R\to N+N, ,N\to N|, N\to Lambda$. Язык - все строки вида $w=u+v$, где $u,v,w\in\{|\}^*$.

Теперь определим формальную систему, или теорию. Теория задается следующими четырьмя компонентами:
1. Алфавит $A$.
2. Множество формул - некоторый язык над алфавитом $A$.
3. Множество аксиом - подмножество множества формул.
4. Множество правил вывода, по которым можно получать из формул формулы.

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

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

Алгоритмы пунктов б и в удобно представлять в виде схем аксиом и схем правил вывода:

Схемой аксиом называется формула, в которой помимо символов языка могут встречаться метапеременные. Формула является аксиомой, если она получается из какой-то схемы аксиом подстановкой допустимых слов (часто допустимые слова - это произвольные формулы, но также это могут быть другие конструкты, например, термы или нумералы).
Схемой правил вывода называется фигура вида $\dfrac {F_1,\quad F_2,\dots, F_m}{G}$, где $F_i$, $G$ - это формулы, содержащие метапеременные. Формула $G'$ выводится из множества формул $F'_i$, если они являются результатами подстановки допустимых подслов вместо метапеременных в $G$ и $F_i$ соответственно.

Примеры
1. Схема правил вывода Modus ponens: $\dfrac{A,\quad A\to B}{B}$ содержит металингвистические переменные $A$ и $B$ - формулы. Пример частного случая этой схемы в логике предикатов: $\dfrac{P(x),\quad P(x)\to \forall y Q(y)}{\forall y Q(y)}$.
2. Схема аксиом $(A\to B)\to(\neg B\to \neg A)$.
3. Пример формальной системы:
Алфавит $A=\{|, =, +\}$, формулы - любые строки вида $C=A+B$, где $A,B,C$-слова из палочек (пример 4 формальной грамматики).
Аксиомы: $Z=Z+$, где $Z$-слово из палочек.
Правила вывода: $\dfrac{Z=X+Y}{Z|=X+Y|}$.
Выыводимыми в этой теории будут формулы вида $|^{m+n}=|^m+|^n$.
4. Еще один пример теории.
Алфавит $A=\{|,=\}$, формулы вида $A=B$, где $A,B$ - слова из палочек.
Аксиомы: $=$, $|=|$, $||=$
Правила вывода: $\dfrac{X=Y}{Y=X}$, $\dfrac{X=Y,\quad Z=T}{XZ=YT}$.
Какие формулы будут выводимы?

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

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

[Xaositect]

1. Классическая пропозициональная логика.

Рассмотрим чледующую формальную систему:
Алфавит $A = \{p, \to, \neg\}$.

Формулы.
Непустые слова, состоящие только из букв $p$, будем называть пропозициональными переменными и использовать обозначение $p_k$ вместо $\underbrace{p\dots p}_{k\ \text{раз}}$
Множество формул задается следующими правилами:
1. Если $P$ - пропозициональная переменная, то $P$ - формула.
2. Если $F$ - формула, то $(\neg F)$ - формула.
3. Если $F_1$, $F_2$ - формулы, то $(F_1\to F_2)$ - формула.
4. Никаких других формул нет.
Это определение легко может быть преобразовано в грамматику для языка формул.

При записи формул мы часто будем опускать внешние скобки, а также скобки вокруг $(\neg F)$. При желании всегда можно восстановить полноскобочную запись.

Примеры формул (сокращенная запись - полная запись)
1. $p_1\to (p_2\to p_1)$ - $(p\to (pp\to p))$
2. $\neg(p_1\to p_2)\to (p_2\to \neg p_3)$ - $((\neg(p\to pp))\to (pp\to (\neg ppp)))$

Аксиомы.
A1. $A\to (B\to A)$
A2. $(A\to (B\to C))\to ((A\to B)\to (A\to C))$
A3. $(\neg A\to\neg B)\to (B\to A)$

Правила вывода:
MP. $\dfrac{A,\quad A\to B}{B}$

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

Выводом формулы $B$ в формальной системе называется цепочка формул $A_1,A_2,\dots, A_l = B$, где каждое $A_k$ - либо аксиома, либо получается из набора формул $A_{i_1}, A_{i_2},\dots, A_{i_r}$($i_1,i_2,\dots,i_r < k$) по одному из правил вывода. Число $l$ называется длиной вывода.
Формула называется теоремой формальной системы, если существует ее вывод.

Пример вывода в пропозициональной логике
1. $p\to (p\to p)$ - частный случай схемы аксиом A1.
2. $p\to ((p\to p)\to p)$ - снова А1.
3. $(p\to ((p\to p)\to p))\to ((p\to (p\to p))\to (p\to p))$ - А2.
4. $(p\to (p\to p))\to (p\to p)$ - из (2) и (3) по MP.
5. $p\to p$ - из (1) и (4) по MP.

Таким образом, формула $p\to p$ является теоремой пропозициональной логики.

А теперь мы поговорим о разделении теории и метатеории, а потом докажем первую метатеорему.
Итак, у нас есть формальная теория, и мы может выводить в ней теоремы (И снова замечу, что пока все это игра со значками, которым не придан смысл). Эта теория - это хороший математический объект для изучения, то есть мы можем доказывать математические теоремы об этой теории. Такие теоремы называются метатеоремами. Позже мы увидим, что мы можем формализовать метатеорию и доказывать метатеоремы так же формально, как мы доказали сейчас $p\to p$.

Теорема (о подстановке). Если $A$ - теорема пропозициональной логики, то формула $A'$, получаенная из $A$ одновременной заменой всех вхождений $p_1$ на некоторую формулу $F_1$, $p_2$ - на $F_2$ и.т.д, также является теоремой.
Доказательство. Индукция по длине вывода.
Если длина вывода теоремы $A$ равна 1, то это частный случай схемы аксиом, т.е. получен подстановкой каких-то формул вместо $A,B,C$ в A1,A2 или A3. Тогда, заменив в этих формулах $p_k$ на $F_k$, мы получим также частный случай схемы аксиом.
Если длина вывода больше 1, то $A$ либо аксиома (рассмотрено выше), либо получается по MP из ранее полученных теорем, т.е. существует формула $B$ такая, что $B$ и $B\to A$ - теоремы. Они имеют более короткий вывод, а значит, $B'$ и $B'\to A'$, полученные заменой $p_k$ на соотв. $F_k$ - также теоремы, а $A'$ получается из них по MP.
Мы доказали теорему, причем параллельно доказали, что существует вывод формулы $A'$, имеющий такую же длину, что и вывод $A$.

Например, для любой формулы $A$ формула $A\to A$ будет теоремой, т.к. $p\to p$ - теорема.

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

[errnough]

2 Xaositect:

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

Вы написали пример:

«2. Схема аксиом $(A\to B)\to(\neg B\to \neg A)$.»

И множество формул определили так:

«Множество формул задается следующими правилами:
1. Если $P$ - пропозициональная переменная, то $P$ - формула.
2. Если $F$ - формула, то $(\neg F)$ - формула.
3. Если $F_1$, $F_2$ - формулы, то $(F_1\to F_2)$ - формула.
4. Никаких других формул нет.»

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

«Если $F$ — истинное высказывание, то $(\neg F)$ — ложное высказывание»,

тогда я отрицаю допустимость вот этого выражения: $\neg B\to$
В натуральном языке это звучит так: «Из ложного высказывания ничего не следует.» (Запрет операции "следует" для ложного высказывания.)

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

------

У меня готов пример из математики. Чаще всего конструкцию проще пояснить на примере. Могу показать, что операция вычитания векторов неопределена (противоречива, незаконна). Сегодня редко встретишь человека, который следует логике и доверяет ей проверку высказываний. Надеюсь, кажущаяся невероятность утверждения из примера не заставит Вас отказаться от исследования логики вывода.