Читаю тут курс матлогики

[deniok]

Контрприменяю правило введения импликации в сукцедент секвенции, затем контрприменяю правило введения импликации в антецедент секвенции, затем опять контрприменяю правило введения импликации в сукцедент секвенции, и мы у цели: оба листа дерева поиска вывода суть аксиомы.

Упражнение на вывод типов: вывод какой тавтологии пропозициональной логики я строю в исчислении секвенций?

Comments

[dmitry gerasimov (from livejournal.com)]

Похоже на (¬ ¬ φ) → φ, если записать как ((φ → ⊥) → ⊥) → φ.
А где курс читаете?

[deni-ok.livejournal.com]

Ага, только чуть обобщить можно.
В СПбАУ.

[deni-ok.livejournal.com]

То есть вру, не обобщить, конечно.

[migmit.livejournal.com]

Господи, неужели мои лекции тоже так смотрятся со стороны?

[deni-ok.livejournal.com]

Не, ну это полезный педагогический прием: изредка доводить плотность терминов до уровня гротеска. Важно держать этот процесс под контролем)

[migmit.livejournal.com]

Слушай, оффтопик: ты вашей sewiki пользуешься? Как в ней зарегистрироваться?

[deni-ok.livejournal.com]

Нет, не пользуюсь. Я все кидаю в список рассылки курса. Напиши О, попроси.