Ряд вопросов по формальным аксиоматическим системам

[Amigo]

Вы не дали комментарий на теорему которую я привёл. Это очень подозрительно. Скажите почему Вы умолчали об этом?
В теореме ясно сказано о двух разных теориях:
1. Алгебра высказываний
2. Формализованное исчислении высказываний
Чем они отличаются?
Просмотрев всю главу касающуюся алгебры выскаазываний (а это сотни страниц и десятки теорем). Я обратил внимание на два момента:
1. Нигде во всей главе я не нашел слово "доказательство", вместо этого там присутствует понятие логического следования . Наоборот, с самого начала главы о Формализаванном исчислении высказываний, немедлено даётся понятие доказательства, как цепочки формул, каждая из которых есть либо аксиома, либо получена из аксиом по закону MP.
2.Нигде во всей главе о формализованном исчислении высказываний, я не нашел
понятия "истинность". Наоборот, с самого начала алгебры высказываний подчеркивается тот факт, что рассматриваемые в ней высказывания интересуют нас исключительно с точки зрения их истинности или ложности и дается таблица истинности основных логических операций.
Что скажите?

К слову,как кажется имеет место тот факт, что когда Вы получаете доказательство теоремы гедёля Вы должны сделать умозаключение о противоречивости на языке высказываний, то есть предпологая, что ТЧ не противоречива, и вней не могут быть
два противоположных высказывания одновременно истинными. Значит последний вывод в т. Геделя о неполноте сделан не внутри ФТЧ а из вне. В той системе, которая включает в себя высказзывания, отличающееся тем, что они могут быть истинными или ложными.

[маткиб]

Amigo писал(а):

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

Когда говорят про алгебру высказываний, думаю, имеют в виду следующее. Имеется язык алгебры высказываний: множество всех формул над переменными (из некоторого счетного алфавита) со связками \&, \vee, \neg. Вводится понятие интерпретации: интерпретация - это отображение множества всех переменных в множество {истина, ложь}. Иными словами, каждой переменной присваивается некоторое булево значение. Формула называется истинной в данной интерпретации, если её значение истинно при данной подстановке значений вместо переменных. Далее определяется общезначимость (тождественная истинность) формулы: формула общезначима, если она истинна в любой интерпретации. Вот и всё.

Аналогично можно поступить и с теорией чисел. Есть язык теории чисел, т.е. язык формальной арифметики: множество всех формул над переменными из счетного набора с булевыми связками, кванторами, константным символом "0", одноместным функтором s, двухместными функторами "+", "*", двухместным предикатным символом "=". При этом рассматривается одна конкретная интерпретация - стандартная модель арифметики: предметное множество \mathbb{Z_+}, все функторы и предикаты действуют так, как они обычно действуют в арифметике, т.е. s(x)=x+1, "+" - сложение, "*" - умножение, "=" - равенство. На основе этой модели вводится понятие истинности формулы.

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

Добавлено спустя 1 минуту 32 секунды:

Amigo писал(а):

К слову,как кажется имеет место тот факт, что когда Вы получаете доказательство теоремы гедёля Вы должны сделать умозаключение о противоречивости на языке высказываний, то есть предпологая, что ТЧ не противоречива, и вней не могут быть
два противоположных высказывания одновременно истинными. Значит последний вывод в т. Геделя о неполноте сделан не внутри ФТЧ а из вне. В той системе, которая включает в себя высказзывания, отличающееся тем, что они могут быть истинными или ложными.

Честно говоря, я не очень понял, что вы хотите сказать. Знаю только, что теорему Гёделя (в том виде, в котором не используется понятие истинности) можно сформулировать на языке формальной арифметики и доказать в формальной арифметике Пеано.

[Amigo]

Уважаемый маткиб, я тут посмотрел за Вашей активностью на форуме, и заметил, что Вы интересуетесь в основном вопросами логики, и уже не однократно принимали участие в подобных обсуждениях. Самое интересное конечно вот это:
http://dxdy.ru/viewtopic.php?t=1361&pos ... sc&start=0


Сразу хочу сказать, что определённый уровень коммуникаций, когда
собеседник больше заботится о том, как, так сказать, всё заформализовать и изложить техническим языком - мне не подходит.
Меня, повторяю, интересуют только идеи. И самая важная из них состоит в том, что бы доказать, что предикат $Doc(x,y):=(y=$Г(доказательство$g^{-1}(x))$,
где $g^{-1}(x)$ - функция, востанавливающая по номеру $x$ вид формулы в ФТЧ.
Г(f) - функция, сопоставляюшая каждой формуле f имеющейся в ФТЧ, Геделевский номер её доказательства , т.е. вывода в ФТЧ.
- действительно выразим в ФТЧ. А не то, что мы его просто придумали и настаиваем, что дескать он там должен быть, только потому, что нам хочется. Что как я понимаю, случилось с котофеичем , который решил засунуть в теорию объект из метатеории.
Это если выражаться формально, т.е. так как это делает Сосинский в своей лекции. (ссылку давал ранее).
Кстати, Сосинский, когда начинает свою лекцию, приводит интересное высказывание, которое
если не изменяет память, так же встречается и в рекомендованном Вами трехтомнике Шеня.
Сосинский рисует рамку, и в ней пишет высказывание - "Высказывание в рамке нельзя доказать". То есть приводит пример автореференции - ссылки на себя само. Это высказывание интересно тем, что оно противоречиво. Смаллиан, в своей книге "Как же называется эта книга" - исправляет этот парадокс следующим образом, он даёт новое высказывание которое звучит так: "Высказывание в рамке нельзя доказать в ФТЧ". То есть доказать не вообще ( тогда будет парадокс) а в конкретной теории.

Если рассмотреть это высказывание, то получим следующее:
Из допущения, что оно ложно, немедленно следует, что не верно, что его нельзя доказать.
Следовательно его доказать можно, ввиду того, что наша теория непротиворечива, то доказать в ней можно только истинные высказывания. Следовательно оно истинно. Противоречие. Таким образом доказанно, что высказывание в рамке - истинно. Но тогда истинно, что оно не обладает доказательством (т.е. не имеет формального вывода) в системе ФТЧ. Значит, если теория чисел непротиворечива, то ФТЧ - неполна.
Приведённое здесь рассуждение, есть концовка теоремы Гёделя, и остаётся один самый важный вопрос, а именно: как доказать что высказывание в рамке можно сформулировать
в терминах ФТЧ?

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

P.S.
Я скачал Ваш трёхтомник, начал изучать... Рекомендую и Вам почитать указанную ранее мною книгу. Писал её всё - таки не дурак, и думаю, что там найдётся много интересного и для формалиста, каким, как я понимаю, являетесь Вы.
P.P.S
Я точно установил, что все теоремы о полноте, непротиворечивости, разрешимости и даже
просто высказывание - "G выводится из $f_1,f_2,..f_n$ " -являются метатеоремами и метавысказыванием соответственно. Потому, при обсуждении т.Гёделя не удасться избежать
"прибывания" в метатеории. А для этого, нужно как минимум её описать. Подозреваю, что
метатеорией для ФТЧ является сама ТЧ. А Вы?

[маткиб]

Про предикат Doc(x,y) - "y - код доказательства формулы с кодом x".

Во-первых, заметим, что он разрешим, т.е. существует машина Тьюринга M, которая его вычисляет.
Т.е. Doc(x,y) можно перефразировать так: существуют конфигурации машины Тьюринга K_0,K_1,\ldots,K_n, такие, что K_0 - "на ленте записаны x,y, состояние q0", Kn - "состояние q1", для всех t K_{t+1} получается из K_t по правилам машины Тьюринга.

В виде формулы это будет так:
\exists K\exists n(\forall z(Vector(K,0,z)\rightarrow Begin(z,x,y)) \& \forall z(Vector(K,n,z)\rightarrow End(z)) \&
\&\forall t\forall u\forall v((t+1<n)\& Vector(K,t,u)\& Vector(K,t+1,v)\rightarrow Next(u,v))),
где
Vector(V,i,x) - "x есть i-й элемент вектора с кодом V",
Begin(z,x,y) - "z есть код конфигурации машины Тьюринга M, находящейся в состоянии q0, на ленте которой последовательно записаны записи чисел x и y",
End(z) - "z есть код конфигурации машины Тьюринга M, находящейся в состоянии q1",
Next(u,v) - "v есть код конфигурации машины Тьюринга M, в которую она придёт за один шаг, если сейчас её конфигурация имеет код u".

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

[Jnrty]

Jnrty:

маткиб, пожалуйста, окружайте формулы знаками $.

$\exists K\exists n(\forall z(Vector(K,0,z)\rightarrow Begin(z,x,y))\&\forall z(Vector(K,n,z)\rightarrow End(z))\&$
$\&\forall t\forall u\forall v((t+1<n)\& Vector(K,t,u)\& Vector(K,t+1,v)\rightarrow Next(u,v)))$

[маткиб]

Amigo писал(а):

Приведённое здесь рассуждение, есть концовка теоремы Гёделя, и остаётся один самый важный вопрос, а именно: как доказать что высказывание в рамке можно сформулировать
в терминах ФТЧ?

Как записывается это утверждение, я не помню, там какая-то достаточно простая, но хитрая конструкция, для которой нужен предикат Doc(x,y) и какие-то ещё вспомогательные предикаты.

Amigo писал(а):

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

Я не формалист. А на основании чего сложилось такое впечатление?
По поводу книжки: почитаю, если не лень будет
Кстати, если уж учить теорему Гёделя по научно-популярным книжкам, то есть ещё Пенроуз "Новый ум короля" - это вообще классика!

Amigo писал(а):

Подозреваю, что
метатеорией для ФТЧ является сама ТЧ. А Вы?

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

Amigo писал(а):

Из допущения, что оно ложно, немедленно следует, что не верно, что его нельзя доказать.
Следовательно его доказать можно, ввиду того, что наша теория непротиворечива, то доказать в ней можно только истинные высказывания. Следовательно оно истинно. Противоречие. Таким образом доказанно, что высказывание в рамке - истинно. Но тогда истинно, что оно не обладает доказательством (т.е. не имеет формального вывода) в системе ФТЧ. Значит, если теория чисел непротиворечива, то ФТЧ - неполна.

Обратил внимание на выделенное жирным. На самом деле это не так, и существует куча примеров.

Amigo писал(а):

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

Честно говоря, понятия не имею, что там произошло с Котофеичем. Я забросил затею разобраться в его тексте как абсолютно бесперспективную, да и вероятность того, что там было что-то стоящее, - около 0.00001%, не более, это сразу видно по косвенным признакам.

[маткиб]

Amigo писал(а):

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

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

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

А теперь докажем, что в теории $T$ (на теорию, естественно, нужно наложить ряд требований, например, корректность) нельзя доказать $\Sigma$-корректность $T$. Для теории построим класс $R_T$ - множество всех функций $f:\mathbb{N}\rightarrow\mathbb{N}$, для которых существует вычисляющий алгоритм и доказательство в теории $T$, что этот алгоритм останавливается на любом входе. $R_T$ обычно называют классом доказуемо рекурсивных функций для теории $T$.

Теперь опишем функцию $F(n,x)$ - универсальную функцию для $R_T$. Пусть в $n$ каким-то образом кодируются пары (алгоритм,доказательство). Тогда

$$ F(n,x)=\begin{cases} f_m(x),\text{ если доказательство, закодированное в $n$, верно доказывает, что} \\ \quad\quad \text{алгоритм с номером $m$ останавливается на любом входе,} \\ 0\text{ в противном случае,} \end{cases} $$

$f_m$ - функция, которую вычисляет алгоритм с номером $m$.

Заметим, что при любом фиксированном $n$ функция $h_n(x)=F(n,x)$ принадлежит $R_T$. Кроме того, любая функция из $R_T$ имеет номер. И, очевидно, что $F(n,x)$ вычислима (потому что мы её описали через алгоритм).

Теперь применим Канторовскую диагональ: $G(x)=F(x,x)+1$, очевидно, не совпадает ни с одной из функций в $R_T$, но, тем не менее, вычислима, и вычисляющий её алгоритм останавливается на любом входе. Если нужно доказать просто неполноту теории $T$, то на этом можно остановиться: мы привели алгоритм, останавливающийся на любом входе, но для которого доказать это в теории $T$ нельзя.

Но мы пойдём дальше и заметим, что если бы в теории $T$ можно было бы доказать её $\Sigma$-корректность, то можно было бы доказать и то, что вычисляющий $G$ алгоритм останавливается на любом входе (технический момент: нужно проделать это нехитрое доказательство в теории $T$), т.е. $G\in R_T$, противоречие.

Примечание 1. Класс $R_T$ часто используют для характеризации доказательной силы теории $T$: чем сильнее $T$, тем больше $R_T$. Но даже для самых слабых теорий (типа арифметики Пеано) $R_T$ содержит практически все встречающиеся в математической практике функции, и привести пример не лежащей в этом классе функции очень трудно. Кроме того, для любой теории $T$ класс $R_T$ можно описать в терминах вычислительной сложности.

Примечание 2. Если в определении $\Sigma$-корректности заменить "останавливается" на "не останавливается", то получится $\Pi$-корректность, которая эквивалентна непротиворечивости (т.е. получится более слабое свойство).

[Amigo]

маткиб писал(а):

Amigo писал(а):

Из допущения, что оно ложно, немедленно следует, что не верно, что его нельзя доказать.
Следовательно его доказать можно, ввиду того, что наша теория непротиворечива, то доказать в ней можно только истинные высказывания. Следовательно оно истинно. Противоречие. Таким образом доказанно, что высказывание в рамке - истинно. Но тогда истинно, что оно не обладает доказательством (т.е. не имеет формального вывода) в системе ФТЧ. Значит, если теория чисел непротиворечива, то ФТЧ - неполна.

Обратил внимание на выделенное жирным. На самом деле это не так, и существует куча примеров.

Вы меня пугаете, коллега…
Каких примеров? Вы о чём? Это стандартное определение непротиворечивости. Посмотрите у Успенского на стр.11. И там ещё дальше оно тоже присутствует.
И какие могут быть вообще примеры? Вы же понимаете, что в ФАС аксиомы (т.е. начальные формулы) выбирают не абы как, а таким образом, что бы они при интерпретации представляли из себя тавтологии т.е. тождественно истинные высказывания какой либо содержательной теории. А правила вывода таковы, что ежели, например, имеется формула F и F--> G, то G. Причем G – является так же тавтологией. Отсюда следует, что все теоремы ФАС таковы, что при интерпретации дают исключительно истинные утверждения. Иначе, в нашей ФАС просто нет ни какого смысла.
Дальше Вы говорите «Я обычно разделяю формальную теорию и неформальные измышления» - много пафоса, и наверное мало смысла. Вы отдаёте себе отчёт в том, что такое вообще формальная аксиоматическая теория? Уверяю, есть огромная разница, между просто аксиоматической теорией и её формальным аналогом. Первая разница состоит в том, что символы ФАС – начисто лишены какого либо содержательного смысла.
Второе и ключевое состоит в том, что об объектах ФАС нам запрещается пользоваться какими – либо предположениями , за исключением тех, которые явно сформулированы в аксиомах. В частности, в формальной теории нет ни какого понятия
полноты, непротиворечивости и выводимости. Эти основные характеристики теории, являются:
а) содержательными ( а нечего содержательного в ФАС нет, там есть просто цепочки символов, приобретающие некий смысл, только в связи с их интерпретацией в какой либо теории, которая уже содержательна, например строчка ФАС - SOO+SOO=SOOOO может быть проинтерпретирована в ТЧ как 2+2=4 и тогда оно истинно, а например в геометрии как сумма объемов кубов, стороны которых выражыются целыми числами, в такой интерпритации - данная строчка, очевидна ложна)
б) внешними по отношению к исследываемой ФАС. То есть такими, что позволяют нам
рассуждать о теории как бы из вне . Совокупность методов и теорем, описывающих какие – либо свойства ФАС – пренадлежат не самой ФАС, а совсем другой системе, которая является метатеорией по отношению к исследываемой теории. В эту (метатеорию), должна входить и алгебра высказываний, со своими понятиями истинности и ложности.
В самой же ФАС, ни какой истинности и ложности вообще нет. Это только совокупность, повторяю, нечего не значащих символов. Которые могут стать содержательными, истинными или ложными, только в связи с их интерпретацией.
Потому мне непонятно, как Вы, занимаясь не первый год логикой не видите разницы между свойствами, которые присуще теории имманентно, и внешними свойствами, которые имеют место только в связи с их интерпретацией. То есть разницы между теорией и метатеорией, в то время как они идут рука об руку с друг с другом.

[маткиб]

Amigo писал(а):

Вы меня пугаете, коллега…
Каких примеров? Вы о чём? Это стандартное определение непротиворечивости.

Стандартное определение непротиворечивости - это невозможность одновременно доказать какое-то утверждение и его отрицание.

[Amigo]

маткиб писал(а):

Amigo писал(а):

Вы меня пугаете, коллега…
Каких примеров? Вы о чём? Это стандартное определение непротиворечивости.

Стандартное определение непротиворечивости - это невозможность одновременно доказать какое-то утверждение и его отрицание.

Есть несколько подходов. Я Вам дал ссылку на Успенского, потому, что доказательство которое он там проводит основанно на излюбленной Вами теории алгоритмов.

[маткиб]

Amigo писал(а):

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

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

Добавлено спустя 13 минут 20 секунд:

Amigo писал(а):

Дальше Вы говорите «Я обычно разделяю формальную теорию и неформальные измышления» - много пафоса, и наверное мало смысла. Вы отдаёте себе отчёт в том, что такое вообще формальная аксиоматическая теория? Уверяю, есть огромная разница, между просто аксиоматической теорией и её формальным аналогом. Первая разница состоит в том, что символы ФАС – начисто лишены какого либо содержательного смысла.
Второе и ключевое состоит в том, что об объектах ФАС нам запрещается пользоваться какими – либо предположениями , за исключением тех, которые явно сформулированы в аксиомах. В частности, в формальной теории нет ни какого понятия
полноты, непротиворечивости и выводимости. Эти основные характеристики теории, являются:
а) содержательными ( а нечего содержательного в ФАС нет, там есть просто цепочки символов, приобретающие некий смысл, только в связи с их интерпретацией в какой либо теории, которая уже содержательна, например строчка ФАС - SOO+SOO=SOOOO может быть проинтерпретирована в ТЧ как 2+2=4 и тогда оно истинно, а например в геометрии как сумма объемов кубов, стороны которых выражыются целыми числами, в такой интерпритации - данная строчка, очевидна ложна)
б) внешними по отношению к исследываемой ФАС. То есть такими, что позволяют нам
рассуждать о теории как бы из вне . Совокупность методов и теорем, описывающих какие – либо свойства ФАС – пренадлежат не самой ФАС, а совсем другой системе, которая является метатеорией по отношению к исследываемой теории. В эту (метатеорию), должна входить и алгебра высказываний, со своими понятиями истинности и ложности.
В самой же ФАС, ни какой истинности и ложности вообще нет. Это только совокупность, повторяю, нечего не значащих символов. Которые могут стать содержательными, истинными или ложными, только в связи с их интерпретацией. Потому мне непонятно, как Вы, занимаясь не первый год логикой не видите разницы между свойствами, которые присуще теории имманентно, и внешними свойствами, которые имеют место только в связи с их интерпретацией. То есть разницы между теорией и метатеорией, в то время как они идут рука об руку с друг с другом.

Всё существенно хуже: я не знаю, что такое метатеория

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

Добавлено спустя 17 минут 45 секунд:

Amigo писал(а):

маткиб писал(а):

Amigo писал(а):

Вы меня пугаете, коллега…
Каких примеров? Вы о чём? Это стандартное определение непротиворечивости.

Стандартное определение непротиворечивости - это невозможность одновременно доказать какое-то утверждение и его отрицание.

Есть несколько подходов. Я Вам дал ссылку на Успенского, потому, что доказательство которое он там проводит основанно на излюбленной Вами теории алгоритмов.

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

[Amigo]

маткиб писал(а):

Всё существенно хуже: я не знаю, что такое метатеория

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

Я Вас умаляю - почитаёте наконец приведённую мною книгу. Говорю Вам - это шедевр.
Она печаталась во многих странах, и имеет большое количество наград. Вобщем - вещь серьёзная.
В этой книге приводится в частности следующий пример:
Строится некая формальная система (MUI)
Алфавит состоит из 3-х букв - A={M,U,I}
имеется одна аксиома – MI.
И четрыре правила вывода:
1. Если имеется строчки, кончающаяся на I, то в конце её можно дописать U.
2.Если имеется строчка Mx-, где x –любая последовательность, то Mxx –также строчка системы.
3. Если где то в строчке встречаются три подряд идущие буквы I, то их можно заменить на U.
4. Если где то в строчке встречаются две подряд идущие буквы U, то их можно из строчки исключить.
Далее предлагается читателю доказать, что строчка MU – является теоремой нашей системы.

Итак, когда система (MUI) построена, автор проделывает следующее: он показывает, что
эту систему можно изучать из вне, то есть, получить все теоремы этой системы, в некой другой системе, затем при помощи изоморфизма, мы можем вернуться обратно в систему, и записать их в терминах системы (MUI). Та теория, в которую он вкладывает систему (MUI) – называется теорией чисел. Он показывает, что любой вопрос системы (MUI)
может быть решён в теории чисел. (вкладывание системы (MUI) – в теории чисел осуществляется при помощи Гёделева изоморфизма, правила системы (MUI) – заменяются соответствующими арифметическими правилами).

Дальше я сам не очень понял, то есть я не понял – является ли теория чисел МЕТАтеорией
для системы (MUI). Было бы хорошо, если бы Вы как раз эту книгу посмотрели, и высказали своё мнение. А то я никак не могу догнать этот момент.

[маткиб]

Amigo писал(а):

Я Вас умаляю - почитаёте наконец приведённую мною книгу. Говорю Вам - это шедевр.

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

Добавлено спустя 3 минуты 14 секунд:

Amigo писал(а):

Дальше я сам не очень понял, то есть я не понял – является ли теория чисел МЕТАтеорией
для системы (MUI). Было бы хорошо, если бы Вы как раз эту книгу посмотрели, и высказали своё мнение. А то я никак не могу догнать этот момент.

Сейчас моё мнение такое, что не стОит на эту тему заморачиваться, на суть дела это не влияет.