The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Is there an existing theory that combines paraconsistent logic with dependent types?  You can do a lot with just the Church encoding of inductives, and all you need for that is Pi.

On Thu, Mar 28, 2019, 23:52 Talia Ringer <tringer AT cs.washington.edu> wrote:

Interesting! I can't say I had a plan; I thought of this while going for a run 30 minutes ago. I wonder if there's a restriction that it is possible to place either on inductive types or on pattern matching that makes this possible, but still leaves a useful and interesting set of inductive types and their eliminators. 

On Thu, Mar 28, 2019 at 8:49 PM Jason Gross <jasongross9 AT gmail.com> wrote:

What are your plans for the Church encoding of False := forall A : Prop, A?

I think you can also get False_ind by defining Fin : nat -> Set and then doing a match on an element of Fin 0:

(fun A x => match x in Fin n return match n with O => A | _ => True end with <each ctor> => I end) : forall A, Fin 0 -> A

On Thu, Mar 28, 2019, 23:38 Talia Ringer <tringer AT cs.washington.edu> wrote:

I anticipate being bored next week, and I'd like a quick, fun, and interesting side project to fill my time (and I'm familiar enough with the Coq internals that playing with the code can meet these criteria). I think, if so tasked, I could write a paraconsistent proof assistant from scratch. But what if I wanted to fork Coq and trim it down to a paraconsistent proof assistant? What is the minimal set of changes I would need to make?

Clearly, I would need for the principle of explosion to no longer hold, which means that False_ind and similar terms should no longer type-check. This means that empty pattern matching ought to be impossible, since in Coq:

False_ind :=

  fun (P : Prop) (f : False) => match f return P with end

: forall (P : Prop), False -> P.

It looks like in so doing, I would make disjunctive syllogism (forall A B, or A B -> ~ A -> B) impossible to prove, since I think all proofs of this in Coq must go through a term like False_ind. Am I wrong?

If this makes disjunctive syllogism unprovable, then I would not need to remove or_introl or or_intror. Does this mean that I could keep inductive types? Or would they cause unforeseen problems?

What about other features that Coq has?

Best,

Talia