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

[deni_ok]

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

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

Comments

[ext_356277]

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

[deni_ok]

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

[deni_ok]

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

[migmit]

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

[deni_ok]

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

[migmit]

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

[deni_ok]

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