Доказательственная сеть

В теории доказательств сети доказательств — это геометрический метод представления доказательств, которыеустраняет две формы бюрократии , которые различают доказательства: (A) нерелевантные синтаксические особенности обычных исчислений доказательств и (B) порядок правил, применяемых при выводе. Таким образом, формальные свойства идентичности доказательства более точно соответствуют интуитивно желательным свойствам. Это отличает сети доказательств от обычных исчислений доказательств, таких как исчисление естественной дедукции и секвенциальное исчисление , где эти явления присутствуют. Доказательные сети были предложены Жаном-Ивом Жираром .

В качестве иллюстрации эти два доказательства линейной логики идентичны:

$\vdash$ А , Б , В , Д $\vdash$ А ⅋ Б , С , Д $\vdash$ А ⅋ Б , С ⅋ Д

$\vdash$ А , Б , В , Д $\vdash$ А , Б , С ⅋ Д $\vdash$ А ⅋ Б , С ⅋ Д

И соответствующие им сети будут одинаковыми.

Критерии правильности

Известно несколько критериев правильности, позволяющих проверить, является ли структура последовательного доказательства (т. е. чем-то, что кажется сетью доказательств) на самом деле конкретной структурой доказательства (т. е. чем-то, что кодирует действительный вывод в линейной логике). Первым таким критерием является критерий дальней поездки , который описал Жан-Ив Жирар .

См. также

• Линейная логика
• Людис
• Геометрия взаимодействия
• Согласованное пространство
• Глубокий вывод
• Сети взаимодействия

Источники

• Доказательства и типы . Жирар Дж. Я., Лафон Ю. и Тейлор П. Cambridge Press, 1989.
• Роберто Ди Космо и Винсент Данос, Букварь по линейной логике
• Шон А. Фулоп, Обзор сетей доказательств и матриц для субструктурной логики