6
$\begingroup$

Update: Updated the title now that I've observed that we can use math in the title. I've also gone thru and removed dots. The tool expresses quantification using dots like this $\forall x.P(x)$ rather than $\forall x P(x)$. I originally used these dots in my post as well.

I'm going through all of the proofs in The Incredible Proof Machine and need a hint for one of the proofs. (The Incredible Proof Machine is an online graphical proof tool.)

Given: $(\forall x P(x)) \to A $
Prove: $\exists x (P(x) \to A )$

It seems like a trivial proof and here's my hand-waving attempt: There are two cases to consider:

  1. $\forall(x) P(x)$: In this case its trivial to prove the conclusion since we can prove $A$.
  2. $\neg \forall(x) P(x) $ In this case it must be that there exists some $c$ such that $ \neg P(c)$. Therefore trivially, $P(c) \to A$ and therefore $\exists x (P(x) \to A)$.

However, I get stuck trying to prove it using the actual logic connectors available in the tool. I'm not able to use the same approach in the second case of my case analysis (or at least I'm not sure how). This is my attempt:

Proof Image

If you look right in the middle of the diagram you'll see there are no connections (and a small red dot indicating an error). This approach doesn't seem to lead anywhere.

I'm using two instances of TND to do case analysis. The first case is as described above. But I don't know how to handle the second case, so I used a TND in the second case to generate two sub-cases: $P(y_{10}) \vee (P(y_{10}) \to \bot)$. The second case of this TND is again trivial, but the first case doesn't lead anywhere.

In the middle of the proof I have two facts $P(y_{10})$ and $(\forall x P(X)) \to \bot$. These two facts don't seem like they can lead to the conclusion.

I'm looking for a hint of an approach to try to solve this proof.

$\endgroup$
  • $\begingroup$ I'm wondering if there is a way to use the universal introduction rule to transfer P(y10) into $\forall x.P(x)$. No attempt I tried worked. If it did work, then we could prove $\bot$ and therefore prove the conclusion. $\endgroup$ – Michael Welch Dec 14 '15 at 22:52
  • $\begingroup$ This is a question for the implementers or user community of the software. $\endgroup$ – Rob Arthan Dec 14 '15 at 23:05
  • 1
    $\begingroup$ I'm voting to close this question as off-topic because MSE is an inappropriate forum for help in using a new online resource. $\endgroup$ – Rob Arthan Dec 14 '15 at 23:08
  • 3
    $\begingroup$ I appreciate the concern. However I feel my question is not about the tool, it's about the proof. If you look at the tool, it's using a set of standard logic rules. These rules should apply no matter what tool you are using. If I determine there is a bug in the system that prevents me from solving the proof, that would be a question for the tool owner. $\endgroup$ – Michael Welch Dec 14 '15 at 23:22
  • $\begingroup$ I could just as easily remove the image and any mention of the tool and rephrase my question using just standard logic rules, however it would be more difficult for me to do so. $\endgroup$ – Michael Welch Dec 14 '15 at 23:24
2
$\begingroup$

For other interested parties, I did get some hints from the tool community. If you wish to review these they are on this issue at GitHub

UPDATE: I finally finished the proof. The key to success was figuring out (with help) how to prove the identity $\neg \forall x P(x) \Rightarrow \exists x (\neg P(x))$. That identity was not built into the tool and can be a little tricky/cumbersome to prove from axioms. If you attempt the proof using the tool, learn how to create custom blocks like "proof by contradiction" and "case analysis". Otherwise the proof gets very messy. Here's the finished proof (still a little messy).

The blocks with the snowmen on them are "proof by contradiction". The block with baseball is case analysis.

Finished Proof

$\endgroup$
  • $\begingroup$ You really ought to be able to easily switch quantifiers. Is this a new program? My own DC Proof 2.0 has been around for years. I never would have released it without being able to switch quantifiers. Visit my website at http//www.dcproof.com $\endgroup$ – Dan Christensen Dec 18 '15 at 6:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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