
Все же как чудесно, что сподобился написать изрядно нудных букв с упоминанием Гёделя, Гильберта и формальной системы доказательств в разных ипостасях. И теперь могу писать намного меньше и чуть менее нудных букв.
Ссылку привожу для того, чтобы синхронизировать системы координат относительно конкретного вопроса - формальной системы доказательств в судебной системе. Краткое содержание: с этой методологией как-то не задалось. Инквизиторы недоинквизировали в свое время, а потом и вовсе начался бридж с куртуазными дамами в отдельно взятой отрасли знания. Не судьба.
Понимая и принимая, что система доказательства в судебной системе не является формальной системой в смысле Рассела и Уайтхеда(равно как и достаточным образом формализованной), становится понятной очень ограниченная применимость математической теории доказательств. Ограниченная - это я страхуюсь на случай встречи динозавра согласно известному анекдоту. В нашей реальности так сложилось, что доказательство хоть позитивного, хоть негативного утверждения в рамках судебной системы не может быть исчислено в смысле математической теории доказательств как минимум исходя из области применения. Потому граждане, приводящие там всяческие размышления, логически доказывающие существование Бога, суть пытаются забить гвоздь в другую стенку.
А так-то да, в состязательном судебном процессе принято доказывать положительные утверждения. И сторона обвинения, кстати, формулирует именно положительные утверждения, как бы парадоксально это не звучало. Грамотные адвокаты стараются придерживаться того же правила, если в целом. Но им куда как проще, т.к. не надо делать первый ход. Важно, что все они глубоко параллельны и Расселу, и Уайтхеду, и Гёделю, и Гильберту.
Отдельно и особо хочу заметить, что народ изрядно расслабился. Дело в том, что дискуссия эта может быть весьма интересной, если соревнующиеся стороны сделают чуть больше первого шага. Например, нетривиальной бывает ветка размышлений о возможности определения положительного и негативного утверждения. Проблема усугубляется хорошим потенциалом к обратимости среднепотолочного негативного(или положительного) тезиса. Да и вообще там отнюдь не бинарное дерево рассуждений, а сплошная полиамория.
В свое время понравился прикладной пример с лекарствами. В рамках описанных выше философских концепций - лекарство не считается опасным, пока не доказано наличие побочки. Тут тебе сразу и проблема определения положительности-негативности, и незамутненное "ei incumbit probatio, qui dicit, non qui negat", и отсутствие доказательств противного как доказательство существования етс. То, что закон тождества забудут практически сразу и практически все - гарантирую. Увлекательное чтиво, если только стороны быстро не скатятся в "сам дурак".
А сегодня народ подзабыл и Готфрида нашего Лейбница, и Гёделя, и чайник Рассела, и мегатонны религиозных споров... Жаль, искренне жаль. Хорошо, если макаронного монстра еще помнят.
PS: В принципе, возможен сценарий реанимации идеи формальной системы доказательств в суде. Дело в том, что тему автоформализации знаний и раньше раскачивали. А ныне, с нейросетками и бигдатами - риск велик, как никогда, буквально по краю ходим. Толку, конечно, не будет, но мозги загадят всем качественно. Одна надежда на case law.
PPS: Подумалось, что уже много лет не встречал дискуссий об онтологических аргументах. Или перехода в онтологическую дискуссию иной дискуссии, благо поводов и способов предостаточно. Еще в нулевых имело место, а сейчас увы и ах. Все же комбинаторные