deniok: (Рыжий)
deniok ([personal profile] deniok) wrote2013-09-19 08:26 pm

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

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

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

[identity profile] dmitry gerasimov (from livejournal.com) 2013-09-19 04:57 pm (UTC)(link)
Похоже на (¬ ¬ φ) → φ, если записать как ((φ → ⊥) → ⊥) → φ.
А где курс читаете?

[identity profile] deni-ok.livejournal.com 2013-09-19 05:01 pm (UTC)(link)
Ага, только чуть обобщить можно.
В СПбАУ.

[identity profile] deni-ok.livejournal.com 2013-09-19 05:10 pm (UTC)(link)
То есть вру, не обобщить, конечно.

[identity profile] migmit.livejournal.com 2013-09-19 09:35 pm (UTC)(link)
Господи, неужели мои лекции тоже так смотрятся со стороны?

[identity profile] deni-ok.livejournal.com 2013-09-19 09:50 pm (UTC)(link)
Не, ну это полезный педагогический прием: изредка доводить плотность терминов до уровня гротеска. Важно держать этот процесс под контролем)

[identity profile] migmit.livejournal.com 2013-09-19 10:47 pm (UTC)(link)
Слушай, оффтопик: ты вашей sewiki пользуешься? Как в ней зарегистрироваться?

[identity profile] deni-ok.livejournal.com 2013-09-20 04:49 am (UTC)(link)
Нет, не пользуюсь. Я все кидаю в список рассылки курса. Напиши О, попроси.