Интериоризация и экстериоризация диалогов

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

1. Пропонент начинает со сложной формулы (логического тождества)
2. Пропонент выигрывает, когда может заявить логический атом (a, b, c, ... – в противовес "формуле"), который ранее оппонент сам принял, и у оппонента не остаётся дальнейших ходов. Пропонент не может заявить логический атом, который ранее не принял оппонент.
3. В ответ на заявление импликации A → B вторая сторона отвечает принятием A. Далее первая сторона может либо атаковать A, либо заявить B.
4. В ответ на заявление конъюнкции A ∧ B (A и B) вторая сторона выбирает между A и B, после чего первая сторона продолжает выбранную ветку доказательства.
5. В ответ на заявление дизъюнкции A ∨ B (A или B) вторая сторона просит первую сторону выбрать между A или B, после чего первая сторона продолжает выбранную ветку доказательства.

Не трудно видеть, что процесс в точности похож на работу в "proof assistants", где роль пропонента соответствует цели (Goal) и манипуляцией с ней, а роль оппонента гипотезам (hypothesis) и работой с ними. "Интерактивное доказательство" с применением тактик это экстериоризация диалога программиста (пруф инженера), в котором компилятор следит за соблюдением правил, а программист переключается между ролями пропонента и оппонента.

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

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

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

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

Далее можно прикинуть и типовые застревания математического мышления (применяемого к повседневным вопросам), например:

1. Общее нарушение "правил игры", выход оппонента за разрешённый набор (по сути конкретизирующих) вопросов/возражений.
2. "Склейка" шагов оппонента и пропонента: такой стиль постоянного "да, но".
3. Бесконечное зацикливание в попытке взять перебором комбинаторно необозримое дерево вариантов.

Ранее обсуждали схожие темы:

– Непогрешимость математики (19.07.2020)
– Вкратце про обучение "матану" (13.08.2022)
– Суть программирования (4.03.2023)
– Евклид был не прав? (16.08.2024)
– Физики vs математики (7.07.2025)