The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Hi Alex,

Alex Meyer 
<alex153 AT outlook.lv>
 writes:

> I am learning about logics that are used for legal reasoning and
> commonsense reasoning - like non-monotonic, defeasible, adaptable (and
> also categorical) logics. Can Coq be used as logical framwork for
> implementing those logics?

In principle yes, however the details are very important.
What do you exactly mean by "implementation"?

As a starting point, the below award-winning work on formalizing a
non-standard logic could provide you with a feeling on how different
approaches and tools work:

https://github.com/FormalTheology/GoedelGod
[the homepage of Christoph Benzmüller has more info]

> And generally - are there logics that can not be implemented in Coq
> and what should be added to Coq to make it into logical framework for
> those logics as well?

As in logical power, Coq is an extremely powerful system that won't be
usually be your primary concern.

> And even more generally - logics are only one kind of reasoning -
> deductive reasoning. What about other types of reasoning - abductive,
> inductive and analogical - and Coq?

It could be useful to make a distinction between "Coq's logic" and "what
Coq's logic can encode".

Native Coq's logic (*) would _very roughly_ correspond to predicate
intuitionistic logic. For instance, given the type Prop of propositions,
Coq won't be able to prove "∀ P : Prop, P ∨ ¬ P".

There are several ways to remedy this situation. The first one is by
extending Coq logical system with an axiom, in this case the excluded
middled is known to be non-problematic, however one has to be careful as
not to break consistency.

A different technique for representing logics in Coq does indeed not
rely on modifying the base theory, but in translations. In that case,
one would define the type of "extended" propositions "Propₒ", and would
provide a translation function for both propositions and proofs of them
such that the desired properties are met.

Thus assuming you new system is called "o", with a probability relation
⊢ₒ you would have to prove that:

Γₒ ⊢ₒ pₒ : Pₒ  ⇒  ⟦Γₒ⟧ ⊢ ⟦pₒ⟧ : ⟦Pₒ⟧

where ⊢ is the standard notion of probability in Coq.

E.

(*) known as the "Calculus of Inductive Constructions" (+ some extensions).