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)
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.