нотация Fitch

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

Каждая строка в доказательстве в стиле Фитча представляет собой:

• предположение или предположение, не являющееся доказательством.
• предложение, обоснованное ссылкой на (1) правило вывода и (2) предшествующую строку или строки доказательства, которые подтверждают это правило.

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

В следующем примере показаны основные особенности нотации Fitch:

0 |__ [предположение, хочу P, если не P]1 | |__ P [предположение, хочу не P]2 | | |__ не P [предположение, для сокращения]3 | | | противоречие [введение противоречия: 1, 2]4 | | не не P [введение отрицания: 2] |5 | |__ не не P [предположение, желание P]6 | | P [исключение отрицания: 5] |7 | P если и только если не не P [двуусловное введение: 1 - 4, 5 - 6]

0. Нулевое предположение, т. е . мы доказываем тавтологию
1. Наше первое поддоказательство: мы предполагаем, что левая часть, чтобы показать, что правая часть следует
2. Поддоказательство: мы вольны предполагать, что хотим. Здесь мы стремимся к сведению к абсурду
3. Теперь у нас есть противоречие
4. Нам разрешено ставить перед утверждением, которое «вызвало» противоречие, префикс not
5. Наше второе поддоказательство: мы предполагаем, что правая часть, чтобы показать, что левая часть следует
6. Мы вызываем правило, которое позволяет нам удалить четное количество not из префикса утверждения
7. От 1 до 4 мы показали, что если P, то не не P, от 5 до 6 мы показали, что P, если не не не P; следовательно, нам разрешено ввести двуусловие в 7, где iff означает тогда и только тогда, когда

• Натуральный вычет

• Фитч, Фредерик Брентон (1952). Символическая логика: Введение . Ronald Press Co.

• Баркер-Пламмер, Дэйв; Барвайз, Джон ; Этчеменди, Джон (2011) [1999]. Язык, доказательство и логика (2-е изд.). CSLI Publications. стр. 606. ISBN 9781575866321.

• Парадокс известности Fitch
• Онлайн-приложение Java для построения доказательств. Архивировано 2006-10-02 на Wayback Machine.
• Веб-реализация системы доказательств Fitch (пропозициональной и первого порядка) на proofmod.mindconnect.cc
• Универсальный помощник по проверке доказательств Jape (см. Jape )
• Ресурсы для набора корректур в нотации Fitch с помощью LaTeX (см. LaTeX )
• FitchJS: веб-приложение с открытым исходным кодом для построения доказательств в нотации Fitch (и экспорта в LaTeX)
• Редактор и проверяющий инструмент для проверки естественного вычета в нотации Fitch