The universal/existential quantifier:

In classical logic, ~∀x P(x) is equivalent to ∃x ~P(x). Looking at the existential quantifier in Lean4, the object ∃ x:nat P(x) is essentially the tuple (x:nat, P(x)), containing a natural number and a proof that the number satisfies the proposition. Looking at the universal quantifier in Lean4, ∀x P(x), it can be constructed by an object of type x -> P(x), which would indicate that for any x, you can use x -> P(x) to create the proposition P(x).

I was curious as to whether equivalence between ∃x ~P(x) and ~∀x P(x), holds in type theory. However, I am having trouble understanding what the negation of a quantifier in type theory would actually mean.

For example, if ∃x P(x) is the tuple (x, P(x)), then ~∃x P(x) would seem to sound like "not the tuple (x, P(x))"? Also, if ∀x P(x) is an object containing a x -> P(x), then does that mean ~∀x P(x) is saying "not the object (x -> P(x))". It almost seems like it doesn't make sense to negate a quantifier (or proposition) in type theory, or is there something I'm missing?

The empty set and the empty type:

In set theory, you learn that for the empty set {} and a proposition, ∀ x∈{} P(x), because the equivalent form ∃x ~P(x) is false by virtue of the fact that the empty set cannot contain a counter example ~P(x).

Is there a corollary in type theory, i.e. can the Lean4 inductive "Empty" type be such that forall x : Empty, P(x), because when you do a destruct/cases commands, there are no cases, so it must be true in all cases?

Edit: I've tried typing this in:

theorem for_all_in_empty_true (P : Empty → Prop) : ∀ x : Empty, P x := by
intro h
cases h

But it feels weird, I can't put my finger on why, it feels like the concept of a proof by cases is somehow borrowing from classical logic, probably because I don't understand fully the universal/existential quantifiers in type theory yet.

Empty List?

Can you prove regarding def mylist := [], for all x in nat, that x ∈ mylist -> P(x), by virtue of the fact that there are no counter examples? (My intuition tells me this cannot be done, since there is no constructivist structure defining the elements in the list to create a proposition P(x), I just don't have enough lean4 experience to actually try this, I'm only able to inspect the definitions at this point).



1 Answer 1


The universal/existential quantifiers and their negations

In type theory, negation is defined as a shortcut for "implying falsity", in other words ~ P is *defined to be P -> False. Thus, ~∃x P(x) roughly means "the existence of a tuple (x,p) with p : P x implies falsity/is absurd", and ~ ∀ x, P(x) means "assuming we can construct a proof of P(x) for all x implies falsity".

Constructively, it is easy to show that for any A and P, ~ ∃ x : A, P x implies ∀ x : A, ~ P x. Indeed, assuming ~ ∃ x : A, P x and given some x : A, we must show ~ P x, ie P x -> False. So we can assume P x too, and must derive False. Now we can apply ~ ∃ x : A, P x (which is ∃ x : A, P x -> False), and so must derive ∃ x : A, P x. But we have an x such that P x already, and so we are done. Conversely, if we assume ∀ x : A, ~ P x we can show ~ ∃ x : A, P x by a very similar reasoning.

The other distribution, however, is not so easy. We can show that ∃ x : A, ~ P x implies ~ ∀ x : A, P x: deconstructing the negation in the goal we get the assumption that ∀ x : A, P x, and we can deconstruct our first hypothesis to obtain an x and a np : ~ P x. But then we can also deduce that P x holds from our second assumption, and combine that with np to get a proof of False, as needed. But for the second one, we assume ~ ∀ x : A, P x, and must show ∃ x : A, ~ P x. How are we supposed to construct this x? All we know is that assuming ∀ x : A, P x leads to falsity, but that does not really help us… Of course, if we can resort to excluded middle or some strong form of choice, we might be saved, but that is not constructively valid any more.

I encourage you to try and do the three proofs I mentioned by yourself in Lean, and fight a bit with the fourth, impossible one, to get a feel of what happens. You can even try them by replacing negation with "entails Q for a fixed, abstract Q, which will show that none of these proofs actually rely on special properties of False.

The empty set

Your confusion stems from the fact that classical logic lets you do a very special kind of proof by cases: those where you do a case-split on whether a certain proposition is true or false. That does not mean that case-splitting is never allowed constructively: all programmers write if statements many times a day! The difference is that this is not case-splitting on "truth", but on a data-type (here, a boolean) being of a specific form.

Things are a bit blurred for booleans, because in the classical world it is easy to confuse propositions (which are true or false by excluded middle) and booleans (which are true or false because they are a data-type with two constructors). But this is very different! Truth or falsity for propositions means the existence of a proof or counter-proof, while for booleans true and false is just a naming convention, but we could as well have named the two constructors foo and bar.

Case-splitting on data-types is not restricted to booleans: for instance, with natural numbers defined inductively as either 0 or the successor of another natural number, it is equally easy to split on whether a given natural is 0 or non-zero. Similarly, you can also case on a list being empty or a cons, etc.

All the data-types I mentioned so far have only two constructors, but that's just a coincidence: if a data-type has 14 constructors, then case-splitting on it will give 14 cases. And if it has no constructors, then case-splitting will give… no cases. That's just a degenerate and slightly weird case, but still perfectly fine.

The empty list

This depends on how exactly you define membership in a list.

As far as I know, the most standard way is as an inductive predicate with two cases: x ∈ x :: l, and x ∈ l -> x ∈ (y :: l). With this definition, you can see that x ∈ l implies that l actually needs to be of the form y :: l'. So in particular, x ∈ [] implies that [] = y :: l' for some y and l', and from this you can derive False (the proof of that by hand is a bit involved, but I think Lean has a tactic for this kind of things).

But in any case, whatever the definition of I would be quite surprised if you were unable to derive ∀ x. ~ (x ∈ []). You might need some sort of excluded middle if the definition of was baking that in, but for sure there are good ways to define it where you don't need it at all.

  • 1
    $\begingroup$ Another exercise could be: show that $¬(∀b:\mathsf{Bool}.P(b)) → ∃b:\mathsf{Bool}. ¬P(b)$ (for the 2 element type $\mathsf{Bool}$) allows you to derive weak excluded middle $¬Q ∨ ¬¬Q$ which is a non-constructive axiom in general. $\endgroup$
    – Dan Doel
    Commented Apr 11 at 15:13
  • $\begingroup$ Black belt exercise: you can even show that the two are equivalent. My guts tell me that the more general $\neg (\forall x : A. P(x)) \to \exists x : A.\neg P(x)$ for all $A$ and $P$ is stronger than WEM, but I don't know how to prove this, nor what kind of excluded-middle-like statement it could be equivalent to. $\endgroup$ Commented Apr 12 at 9:29
  • 1
    $\begingroup$ The general version yields $¬¬T → \Vert T \Vert$ and therefore full excluded middle. $\endgroup$
    – Dan Doel
    Commented Apr 12 at 17:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.