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:
One easy non-branching rule to apply is double negation elimination on 3.:
And one more non-branching rule is universal instantiation on 2., where the only useful constant to substitute is 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.