I'm struggling with the following question:

Show the following derivability fact:

$P(c) \lor (P(c)\land Q(c)),\quad \forall x (Q(x) \implies \neg P(x)) \not\vdash \neg P(c)$

Also determine the associated model of at least one open branch.

This is how I would solve the problem:

Note, that $P(c) \lor (P(c)\land Q(c)) \equiv P(c) \land(P(c)\lor Q(c))$, so definitely $P(c)$. But if we rewrite the premises to $P(c),\; (P(c) \lor Q(c)),\; \left(\forall x :Q(x) \implies \neg P(c)\right)$, then it becomes apparent that $\neg P(c)$ is unsatisfiable, and hence $... \not\vdash\neg P(c)$.

The reason I'm unsure about this is that I don't use the second premise at all, nor do I mention the word "model". What am I missing?


In general, it is okay in a proof of whatever kind for a premise not to be used.

However, you are supposed to show $\not \vdash$ -- that is, non-derivability. This is about (the non-existence of) a formal derivation in some syntactic calculus. You are talking about truth and equivalence and unsatisfiability, but that is $\not \vDash$ (non-validity), not $\not \vdash$ (non-derivability) and hence off-topic to the actual question asked. That's what you're missing.

Since you're mentioning open branches, I assume you're working with tableaus aka truth trees?

In that case, showing $\not \vdash$ amounts to showing that no tree with all branches closed exist -- the tricky part here is to argue convincingly that there can indeed be no closed tree, so you will have to write a bit of argumentation; just presenting one unsuccessful tree without exploring further possibilities will not suffice.
Models are, for the moment, irrelevant, since they are about $\vDash$ and not about $\vdash$ -- however, syntactic calculi and semantic models obviously play together and there is an easy way to construct a counter-model from an open branch in a tableau tree, so we will do that at the end of the proof.

So let's start the proof tree by placing the premises and the negated conclusion:

  1. $P(c) \lor (P(c) \land Q(c))$
  2. $\forall x (Q(x) \to \neg P(x))$
  3. $\neg \neg P(c)$

One easy non-branching rule to apply is double negation elimination on 3.:

  1. $P(c)$

And one more non-branching rule is universal instantiation on 2., where the only useful constant to substitute is c:

  1. $Q(c) \to \neg P(c)$

From here on we have to branch, either on $\lor$ in 1. or on $\to$ in 5. Let's do the latter first, and apply one more double negation elimination:

       /          \
6. $\neg Q(c)$    7. $\neg \neg P(c)$
                  8. $P(c)$

And then we disassemble the disjunction in 1.:

                 /                                      \
            6. $\neg Q(c)$                            8. $P(c)$
       /                   \                      /                  \
9. $P(c)$    10. $P(c) \land Q(c)$    11. $P(c)$    12. $P(c) \land Q(c)$

At this point we have exhausted all possibilities for the leftmost branch (the one with leaf 9.), there are no more subformulas to disassemble. And it is obvious now that the leftmost branch can never be closed; there are no formulas in the same branch that contradict $P(c)$, and no other way to continue the branch such that it might eventually get closed. Since at no point could we have made a smarter decision that would have led to a different tree -- we just disassembled all subformulas available are step by step, and switching the order of some rule applications woulnd't help -- there exists no tree with all branches closed. Hence, $𝑃(𝑐)∨(𝑃(𝑐)βˆ§π‘„(𝑐)),βˆ€π‘₯(𝑄(π‘₯)βŸΉΒ¬π‘ƒ(π‘₯))βŠ¬Β¬π‘ƒ(𝑐)$.

And this is the proof of the non-derivability. Note that the argumentation at the end is an essential part of the proof -- you're not done by just showing an unfinishable tree.

One nice thing about tableau trees is that they give us a very straightforward way to construct an associated countermodel form an open branch, which is the second part of the exercise.
Remember that in a tableau tree, we are trying to close branches by deriving contradictions to the negation of the conclusion, so if a branch remains open, it will be non-contradictory, hence the open branches show us those possibilities where the true premises and the non-true conclusion happily live together -- and this is precisely what's going on in a counter-model.

To find the associated countermodel of an open branch, work your way up the branch and collect all the formulas that you find on the way, that is, create a model as simple as possible in which 1. $P(c)$ holds and 2. $\neg Q(c)$ holds, i.e. $Q(c)$ doesn't hold. The simplest such model is

$$\mathcal{M} = \langle A, \mathcal{I} \rangle$$ with $$A = \{c\}$$ $$\mathcal{I} : P \mapsto \{c\}, Q \mapsto \emptyset$$

It is easy to see that in this model, the premises are true but the conclusion $\neg P(c)$ is false, hence, it is a countermodel to the validity of the inference ($\vDash$).

Now that I showed you how it works, as an exercise you can try to come up with counter-models for the other open branches.

If you are allowed to use soundness and completeness, you can just present the counter-model and thereby avoid the cumbersome argument talking about non-existent trees, but it looks like the purpose of the exercise is to practice specifically tableau trees with open branches.

  • $\begingroup$ I haven't read the full post yet; but the primary proof tool in this course is the tableaux. I'm trying to avoid those as much as possible ^_^' $\endgroup$ Oct 30 '19 at 20:03
  • $\begingroup$ Well, it looks like you can't avoid them here, because the exercise is about those tableaux. (What I'm calling "tree" is nothing else than what you call "tableau".) $\endgroup$
    – lemontree
    Oct 30 '19 at 20:04
  • $\begingroup$ Wait... Can't you use natural deduction to show $P(c)$ to be unproveable? The answer key mentions specifically that any valid proof is accepted; which in this case would be a proof of unproveability + a model. The reason I try to avoid the tableaux is because I have several years of formal mathematical background, making them a lot harder to reason about than "normal" proof techniques. $\endgroup$ Oct 30 '19 at 20:12
  • $\begingroup$ In principle, as long as you have soundness and completeness, you can switch between different calculi and semantic proofs however you like; but the addition "determine the associated model of at least one open branch" makes it very likely that you are supposed to work specifically with tableaus, since there is no such thing as open branches in natural deduction. But I'm not the one who designed that exercise, so if you're unsure about which methods you are allowed to use, you should ask your instructor for clarification. $\endgroup$
    – lemontree
    Oct 30 '19 at 20:17

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.