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, 2016 at 11:23
  • $\begingroup$ Is there any particular reason why you dragged HoTT into this question? $\endgroup$ Oct 4, 2016 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, 2016 at 17:14


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.