Why can I prove ⟦ ( ∃ x. P ) ∧ ( ∃ x. Q ) ⟧ ⟹ ∃ x. (P ∧ Q)?

Question

I'm an Isabelle beginner, learning the basics. To my surprise, I just proved

lemma "⟦ ( ∃ x. P ) ∧ ( ∃ x. Q ) ⟧ ⟹  ∃ x. (P ∧ Q)"
apply ( auto )
done

in Isabelle/HOL. Now assuming that P and Q range over arbitrary predicates, this is false, just instantiate P to x = 1 and Q to x = 2.

Of course the mistake must be on my side, but where is my misconception?

Answer 1

As was already indicated in the comment, P and Q in your example are not predicates, they are simply Boolean variables. If you type term P, you will get simply bool. Since HOL types are nonempty, ∃x. P is equivalent to P and similarly for Q, so your assumptions force P and Q to be True, which obviously implies the statement you proved.

What you meant is

lemma "⟦(∃x. P x) ∧ (∃x. Q x)⟧ ⟹  ∃x. P x ∧ Q x"

This is wrong, and simply by writing down the lemma, quickcheck will already provide you with a counterexample automatically.

Also note that the brackets ⟦…⟧ are not required for a single assumption (like in your case). Furthermore, it is uncommon to use the HOL conjunction operator ∧ to combine assumptions. You would more commonly state this lemma as

lemma "⟦∃x. P x; ∃x. Q x⟧ ⟹ ∃x. P x ∧ Q x"

or

lemma "∃x. P x ⟹ ∃x. Q x ⟹ ∃x. P x ∧ Q x"

This form is easier to handle than the one with the HOL ∧, since you can instantiate particular assumptions.