# Propositional logical equivalence in Lemmon style proof

I am doing a bit of propositional logic and I was wondering does Lemmon style of proofing allows writing logical equivalence of some propositions. There is an example of biconditional that you can express it using conjunction and conditional. Example:

P, (P ↔ Q) ⊢ Q

1  (1)P                 Assumption
2  (2)P ↔ Q             Assumption
2  (3)(P → Q) & (Q → P) 2 Df. ↔


Is this possible with other logical expressions? If yes, what do you write on a right side where you write from where did you get this proposition and what rule did you apply. Possible example:

P, (P → Q) ⊢ Q

1  (1)P                 Assumption
2  (2)P → Q             Assumption
2  (3)¬P V Q            2 (What to write here)
3  (4)¬(P & ¬Q)         3 (What to write here)

• Do you have a link or reference to the particular system you are working with? – Bram28 Aug 14 '17 at 21:47
• I am reading E.J. Lemmons book Beginning logic – Slit Aug 14 '17 at 21:54

Your example seems to indicate that the $\leftrightarrow$ is defined as a conjunction of two conditionals. That is, $\varphi \leftrightarrow \psi$ is seen as shorthand for $(\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$

Some formal proof systems do indeed do this, and some will even consider the rewriting of that definition/shorthand as a step in the proof, which is what your example proof seems to be doing.

However, this is not the same as using any kind of logical equivalence to rewrite statements. If you want to rewrite statements using logical equivalences, then the formal proof system needs to have the corresponding rules defined for that. If the system has not defined those equivalences as rules, then you are not allowed to do that within the system

OK, but maybe the proof system, has some other definitions/shorthands, like the one you propose for the $\rightarrow$, or for the $\lor$? Well, that's possible, but again that all depends on how your proof system has defined its formal syntax, and its rules.

• I am reading E.J. Lemmons book Beginning logic and I didn't find rules for my logical equivalences. I tought of them like it is the same if you write (P v Q) or you can write (Q v P). As long as truth tables are the same... why not. – Slit Aug 14 '17 at 21:51
• @Slit Yeah, you'd think .. but unfortunately formal proofs don't work that way. The game there is: follow the rules! If there's no rule for it, you can't do it, sorry! – Bram28 Aug 14 '17 at 21:56
• Pity... Well maybe in some other system... – Slit Aug 14 '17 at 21:59
• @Slit Yes, there are formal proof systems that use all kinds of equivalence rules as inference rules. Symbolic Logic by Copi comes to mind. Also Introduction to Logic by Copi and Cohen. So again, not just any logical equivalence can be used, but at least they define some of the important ones, like Commutation, Association, Double Negation, Distribution, DeMorgan, Implication, and Equivalence – Bram28 Aug 14 '17 at 22:00
• I will look up. I hope it is similar to Lemmon – Slit Aug 14 '17 at 22:06