There is known connection between classical and modal logics and type theory (lambda calculus), but are there connections between nonmonotonic logics (e.g. defeasible logic) and type theory (lambda calculus)? Maybe HoTT provides some generatlization where such connections can be found?

If such connections can not be established then widely available proof assistants (Isabelle, Coq) are not useful for nonmonotonic logics, aren't they?

  • 2
    $\begingroup$ You might want to read about the linear lambda calculus. $\endgroup$ – chi Oct 3 '16 at 11:23
  • $\begingroup$ Is there any particular reason why you dragged HoTT into this question? $\endgroup$ – Andrej Bauer Oct 4 '16 at 16:29
  • $\begingroup$ I have just started to learn HoTT and I felt that it promises to be generalization that can handle all cases (if no, why this buzz?) but I now I am starting to se that this is not the case. Lambda calculi are generalized by lambda-mu calucli and they themselves are generalized by lambda-mu-ni and lambda-mu-T calculi and I don't know abut other calculi that can be related to nonmonotonic logic. Maybe there ois no sense to devise expressive calculi if no decidability can be achieved. $\endgroup$ – TomR Oct 4 '16 at 17:14

Your Answer


Browse other questions tagged or ask your own question.