Здравствуйте, Sinclair, Вы писали:

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

Б>> да я ждал подобный вопрос, и заранее предполагал ответ. в шаблонизации из С++ параметры шаблона указывать не обязательно, они подразумеваются.
S>Так всё-таки n или n+1?
так а что вас смущает, добавляется правило (оккей — язык), есть язык до этого правила, есть после. говорится лишь о рекурсивной составляющей, чтобы правило соответствовало себе-же. в грамматиках такой рекурсивный
rule : rule next_block | next_block

Б>> да именно рекурсивно завязанный на себя утверждающий, сам. т.е. просто применяет к себе то правило которое он вводит, в языковую область
S>Всё-таки язык.
да в тот язык, в котором идет образование формальных моделей. но он таки — natural,

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

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

root_rule: root_rule next_block | next_block

- до P и после

root_rule: root_rule next_block | next_block
next_block: next_block P | P
P : ...

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

template <typename... T>
struct grey_code_frase
{
   using this_frase_type = decltype(grey_code_frase());
   usng code_frases = std::tuple<this_frase_type, T...>; 
};

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

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

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

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

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

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

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

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