Здравствуйте, ботаныч, Вы писали:

Б> да я ждал подобный вопрос, и заранее предполагал ответ. в шаблонизации из С++ параметры шаблона указывать не обязательно, они подразумеваются.
Так всё-таки n или n+1?
Б> да именно рекурсивно завязанный на себя утверждающий, сам. т.е. просто применяет к себе то правило которое он вводит, в языковую область
Всё-таки язык.

S>>У вас P — это некое утверждение, записанное на языке L1.
Б> я бы не стал пока говорить языке, скорее о правилах, его описывающих. и вот все таки мы мыслим формальными языками в данном случае,
И вот вы уже не хотите говорить о языке.

Б> опяьт таки, не согласен с языком, для подразумеваемого языка что P(n0-nK) что P(n0-P-nK) им покрывается
Таких языков не бывает

S>>Есть пропасть между утверждением "(x < 0) and (x > 0)", и утверждением "не существует таких x, что (x < 0) and (x > 0)".
S>>Они записаны на разных языках.
Б> странно, правило P вводится в язык.. рамки (scope ввода определен) P(x0-xN) : P(x0..xn, PO) — есть требование рекурсивной устойчивости. очевидно же, что оно и описано именно так.
Не получается его так описать. Я же привёл примеры — как вы опишете утверждение про разрешимость предиката, оставаясь в рамках логики предикатов первого порядка?

Б> все давайте докажем L1 and L2 как по мне ввод и есть L
Что такое "докажем"? Всё, что можно сделать с L1 — вычислить для заданных параметров.

Возьмём другой пример. Вот у нас три утверждения:

1. C = A & B
2. A = true
3. B = true

Можем ли мы вычислить С? Кажется, что да. Ведь если мы подставим значения A и B из утверждений 2 и 3 в утверждение 1, то получится true.
Но на самом деле нет — мы воспользовались некоторым "мета-утверждением", которое не было задано в нашем списке. Как нам быть? Может быть, добавить его в модель?

1. C = A & B
2. A = true
3. B = true
4. Если X описано формулой с использованием других переменных, и в модели есть формулы, явно задающие значения этих переменных, то можно вычислить X, подставляя эти значения в эту формулу.

Всё, можно вычислять C?
Нет, нельзя. Теперь мы неявно пользуемся ещё одним правилом:

1. C = A & B
2. A = true
3. B = true
4. Если X описано формулой с использованием других переменных, и в модели есть формулы, явно задающие значения этих переменных, то можно вычислить X, подставляя эти значения в эту формулу.
5. Если модель состоит из формул и правил вывода, то можно вычислять значения формул, применяя к ним заданные в модели правила вывода.

Уже начинает просматриваться бесконечность. Получается, мы вообще ничего не можем — даже элементарную булеву формулу вычислить.
Почему? Потому, что мы пытаемся обойтись одним уровнем языка. Фактически, утвеждение 4 — это свойство L1, языка, на котором описаны свойства 1-3. А утверждение 4 — это свойство L2, языка, на котором описываются формальные модели. И само оно написано на языке L3.