In this particular sequent:

q ⊢(p∧q)∨(¬p∧q)

which is invalid (I drew a Truth Table, since it wasn't self-evident to me); the following explanation has been given:

The premise is q. By (tnd) we get p ∨ ¬p. We know start an assumption based proof based on the latter. Assume: p In this case by (∧i) we get p ∧ q. Assume: ¬p In this case by (∧i) we get ¬p ∧ q. Thus ¬p ∧ q holds only on the premise q.

I understand the need for a contradiction based assumption proof, however, I am having trouble connecting the last sentence in the explanation to proving invalidity. I actually had to draw a truth-table to see that this sequent was invalid.

My question is: how do I figure during writing my proof (the way it is formally done) that the sequent I am trying to proof is actually not valid? I continue to apply rules and things usually work out if the formulae are valid, but I can't seem to be able to tell during a proof that it is invalid.

  • $\begingroup$ Could you elaborate what you mean with the sequent being invalid? $\endgroup$ – Hagen von Eitzen Feb 10 '19 at 14:08

The end confuses me as well. I'd say you first show by Conjunction Introduction $$q,p\vdash p\land q$$ and from this by Disjunction Introduction $$q,p\vdash (p\land q)\lor (\neg p\land q)$$ and from this by Deduction $$\tag1q\vdash p\to ((p\land q)\lor (\neg p\land q)).$$ The same way, we show $$\tag2q\vdash \neg p\to ((p\land q)\lor (\neg p\land q)).$$ It seems you accept Tertium Non Datur $$\tag3\vdash p\lor \neg p, $$ so that we obtain by Disjunction Elimination from $(1)$, $(2)$, $(3)$ $$ q\vdash (p\land q)\lor (\neg p\land q).$$

| cite | improve this answer | |
  • $\begingroup$ My apologies, I actually made a mistake in my Truth Table, which is why I thought that the sequent was invalid. I took the mistake further by thinking the explanation was actually a proof for invalidity, and got confused because I did my own proof exactly like you wrote. Thank you. $\endgroup$ – haris.a.amin Feb 10 '19 at 14:26

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.