The Coq mailing list

[Ben Sherman <sherman AT csail.mit.edu>]

Here’s a proposal:

What if you take the category of presheaves over the discrete set with two points (i.e., the set with two points, which are incomparable to each other), i.e., the category Set * Set, and then add special terms for new version of the logical operations as follows: 

Definition para A := bool -> A.

Definition to_para {A} (x : A) : para A := fun _ => x.

Definition mk_paraprop (proof refutation : Prop) : para Prop :=

  fun b : bool => if b then proof else refutation.

Definition proof (p : para Prop) : Prop := p true.

Definition refutation (p : para Prop) : Prop := p false.

Definition true_and_false : para Prop := to_para True.

Definition ptrue : para Prop := mk_paraprop True False.

Definition pfalse : para Prop := mk_paraprop False True.

Definition pneg (p : para Prop) : para Prop := mk_paraprop (refutation p) (proof p).

Definition pand (a b : para Prop) : para Prop :=

  mk_paraprop (proof a /\ proof b) (refutation a \/ refutation b).

Definition por (a b : para Prop) : para Prop :=

  mk_paraprop (proof a \/ proof b) (refutation a /\ refutation b).

Definition pimpl (p q : para Prop) : para Prop := por (pneg p) q.

Definition impl (p q : para Prop) : Prop := (proof p -> proof q) /\ (refutation q -> refutation p).

Theorem no_explosion : ~ (forall p : para Prop, refutation p -> forall q : para Prop, impl p q).

Proof.

  intros contra.

  apply (contra (true_and_false) I pfalse).

  apply I.

Qed.

Then `para Prop` forms a quasi-Boolean algebra, which can model paraconsistent logic.

The Theorem `no_explosion` is an interpretation (my interpretation) of what it means for the principle of explosion to no longer hold.

Then you could presumably use Coq’s forcing plugin (https://www.pédrot.fr/articles/lics2016.pdf) to translate Coq terms into terms of this topos (again, where you’d have special constants for the logical terms, since their meanings would be different). I’m not sure I really understand how the set-level operations interact with the logic. A term G |- e : A corresponds to a pair of maps from G to A, one for the “true” world and one for the “false” world. The key interaction with the logic is that Boolean negation swaps the two worlds. Maybe that’s not so meaningful. I don’t really understand! You might be interested in this:

Linear Logic for Constructive Mathematics

Michael Shulman

https://arxiv.org/abs/1805.07518

I don’t remember that paper well but likely it focuses on those “dual pairs of propositions” that never have both proofs and refutations.

From: Talia Ringer <tringer AT cs.washington.edu>

Subject: [Coq-Club] Just for fun: From Coq to a paraconsistent poof assistant

Date: March 28, 2019 at 11:37:26 PM EDT

To: Coq-Club <coq-club AT inria.fr>

Reply-To: coq-club AT inria.fr

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