Beginner: Help understanding interaction between quantification and implication

Using Coq
1

I’m having trouble understanding why I can’t prove a particular lemma:

Definition gen_prop := forall (X : Type) (p1 p2 : X -> X -> Prop),
  (forall x y, p1 x y <-> p2 x y) ->
  (forall x y, p2 x y -> False) -> 
  (forall x y, p1 x y) -> False.

Lemma gen_prop_contra : gen_prop.
Proof.
intros X p1 p2 H1 H2 H3.
eapply H1 in H3. apply H2 in H3. assumption.
Unshelve.
Abort.

2 goals
X : Type
p1, p2 : X -> X -> Prop
H1 : forall x y : X, p1 x y <-> p2 x y
H2 : forall x y : X, p2 x y -> False
______________________________________(1/2)
X
______________________________________(2/2)
X

So, I need an “example” instance of an X in order for this proof to work. E.g.:

Definition gen_prop' := forall (X : Type) (z : X )(p1 p2 : X -> X -> Prop),
  (forall x y, p1 x y <-> p2 x y) ->
  (forall x y, p2 x y -> False) -> 
  (forall x y, p1 x y) -> False.

Lemma gen_prop_contra' : gen_prop'.
Proof.
intros X z p1 p2 H1 H2 H3.
eapply H1 in H3. apply H2 in H3. assumption.
Unshelve.
all: assumption.
Qed.

I don’t understand why that is required. The non-quantified version is automatic:

 Lemma prop_contra : forall p1 p2 : Prop,
  (p1 <-> p2) -> (p2 -> False) -> p1 -> False.
Proof. intuition. Qed.

And the quantified version is automatic as long as I keep the quantification “outside”:

Definition gen_prop_outer_quant := forall (X : Type)
(p1 p2 : X -> X -> Prop)
(x y : X),
(p1 x y <-> p2 x y) ->
(p2 x y -> False) -> 
p1 x y -> False.

Lemma gen_prop_outer_contra : gen_prop_outer_quant.
Proof. intros X p1 p2 x y. intuition. Qed.

Similarly, if I’m working with a concrete type, e.g. nat, I can supply my own example as part of the proof:

Definition nat_prop' := 
forall p1 p2 : nat -> nat -> Prop,
  (forall x y, p1 x y <-> p2 x y) ->
  (forall x y, p2 x y -> False) -> 
  (forall x y, p1 x y) -> False.

Lemma nat_prop_contra : nat_prop'.
Proof.
intros p1 p2 H1 H2 H3.
specialize H1 with (x := 0).
specialize H1 with (y := 1).
apply H1 in H3. apply H2 in H3.
assumption.
Qed.

But I still don’t understand why I need to supply a nat at all here.

Structurally, the quantified one I want to prove seems like the same proof as the propositional version. And the additional quantifier I have to add to make Coq accept the proof doesn’t seem to contribute anything meaningful.

Am I doing the proof wrong? Or am I failing to understand something about the underlying logical system that makes my initial version invalid?

Any insight would be appreciated.

2

The initial version is invalid because X can be empty

Definition gen_prop := forall (X : Type) (p1 p2 : X -> X -> Prop),
  (forall x y, p1 x y <-> p2 x y) ->
  (forall x y, p2 x y -> False) ->
  (forall x y, p1 x y) -> False.

Lemma not_gen_prop : ~ gen_prop.
Proof.
  unfold gen_prop; intros H.
  apply H with (X := Empty_set) (p1 := fun _ _ => False) (p2 := fun _ _ => False).
  - intros _ _; apply iff_refl.
  - intros _ _; apply iff_refl.
  - intros _. apply Empty_set_ind.
Qed.
1 Like
3

Thank you. I’d like to understand where my reasoning broke down when I thought this was provable.

My thinking had been that since universal quantification doesn’t have existential import, X being empty wouldn’t make a difference.

Is this an issue because of something unique to constructive logic that I’m not understanding? Or is this also invalid in classical logic?

4

I don’t know what “existential import” means.

1 Like
5

Classical logic is constructive logic plus some extra axioms, so one can never invalidate a theorem by changing from constructive logic to classical logic. Therefore not_gen_prop is also a theorem in classical logic.

1 Like
6

Thank you. That makes sense. So the bottom line is that I misunderstood how quantifiers actually work with this sort of nesting.

If anyone has any good resources they found helpful for improving their understanding of the logic side of things past the “standard” 1st order logic material, I’d appreciate the recommendations.

This sort of stuff misunderstanding, especially around higher order quantification, seems to be what’s limiting me more than anything software related.

7

My thinking had been that since universal quantification doesn’t have existential import, X being empty wouldn’t make a difference.

On the contrary, because X can be empty, you have to consider that possibility, indeed you have exactly two cases here, namely: your statement is (provably) true if and only if X is inhabited.

The fact is, a universal quantifier is a dependent implication, so when the domain quantified over is empty, we get an identically true statement: whence all assumptions in your theorem are true if X is empty, and the theorem itself is necessarily false. On the other hand, if X is non-empty, the assumptions contradict each other and the theorem is true.

is this also invalid in classical logic?

The interpretation of implication and of proof in particular are quite different in constructive vs classical logic, but the above is basic enough that it holds classically, too: in fact, as @davidjao was saying, we can “embed” classical logic in Coq’s constructive logic by just introducing the needed axioms, whence any theorem of constructive logic is also a theorem of classical logic (but not the other way round). (“embed” in scare quotes as I am not sure about the terminology there: classical is a sublogic of constructive?)

(BTW, I have been told that in some treatments, especially in classical FOL, it is sometimes convenient or even customary to “assume a non-empty domain (of discourse)”, in which case one might say that universal quantification has “existential import”, in other words, forall x, P implies exists x, P: but it is only a convenience, i.e. there is an assumption, of inhabitance, even if just implicitly.)

1 Like
8

My knowledge of logic is limited to 1st order classical logic (and some basic extensions like modal logic), but in that limited context, a statement has existential import with regard to a term when it would be false if that term had no instances.

Specifically: forall x, P x is equivalent to ~(exists x, ~P x). So both of these can be true even in the case where x is empty.

But clearly something went wrong when I extrapolated from that to the assumption that existence wouldn’t matter in my gen_prop example.

Ah. I think I see now. If I’d been proving something other than False, my thinking might have worked. But since a universal quantification is true whenever the term is empty, then I can’t have it imply False until I show that it is non-empty.

Since, ~(forall x y, p1 x y) is the same as ~~ (exists x y, ~ (p1 x y)), I’m effectively making an existential assertion (at least classically; I still haven’t wrapped my head around how negation works in Coq).

If my new understanding is correct, this greatly clarified things. Thank you all for your help.

9

I have found overall very useful the Software Foundations series: in the Logical Foundations book there is a Logic chapter where you can find an introduction to understanding and doing logic in Coq up to considerations w.r.t. classical logic.

If I am not mistaken, (without classical axioms) the former implies the latter, not the other way round…

1 Like
10

I am working through that entire series now. I am part way through the second volume.

The Logic chapter helped, but I wouldn’t say I feel comfortable with constructive reasoning yet, especially when it comes to negation and proofs by contradiction.

I hope the repetition and exercises through the rest of that series will prove helpful in drilling it in.

I’ve also got the notes I took when working through Priest’s Introduction to Non-classical Logic some years ago, though that book focuses on semantic tableaux exclusively, and I probably need to see things from the perspective of proof theory to make it all click.

Thank you again for your help.

1 Like