The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

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