Карри-Говард для FOL

[akuklev]

Как все тут знают, по соответствию Карри-Говарда интуиционистской логике высказываний (логике нулевого порядка) соотведствует просто-типизированное лямбда-исчисление с произведениями STLC

Comments

[vit_r]

Замечательно. А если нам нужна нечёткая логика.

[akuklev]

Тогда вам нужна нечеткая логика и другая семантика. Гвозди отверткой неудобно забивать, а шурупы молотком закручивать.

[66george]

Написал ликбез по нестандартному анализу, оцените свежим взглядом
https://mega.nz/#!Klx2TIrC!4WWrupBHPGMbrb-4Cq6wbjl4mpFbjlrxbRT2vRYqYPQ

[akuklev]

Мне очень понравилось, прочитал с удовольствием!

[66george]

Почему-то мне комментарии на почту не приходят. Нашёл и исправил один ляп - вводя аксиомы свёртывания, не указал ограничений на свободные переменные. В сообществе ru-math выложил исправленный вариант (наверняка ещё ляпчики будут), следите за обсуждением.

[akuklev]

Спасибо!

[clayrat]

а кстати как это соотносится с https://ncatlab.org/nlab/show/Heyting+category ?

[66george]

Что лучше, Agda или Idris? Хочу формализовать статью про альфа-конверсию.

[akuklev]

Для формализации equational theories Agda 2.6, чтобы Prop был.