We know that p → q is not equivalent to q → p. But suppose we make a proof system that has all the rules of logical identities plus the rule (“commutativity of implies”) p → q ≃ q → p. (We are using the new symbol ≃ because these are not really equivalent.)

This new proof system is not sound. The point of this question is to show that you can prove any contradiction in this system.

Prove true ≃ false in this proof system.

Hint: You might want to start your chain of ≃ in the middle with false → true ≃ true → false. Note that the logical identities do not include a rule ¬true ≡ false, so if you want to use this, you should derive it from the other logical identities.

How do I go about starting this proof? Can someone explain the hint to me?


EDIT: Here's a list of identities we're allowed to use.


p∧q ≡ q∧p

p∨q ≡ q∨p

p↔q ≡ q↔p


p∧(q∧r) ≡ (p∧q)∧r

p∨(q∨r) ≡ (p∨q)∨r


p∨(q∧r) ≡ (p∨q)∧(p∨r) p∧(q∨r) ≡ (p∧q)∨(p∧r)

De Morgan

¬(p∧q) ≡ ¬p∨¬q

¬(p∨q) ≡ ¬p∧¬q

Negation ¬(¬p) ≡ p

Excluded Middle

p∨¬p ≡ true


p∧¬p ≡ false


p→q ≡ ¬p∨q


p→q ≡ ¬q→¬p


p↔q ≡ (p→q)∧(q→p)


p∨p ≡ p

p∧p ≡p

Simplification I

p ∧ true ≡ p

p ∨ true ≡ true

p ∧ false ≡ false

p ∨ false ≡ p

Simplification II

p∨(p∧q) ≡ p

p∧(p∨q) ≡ p


We assume that if $\phi \equiv \psi$, then $\phi \simeq \chi$ if and only if $\psi \simeq \chi$ (and similar for the right-hand side). Otherwise, we can do nothing meaningful with $\simeq$, and this rule of substitution is one of the cornerstones of propositional logic, so it seems reasonable to use it here.

For brevity, denote $\top$ for true and $\bot$ for false.

Using the rule for implication, we infer from $\bot \to \top \simeq \top \to \bot$ that: $$\neg \bot \lor \top \simeq \neg \top \lor \bot$$

If we can derive:

$$\neg\bot \equiv \top \\ \neg\top \equiv \bot$$ then it follows from idempotence that $\top \simeq \bot$.

To prove these identities, we can use excluded middle and contradiction.

  • $\begingroup$ How do I go about proving ¬⊥≡⊤ using excluded middle? Thanks! $\endgroup$ – Yekk Jan 25 '15 at 21:43
  • $\begingroup$ It goes as follows: $\neg \bot \equiv \neg(p \land \neg p) \equiv \ldots \equiv \top$. Can you see what rules to apply on the dots? $\endgroup$ – Lord_Farin Jan 25 '15 at 21:45
  • $\begingroup$ OH De Morgan and then Excluded middle! Thanks! $\endgroup$ – Yekk Jan 25 '15 at 21:52
  • $\begingroup$ You're welcome :). $\endgroup$ – Lord_Farin Jan 25 '15 at 21:53

As suggested, let’s start with


which follows immediately from the new rule. From Implication we get


You have a Simplification rule that you can usefully apply to the lefthand side of $(1)$ to reduce it to a single term. On the righthand side use Negation to rewrite it as $\neg\text{true}\lor\neg(\neg\text{false})$, apply De Morgan, and Simplification and Negation again; I’ll it to you to work out the details, but feel free to leave a question if you get completely stuck.


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.