Обозначение Фитча

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

Пример [ править ]

Каждая строка в доказательстве в стиле Fitch является либо:

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

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

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

0 |__                        [assumption, want P if not P]
1 |   |__ P                  [assumption, want not P]
2 |   |   |__ not P          [assumption, for reduction]
3 |   |   |   contradiction  [contradiction introduction: 1, 2]
4 |   |   not not P          [negation introduction: 2]
  |
5 |   |__ not not P          [assumption, want P]
6 |   |   P                  [negation elimination: 5]
  |
7 |   P iff not not P        [biconditional introduction: 1 - 4, 5 - 6]

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

См. также [ править ]

Естественный вычет

Ссылки [ править ]

Фитч, Фредерик Брентон (1952). Символическая логика: Введение . Рональд Пресс Ко.

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

Внешние ссылки [ править ]