For a logical Formula there exists infinitely many equivalent forms, by arbitrary transformations.
Cumulative Law: Variables can be exchanged for Conjunctions and Disjunctions.
F ∧ G ≡ G ∧ F F ∨ G ≡ G ∨ F
F → G ≡ ¬F ∨ G F ↔ G ≡ (F → G) ∧ (G → F)
The Negation in front of expressions can be put inside of braces, i.e. directly in front of the Variables.
Not F and G equals not F or not G. Also vice versa not F or G equals not F and not G. So by applying this
De Morgan law one switches between Conjunction and Disjunction or vice versa and one changes the Negation and the Position of the Negation.
¬(F ∧ G) ≡ ¬F ∨ ¬G ¬(F ∨ G) ≡ ¬F ∧ ¬G
double Negation inverts itself.
¬¬F ≡ F
A Conjunction with a Truth value True (t) results into the original value of the Variable. On the other hand a Disjunction with a Truth value True is always True. A conjunction with a Truth value False (f) will be False and a Disjunction with a Truth value False will be the original Value F. F and not F always computes to False, while F or not F computes to True.
F ∧ t ≡ F F ∨ t ≡ t F ∧ f ≡ f F ∨ f ≡ F F ∧ ¬F ≡ f F ∨ ¬F ≡ t
Distributive Law: In Disjunction or Conjunction one can put the Variables into braces, where F is applied to both Variables inside th braces.
F ∨ (G ∧ H) ≡ (F ∨ G) ∧ (F ∨ H) F ∧ (G ∨ H) ≡ (F ∧ G) ∨ (F ∧ H)
Also for Quantifiers there are certain equivalence that need to be considered. For example negations in front of quantifiers are often required to be put inside the bound formula, i.e. the formula that is bound by the Quantifier. So not for all X is F is the same as there exists an X for that holds not F. On the other hand there exists a Variable X that holds F equals to for all X it holds not F.
¬(∀X) F ≡ (∃X) ¬F ¬(∃X) F ≡ (∀X) ¬F
If one has the same Quantifiers over several Variables one can exchange their positions. This holds for the Essential as well as for the Universal Quantification.
(∀X)(∀Y)F ≡ (∀Y)(∀X)F (∃X)(∃Y)F ≡ (∃Y)(∃X)F
Quantifiers before Formulas in braces can be put into the braces.
(∀X)(F ∧ G) ≡ (∀X)F ∧ (∀X)G (∃X)(F ∨ G) ≡ (∃X)F ∨ (∃X)G