The Coq mailing list

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

I don't know. I was hoping coq-club would know, or at least be able to muse. The musing part is happening, so that's good :)

I can define the term you've given me in Type, but not in Prop. I have to wonder if this is really a problem, though; you may get that Fin 0 -> False, but without eliminating False, there's no way to get that False -> Fin 0, and so there's no way to get False -> P. What you get is that some encoding of false via some other uninhabitable type -> P, but in this logic, that encoding does not imply False. It does sort of fundamentally change what False actually means though; not all uninhabitable types would imply each other anymore. There would, in that model, be uninhabitable types with constructors that explode, but uninhabitable empty types would not explode. Would this be meaningful?

If this wouldn't be meaningful, then what is the minimum set of restrictions one would need to make to prevent something like Jason's term (which I'm calling fin0_ind)?

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

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