<p>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?</p>

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

CC BY-SA 3.0
2016-10-03T11:23:21.147Z
You might want to read about the [linear lambda calculus](https://www.cs.cmu.edu/~fp/courses/15816-f01/lectures/lecture15.html).
chi
CC BY-SA 3.0
2016-10-04T16:29:37.790Z
Is there any particular reason why you dragged HoTT into this question?
Andrej Bauer
CC BY-SA 3.0
2016-10-04T17:14:54.707Z
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.
TomR
<lo.logic><type-theory><lambda-calculus>
Connection between nonmonotonic logic and type theory (lambda calculus)
TomR
# Connection between nonmonotonic logic and type theory (lambda calculus)

(Asked by: username_0 on 2016-10-03)

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?

**Tags:** lo.logic, type-theory, lambda-calculus
> **Comments:**
> **username_1**: You might want to read about the [linear lambda calculus](https://www.cs.cmu.edu/~fp/courses/15816-f01/lectures/lecture15.html).  
> **username_2**: Is there any particular reason why you dragged HoTT into this question?  
> **username_0**: 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.  

---

## 0 answers

