Теорема Геделя и вера

[vc]

Вот я хочу узнать, как Вы собираетесь кодировать Геделизацию. Пожалуйста, с номерами аксиом и правил вывода. Серьезно (опишите идею)

Halting problem is closely related to the 1st GT both in proof and its result. In fact, a slightly weaker incompleteness theorem can be proved based on the unsolvability of the halting problem (no true recursively axiomatizable theory in arithmetic can be complete). So roughly speaking, the Turing theorem can be regarded as the incompleteness theorem for computer people, and the strings that cause the TM not to halt as undecidable statements (Godel sentence being one of them).

As to the non-halting TM encoding, it can easily be found in any book on computability that proves the Turing theorem.

[Dmitry67]

1
Это на каком языке Фома утверждает? Теории или модели? Вы путаете эти языки опять.
"формула выводима" - утверждение на языке модели. Оно может быть истинным или ложным.
"Pf(от ее геделевского номера)" - строка теории, которая не может быть ложной. Она может быть выводимой или нет.

2
Если под "Pf(от ее геделевского номера) ложно" Фома понимает "интерппретация "Pf(от ее геделевского номера)" в модели ложна", то это то же самое что "НЕ формула выводима", и Фома неправ по закону исключенного третьего.

1
Вот вот. Согласитесь, что само понятие геделизации - это утверждение на языке модели. ЧТо дескать значок => мы будем заменять тем то, а отрывающую скобку темто

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

Я прекрасно понимаю, что есть арифмитическое выражение ТГ в арифметике. Его можно доказать формально. Но увы, никакого смысла это утвержение не несет, если мы не выходим в мета-область.

2
Ваше второе замечание натолкнуло на другую интересную мысль
Вот есть классическая логика, а есть интуитивисткая. Про интуитивистские теории тоже можно кое что подаазывть. Вопрос: почему когда мы рассуждаем о теориях (то есть на уровне natural language) мы используем стандартную логику, а не интуитивисткую? Кто сказал что она правильнее ?

[Dmitry67]

Вот я хочу узнать, как Вы собираетесь кодировать Геделизацию. Пожалуйста, с номерами аксиом и правил вывода. Серьезно (опишите идею)

Halting problem is closely related to the 1st GT both in proof and its result. In fact, a slightly weaker incompleteness theorem can be proved based on the unsolvability of the halting problem (no true recursively axiomatizable theory in arithmetic can be complete). So roughly speaking, the Turing theorem can be regarded as the incompleteness theorem for computer people, and the strings that cause the TM not to halt as undecidable statements (Godel sentence being one of them).

As to the non-halting TM encoding, it can easily be found in any book on computability that proves the Turing theorem.

Я не очень хорошо написал. Геделизация сама есть кодирование
Я имел в виду как записать 'мы будем заменять символ => тем то' в номерах аксиом аксиоматики Пеано и исчисления предикатов

[vc]

Я не очень хорошо написал. Геделизация сама есть кодирование
Я имел в виду как записать 'мы будем заменять символ => тем то' в номерах аксиом аксиоматики Пеано и исчисления предикатов

As I wrote before, there is no difference between the idea that the letter A can be encoded with the natural number 33 and the idea that the formula (E x) (x > 0) can be encoded with some other natural number. The encoding in both cases would be a collection of pairs like A -> 33, 'some formula' -> 'some natural number'. Clearly, the idea itself cannot be expressed in the first order language (FOL+ PA), one needs some subset of a natural language to do that, but the idea representation in the formalized language would be a collection of above pairs.

One can use the jargon of 'metalanguage'/'object language' by juxtaposing the idea as expressed in a natural language and the formalized language translation, but it's unclear what advantage of talking so might be except trying to sound important. After all, even simplest mathematical ideas are expressed in a natural ['meta']language and then translated into some formalized expressions. When everything is 'meta', why not just save on the prefix and say that the idea is described in a math dialect of some natural language ?

So back to the original question. What's the difference between encoding a letter and doing the same with a formula ? If there is no difference, then how can you claim that there is more 'meta' about the1st GT than any other math theorem ?

[Bobo]

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

Что такое "понятие"? Интерпретация в модели? Тогда - да. Интерпретация ТГ в модели - это утверждение о теории на языке модели. Если хотите - мета-утверждение.

ЧТо дескать значок => мы будем заменять тем то, а отрывающую скобку темто

Вы описываете синтаксическую процедуру на языке теории. Модель появляется когда мы говорим, что значок => обозначает импликацию.

Задумайтесь, а зачем геделизация понадобилась Геделю вообще

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

Ведь если ТГ - исключительно арифметическа теорема, то ее можно доказать, не прибегая к геделизации вообще.

Это еще почему?

Я прекрасно понимаю, что есть арифмитическое выражение ТГ в арифметике. Его можно доказать формально. Но увы, никакого смысла это утвержение не несет, если мы не выходим в мета-область.

Да. Так же как не несет смысла ни одна другая теорема. ТГ ничем не хуже и не лучше.

[DMAlex]

Вот я хочу узнать, как Вы собираетесь кодировать Геделизацию. Пожалуйста, с номерами аксиом и правил вывода. Серьезно (опишите идею)

As to the non-halting TM encoding, it can easily be found in any book on computability that proves the Turing theorem.

Я не очень хорошо написал. Геделизация сама есть кодирование
Я имел в виду как записать 'мы будем заменять символ => тем то' в номерах аксиом аксиоматики Пеано и исчисления предикатов

Забавный тут ведется спор. Ээээээ..... как бы это поточнее выразить.... "спор средневековых схоластиков" выраженный с применением матиматического аппарата формальной логики Все это конечно интересно, вот только почему то математики (я вот тоже.... эээ... прикладной, спец. 402) часто забывают как эта странная наука связана с реальной жизнью.... а может не связана? чур меня! Так вот друзья ПОЖАЛУЙСТА задумайтесь ненадолго хотя бы о том что "вначале было слово". Дайте ему определение.... эээ... неважно в какой аксиоматике, посмотрите как ваше "слово" соотносится с действительностью ну и так далее, не мне вас учить ... вы тут такими умными словами бросаетесь, я их и забыл уж давно за ненадобностью..... так вот когда вы немного поразмыслите о "жизненности" ("физичности") всех ваших теорий (не только ТГ кстати) то я думаю ваш многоученый спор закончится довольно быстро и неожиданно.

PS:
прошу меня сильно извинить, ногами не бить. Школу флейма я прошел еще в 94 году в Фидо и тут просто не удержался, уж больно смешно читать вас было

[Dmitry67]

Во первых, после поста DMAlex я хотел сказать, что сам удивлен, что тут собрались люди, которые могут говорить о такой узкой и специальной области. Это просто замечательно ! Но перейдем к делу

1
One can use the jargon of 'metalanguage'/'object language' by juxtaposing the idea as expressed in a natural language and the formalized language translation, but it's unclear what advantage of talking so might be except trying to sound important.
After all, even simplest mathematical ideas are expressed in a natural ['meta']language and then translated into some formalized expressions. When everything is 'meta', why not just save on the prefix and say that the idea is described in a math dialect of some natural language ?

2
So back to the original question. What's the difference between encoding a letter and doing the same with a formula ? If there is no difference, then how can you claim that there is more 'meta' about the1st GT than any other math theorem ?

1 Разница важнейшая и принципиальнейшая
Геделизация отображдает любое доказательство в число. Это делается некоей функцией от номеров аксиом и номеров правил вывода в доказательстве. Если blab blah blah является неотъемлеммой и неэлиминируемой частью доказательства, то такое метадоказательство не является геделизируемым. Ему не соответствует число. Про него нельзя доказывать теоремы, подавать на вход машине Тьюринга итд

В частности, предикат Pf(X) геделя рассматривает только доказательства, не мета-доказательства

2 См выше. И то и то не сводимо к номерам аксиом и правил вывода. Это метарассуждения. Геделизация позволяет отобразить формулы и выводы в числа, но сама геделизация не геделизируема

[Bobo]

Schoolmaster: 'Suppose x is the number of sheep in the problem.'
Pupil: 'But, Sir, suppose x is not the number of sheep.'
(I asked Prof. Wittgenstein was this not a profound philosophical joke, and he said it was).

Проф. Витгенштейн, как и мы, считал, что понимает ТГ, в то время, как многие по сей день считают, что он не понимал.

[vc]

...

1 Разница важнейшая и принципиальнейшая
Геделизация отображдает любое доказательство в число. Это делается некоей функцией от номеров аксиом и номеров правил вывода в доказательстве.

OK.

Если blab blah blah является неотъемлеммой и неэлиминируемой частью доказательства, то такое метадоказательство не является геделизируемым. Ему не соответствует число.

Sorry, that does not make any obvious sense. Could you please rephrase ?

В частности, предикат Pf(X) геделя рассматривает только доказательства, не мета-доказательства

2 См выше. И то и то не сводимо к номерам аксиом и правил вывода. Это метарассуждения.

So you agree that there is no difference between those two notions in the sense that both require a natural language to express some ideas (that's essentially what you've said above) ? You agree, don't you, that for example the fundamental theorem of arithmetic ("Every natural number is either prime or can be represented as a product of primes in a unique way") is no different from the 1st GT in the sense of being just an ordinary theorem about natural numbers and proof strings?

[Dmitry67]

Если blab blah blah является неотъемлеммой и неэлиминируемой частью доказательства, то такое метадоказательство не является геделизируемым. Ему не соответствует число.

1
Sorry, that does not make any obvious sense. Could you please rephrase ?

2
So you agree that there is no difference between those two notions in the sense that both require a natural language to express some ideas (that's essentially what you've said above) ? You agree, don't you, that for example the fundamental theorem of arithmetic ("Every natural number is either prime or can be represented as a product of primes in a unique way") is no different from the 1st GT in the sense of being just an ordinary theorem about natural numbers and proof strings?

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

2 Нет
"Every natural number is either prime or can be represented as a product of primes in a unique way" может быть переписан исключительно с помощью кварторов, связок =>/NOT, скобок, и пары еще символов
Никаких слов ни для выражения этого, ни для доказательства не нужно
Доказательство записывается формально

ТГ формально не записывается, потому что она говорит о то что "существует невыводимое..." итд

[tau797]

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

Да, меня тоже.

Ребята, я не принимаю участия в споре, но я - в теме и, таким образом, с Вами!

[vc]

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

But the whole point is that one can can as long as there is an agreement on some basic mathematical notions expressed in a natural language, e.g. a function is represented as a collection of pairs, a proof is represented as a sequence of formulas.

2 Нет
"Every natural number is either prime or can be represented as a product of primes in a unique way" может быть переписан исключительно с помощью кварторов, связок =>/NOT, скобок, и пары еще символов
Никаких слов ни для выражения этого, ни для доказательства не нужно
Доказательство записывается формально

The same is true for the 1st GT.

ТГ формально не записывается, потому что она говорит о то что "существует невыводимое..." итд

What the theorem actually says is that if the theory (PA) is consistent, then there is no sequence of formulas (G1, .., Gn) representing a proof of either G or ^G where G is a Godel sentence. The final stage of the 1st GT proof is a simple proof by contradiction:

assume PA |- G, which means PA |- Pr(#G) where #G is the number representing G. But, by the diagonal lemma: PA |- ~Pr(#G) which leads to a contradiction assuming PA is consistent. Showing that neither is there a sequence of formulas representing a ^G proof is similar.

The usual proof of the FTA also relies on a proof by contradiction. The 1st GT proves some facts about strings of characters that happen to be proof encodings, and the FTA proves some facts about natural numbers, that's all. So what's fundamentally different between the two proofs ?

[Dmitry67]

1
But the whole point is that one can can as long as there is an agreement on some basic mathematical notions expressed in a natural language, e.g. a function is represented as a collection of pairs, a proof is represented as a sequence of formulas.

2
The same is true for the 1st GT.

3
What the theorem actually says is that if the theory (PA) is consistent, then there is no sequence of formulas (G1, .., Gn) representing a proof of either G or ^G where G is a Godel sentence. The final stage of the 1st GT proof is a simple proof by contradiction:

assume PA |- G, which means PA |- Pr(#G) where #G is the number representing G. But, by the diagonal lemma: PA |- ~Pr(#G) which leads to a contradiction assuming PA is consistent. Showing that neither is there a sequence of formulas representing a ^G proof is similar.

The usual proof of the FTA also relies on a proof by contradiction. The 1st GT proves some facts about strings of characters that happen to be proof encodings, and the FTA proves some facts about natural numbers, that's all. So what's fundamentally different between the two proofs ?

1 Доказательство в формальной теории есть дерево с правилами вывода в узлах и аксиомами в качестве листьев. ВСЕ. PERIOD. (c точностью до эквивалентных формулировок

Мета доказательство, есть рассуждение, приводящее оппонетна к убеждению, что это так

Формальное доказательство может быть применено к аксиоматическим системам, в которых нет понятия function, sequence, set etc.

Более того, формальное доказательство может быть применено к системам, в которых нет правила contradiction вообще, например, к интуиционисткой логике. Скажите, можете ли Вы в доказательстве (в рассуждениях на естественном языке) применять contradiction, если теория - субъект доказательства этот принцип отрицает? Непонятно. Именно поэтому финитные, абсолютно строгие методы без единого слова и были востребованы, особенно после того, что произошло с 'наивной теорией множеств'

2. Нет.
Так как я утверждаю несуществование (невыразимость GT через номера аксиом), а Вы существование, то Вам очевидно легче опровергнуть меня всего одним примером. Слабо ?

3.
>So what's fundamentally different between the two proofs ?
Words 'consistent', 'sequence of formulas', 'representing a proof', которые отсутствуют в аксиоматике Пеано, и, следовательно, не являются его частью

[vc]

1 Доказательство в формальной теории есть дерево с правилами вывода в узлах и аксиомами в качестве листьев. ВСЕ. PERIOD. (c точностью до эквивалентных формулировок

We've already been through this tree business -- the proof tree is the same as the sequence of formulas in the 1st GT proof. Not sure why it's not, like, obvious.

Мета доказательство, есть рассуждение, приводящее оппонетна к убеждению, что это так

The phrase does not make any obvious sense.

Формальное доказательство может быть применено к аксиоматическим системам, в которых нет понятия function, sequence, set etc.

Could you provide an example of such system ?

Более того, формальное доказательство может быть применено к системам, в которых нет правила contradiction вообще, например, к интуиционисткой логике.

You are confused: the intitionist logic is quite happy with a proof by contradiction, and the 1st GT proof is quite constructive. What the IL does not accept is the 'excluded middle principle', not the proof by contradiction.

Скажите, можете ли Вы в доказательстве (в рассуждениях на естественном языке) применять contradiction, если теория - субъект доказательства этот принцип отрицает? Непонятно.

See above.

]
Именно поэтому финитные, абсолютно строгие методы без единого слова и были востребованы, особенно после того, что произошло с 'наивной теорией множеств'

It's unclear what you mean here.

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

??? The large chunk of the proof is exactly about how one can map formulas and proofs to the natural numbers. Are you denying the obvious ? What exactly is not translatable into the PA language ?

>So what's fundamentally different between the two proofs ?
Words 'consistent', 'sequence of formulas', 'representing a proof', которые отсутствуют в аксиоматике Пеано, и, следовательно, не являются его частью

The word 'consistent' has a clear math defintion and is part of the first order logic vocabulary and thus of the PA ; 'representing anything as' is a natural language statement and you cannot say anything at all in the entire math without having some intuitive idea of what those words mean. Thus, the 1st GT is not special in this respect.

As to the sequence, if you read any GT exposition, you'll discover that sequences are encoded via Godel's beta function, with just a pair of natural numbersand therefore are expressed in the PA language as is the rest of the proof components.

[tau797]

Осмелюсь предложить уважаемому собранию великолепную книгу Дугласа Хофштадтера "Гёдель, Эшер, Бах - эта бесконечная гирлянда". Не исключено, что кто-то из посетивших сии страницы еще не знаком с этим блестящим, широчайшим по эрудиции и глубоким трудом.
http://www.lib.ru/INDEXLESS/wwg/russian/index.htm

Кстати, вот еще довольно любопытная статья на смежные темы:
Макроскопические флуктуации в модели алгоритмического мира

[Dmitry67]

1

Формальное доказательство может быть применено к аксиоматическим системам, в которых нет понятия function, sequence, set etc.

Could you provide an example of such system ?

2

Более того, формальное доказательство может быть применено к системам, в которых нет правила contradiction вообще, например, к интуиционисткой логике.

You are confused: the intitionist logic is quite happy with a proof by contradiction, and the 1st GT proof is quite constructive. What the IL does not accept is the 'excluded middle principle', not the proof by contradiction.

3

Скажите, можете ли Вы в доказательстве (в рассуждениях на естественном языке) применять contradiction, если теория - субъект доказательства этот принцип отрицает? Непонятно.

See above.

4

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

??? The large chunk of the proof is exactly about how one can map formulas and proofs to the natural numbers. Are you denying the obvious ? What exactly is not translatable into the PA language ?

5
'representing anything as' is a natural language statement and you cannot say anything at all in the entire math without having some intuitive idea of what those words mean.

1 Пожалуйста. Аксиоматика Пеано. В нет нет понятия 'множества'. Поэтому, когда Вы говорите 'последовательность формул', например, то Вы уже выходите за рамки аксиоматики Пеано, а находитесь в области AP+наивная теория множеств

2 Может быть. Во всяком случе (A or not A) в интуиционисткой логике не доказуемо для любого A

3
Я переформулирую вопрос
Например, можете ли Вы произвонсить фразу 'возьмем любое не важно что', рассуждая о теории множеств БЕЗ аксиомы выбора AC ?

4
Вот Вы и подтвердили мои слова
Поймите, я не отрицаю того, что предикат Con(#X) работает также как |- X
потому что Гедель так замечательно придумал. Построил. То есть по построению
Но Вы никак не хотите признать что Con(#X) и |- X все таки разные вещи. Одно отображено в другое Геделизацией, но сама Геделизация есть handwaving, да, она формальна, но описывается на метаязыке.

Признав что "The large chunk of the proof is exactly about how one can map formulas and proofs to the natural numbers" Вы фактически признали, что handvawing есть неотъемлимая часть доказательства

5
Формальное доказательство содержит только номера аксиом и правил вывода
Для его верификации не требуется абсолютно никаких "some intuitive ideas"

[olg2002]

The essence of Gödel's incompleteness theorem is that you cannot have both completeness and consistency. A bold anthropomorphic conclusion is that there are three types of people; those that must have answers to everything; those that panic in the face of inconsistencies; and those that plod along taking the gaps of incompleteness as well as the clashes of inconsistencies in stride if they notice them at all, or else they succumb to the tragedy of the human condition.

The first kind are prone to refer to authorities; religion, bureaucracy, governments and their own prejudices. They postulate a Supreme Being that knows all the answers because everything must have an answer. With inconsistencies they deal by hopping over them, brushing them aside, sweeping them under a rug, ignoring them or making fun of them. These people are unpredictable and exasperating to deal with, though often disarmingly charming.

The second kind are the more heroic and independent thinkers. They are not afraid of vast expanses of the unknown; they forge ahead and rejoice over every new question opened up by questions answered. But when up against the walls of inconsistencies they go berserk. These claustrophobics are in fact the scientific minds.

And then, finally, there are the ordinary humans who make do with both inconsistencies and gaps in their experience of life and the world. Some of those, when driven to the brink of endurance by roadblocks of paradox and pitfalls of the unknown, go mad.

[vc]

1 Пожалуйста. Аксиоматика Пеано. В нет нет понятия 'множества'.
Поэтому, когда Вы говорите 'последовательность формул', например, то Вы уже выходите за рамки аксиоматики Пеано, а находитесь в области AP+наивная теория множеств

The Peano theory does not have the notion of finite sequence. That's precisely why Godel used his Beta function to translate any finite sequence of natural numbers into a natural number. In his proof however he did not use any axioms of a set theory, naive or otherwise, because he encoded everything he needed for the proof with natural numbers and worked within the Peano theory, that was the whole point. It's unclear why you think that representing a finite sequence with a natural number is somehow inadequate.

2 Может быть. Во всяком случе (A or not A) в интуиционисткой логике не доказуемо для любого A

How's that relevant to the proof by contradiction ?

3
Я переформулирую вопрос
Например, можете ли Вы произвонсить фразу 'возьмем любое не важно что', рассуждая о теории множеств БЕЗ аксиомы выбора AC ?

How 's the AC relevant to the 1st GT proof ?

4
Вот Вы и подтвердили мои слова
Поймите, я не отрицаю того, что предикат Con(#X) работает также как |- X
потому что Гедель так замечательно придумал. Построил. То есть по построению
Но Вы никак не хотите признать что Con(#X) и |- X все таки разные вещи. Одно отображено в другое Геделизацией, но сама Геделизация есть handwaving, да, она формальна, но описывается на метаязыке.

Of course, Con(PA) and |-X mean different things. You probably wanted to say that you are not convinced that the Godel provability predicate formalizes the informal notion of proof, or that a finite sequence cannot be meaningfully represented by a natural number, etc. It's a strange point of view, but apparently there is nothing anyone can do to change your mind. So, if you are serious about your opinions, the GTs simply should not exist for you because you do not accept their proofs. Further, you should also reject such notions as the natural numbers, the set and the idea of set membership because none of the above is formalizable. The idea of a function represented as a set of pairs should also be meaningless to you at least for two reasons: first, you might not be satisfied with the informal notion of function represented as a set of pairs, second, the very word 'set' might be meaningless to you as well.

Признав что "The large chunk of the proof is exactly about how one can map formulas and proofs to the natural numbers" Вы фактически признали, что handvawing есть неотъемлимая часть доказательства

No, I did not. 'Handwaving' usually means that some [not so] important steps in a proof are missing and replaced with more or less informal persuasion. What's missing in the proof ? If by 'handwaving' you mean that the sequence/provability representation does not convince you, see above.

5
Формальное доказательство содержит только номера аксиом и правил вывода
Для его верификации не требуется абсолютно никаких "some intuitive ideas"

The proof was intended for human consumption and in addition to a fully rigorous exposition contains informal explanations. What you are looking for has been done by Shankar in 1986 (the GT proof by a computer theorem prover). However, it'll hardly convince you since apparently you have a problem with the provabilty/syntax representation rather than the proof itself.

[vc]

The essence of Gödel's incompleteness theorem is that you cannot have both completeness and consistency.

The above is rather a meaningless statement. There are complete and consistent theories out there, so yes you can have both assuming you know what you are talking about.

What follows is quite irrelevant to Gödel's incompleteness theorem unless it's some kind of joke.

A bold anthropomorphic conclusion is that there are three types of people; those that must have answers to everything; those that panic in the face of inconsistencies; and those that plod along taking the gaps of incompleteness as well as the clashes of inconsistencies in stride if they notice them at all, or else they succumb to the tragedy of the human condition.

The first kind are prone to refer to authorities; religion, bureaucracy, governments and their own prejudices. They postulate a Supreme Being that knows all the answers because everything must have an answer. With inconsistencies they deal by hopping over them, brushing them aside, sweeping them under a rug, ignoring them or making fun of them. These people are unpredictable and exasperating to deal with, though often disarmingly charming.

The second kind are the more heroic and independent thinkers. They are not afraid of vast expanses of the unknown; they forge ahead and rejoice over every new question opened up by questions answered. But when up against the walls of inconsistencies they go berserk. These claustrophobics are in fact the scientific minds.

And then, finally, there are the ordinary humans who make do with both inconsistencies and gaps in their experience of life and the world. Some of those, when driven to the brink of endurance by roadblocks of paradox and pitfalls of the unknown, go mad.

[olg2002]

...

По-моему очень хорошо характеризует участников данной дискуссии.