Протокол сопоставления логических систем: авторское изложение

ru · official · sha256:95c36be7601304a5289f622246ee7b499f2ac97fc34428e800b77814b1652e9b

ПРОТОКОЛ СОПОСТАВЛЕНИЯ ЛОГИЧЕСКИХ СИСТЕМ: АВТОРСКОЕ ИЗЛОЖЕНИЕ Настоящий документ является АВТОРСКИМ ИЗЛОЖЕНИЕМ, составленным для целей формализации пакета logic.comparisons. Он не содержит ни одного утверждения о том, что верно в какой-либо логической системе: всё, что здесь сказано, относится к УСТРОЙСТВУ СОПОСТАВЛЕНИЯ — какие стороны обязано назвать сравнение и чего оно не утверждает. СОБСТВЕННЫХ ФАЙЛОВ ИСТОЧНИКА У ЭТОГО ПАКЕТА НЕТ, И ЭТО ПРАВИЛО, А НЕ ПРОБЕЛ. Всякое содержательное утверждение о сравниваемых системах — о том, что интуиционистски эквивалентны три схемы, что двойное отрицательное преобразование переводит классически доказуемое в интуиционистски доказуемое, что классическое правило сведения к противоречию не входит в интуиционистский естественный вывод, — анкеруется межпакетно на закреплённые байты тех пакетов, где эти утверждения стоят: logic.classical, logic.intuitionistic, logic.calculi, logic.semantics. Сравнение не заводит второй копии байтов сравниваемого. Настоящее изложение не является нормативным актом и не имеет силы источника права ни в одной юрисдикции.

ru · official · sha256:7aac63394954134bafe9a68180ce71da3422bcf6a5e208d51f03b5488c0c2456

Раздел 1. Что обязано назвать сопоставление двух систем. Сопоставление, состоящее из слов «эти системы различаются», сравнением не является. Всякое сопоставление в настоящем пакете обязано назвать пять вещей: язык или фрагмент языка, в котором сравнение вообще осмысленно; КОНКРЕТНЫЙ принцип либо КОНКРЕТНОЕ правило, по которому системы расходятся; сторону, которая его принимает, и сторону, которая его отвергает; условие, при котором метод одной системы применим в другой; и источник каждого из этих утверждений. Сопоставление, у которого не названа хотя бы одна из пяти сторон, настоящим пакетом не заводится.

Ссылаются нормы: ComparisonComplete, compared, comparison_complete

ru · official · sha256:a20d2313cee6d86268767bc02d2ff43f7d19d5b4fa2321ff0c371ca608a01c14

Раздел 2. Общий язык и общий фрагмент. Две системы сравнимы постольку, поскольку у них есть общий язык либо общий фрагмент языка: утверждение «в одной системе выводимо то, что в другой не выводимо» имеет смысл только для формул, записываемых в обеих. Общий фрагмент вычисляется, а не объявляется: понятие принадлежит общему фрагменту, если оно объявлено принадлежащим обоим языкам. Там, где общего фрагмента нет, сопоставление ограничивается переводом (раздел 6) либо не производится вовсе.

ru · official · sha256:6e76a7eaa0f615c52262049d012b260c683bf0ddba78c6551b555143559efcb2

Раздел 3. Различие принципов и различие правил — разные утверждения. Система принимает ПРИНЦИПЫ; исчисление содержит ПРАВИЛА. Две системы могут расходиться принципом, будучи представлены исчислениями с одинаковыми именами правил, и наоборот. Поэтому настоящий пакет ведёт два разных сопоставления: по принципам (одна принимает, другая отвергает) и по правилам (правило одного исчисления чуждо другому). Ни одно из них не выводится из другого, и подменять первое вторым запрещено.

Ссылаются нормы: ComparisonNamesPrinciple, ComparisonNamesRule, comparison_names_principle, comparison_names_rule

ru · official · sha256:86f88c9ae3c27e2e39b26b89f0b27267de56554fe99424146ca0ab71df549c30

Раздел 4. Условие переноса метода. Метод одной системы применим в другой, если КАЖДОЕ правило, которым метод пользуется, принадлежит исчислению второй системы. Условие проверяемо и проверяется: счёт чужих правил метода в исчислении должен быть нулевым. Утверждение «метод классический» условием не является и здесь не употребляется: классическим метод делает конкретное правило на конкретном шаге, и оно называется.

Ссылаются нормы: MethodTransfers, TransferBlockedBy, method_transfers, transfer_blocked_by

ru · official · sha256:2927b1b6975227e0388c336bdb5caca534c6e958065eb879c2adb71324d09667

Раздел 5. Расширение и ограничение. Одна система есть ОГРАНИЧЕНИЕ другой, если её исчисление получается из исчисления второй удалением правил без добавления новых. Одна система есть РАСШИРЕНИЕ другой, если её исчисление получается добавлением правил либо схем без удаления. Оба отношения устанавливаются перечислением конкретных правил, а не общим впечатлением о силе систем.

Ссылаются нормы: RestrictionNamesARule, restriction_names_a_rule, restricts_system

ru · official · sha256:fd9ad10cdbc0eb602d663a057a84f7241587b6784ee3ad26e86996ab9daa2043

Раздел 6. Перевод формул и результаты о переводах. Переводом называется заданное преобразование формул одного языка в формулы другого (либо того же), определённое индукцией по построению формулы. Перевод описывается ПОФОРМУЛЬНО: для атомарной формулы, для каждой связки, для каждого квантора. Результаты о переводе — что перевод сохраняет доказуемость, что исходная формула и её перевод эквивалентны в одной из систем — приводятся как УТВЕРЖДЕНИЯ ИСТОЧНИКА с локатором и настоящим пакетом не доказываются.

Ссылаются нормы: NEGATIVE_TRANSLATION, TranslationClauseCount, TranslationWithResults, translation_clause, translation_is_total, translation_of, translation_result, translation_with_results

ru · official · sha256:f6ba36aede14ce581fd717df5b275017b4ccbf5add87cc77168919af13b51e0d

Раздел 7. Чего сравнение не утверждает. Сравнение не утверждает, что одна система «лучше» другой: такого отношения в пакете нет. Оно не утверждает, что система, отвергающая принцип, доказывает его отрицание: отвергнуть принцип значит не иметь его среди доказуемого, а не иметь его отрицание. Оно не переносит СТАТУС правила из исчисления в исчисление: правило, основное в одном, может быть производным, допустимым либо чуждым в другом. И оно не выводит различия из молчания: если об отношении системы к принципу не сказано ничего, сопоставление по этому принципу не производится.