Какова связь между просто типизированным лямбда-исчислением и логикой более высокого порядка?
При Карри-Говарде кажется, что просто типизированное лямбда-исчисление соответствует логике высказываний. Как это связано с логикой высшего порядка? Согласно этому руководству Geuvers: http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf язык HOL выглядит как STT. Разве это не должно быть PROP? Что это значит?
Имел ли в виду Церковь HOL при определении STT?
Ответы:
Различие заключается в следующем: если STLC принимается как примитивный язык на конструкторах добавления на уровне типов и достаточно небольшого числа аксиом, чтобы дать вам полную выразительную силу HOL.
Взяв за базовый тип чисел ans ο за базовый тип предложений, вы можете добавить константы ∀ τ : ( τ → ο ) → οι ο
где - произвольный тип (так что одна ∀ константа для каждого типа). Один возможный набор аксиом:τ ∀
источник