Why can I prove ⟦ ( ∃ x. P ) ∧ ( ∃ x. Q ) ⟧ ⟹ ∃ x. (P ∧ Q)?
isabelle
Solution
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.
Problem
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?