Investigation of Formulae in Predicate Calculus (3)

(nested quantifiers)

∀x[∀y( )]     ∀y[∀x( )]    ∀x[∃y( )]    ∀y[∃x( )]     ∃x[∀y( )]     ∃y[∀x( )]    ∃x[∃y( )]     ∃y[∃x( )]

¬∀x[∀y( )]   ∀x[¬∀y( )]   ∀x[∀y(¬ )]   ¬∀x[¬∀y( )]  ¬∀x[∀y(¬ )]   ∀x[¬∀y(¬ )]   ¬∀x[¬∀y(¬ )]
∀x[( ) ∧ ∀y( )]    ∀x[∀y( ) ∧ ( )]    ∀x{∀y[( ) ∧ ( )]}

∀x[( ) ∨ ∀y( )]    ∀x[∀y( ) ∨ ( )]    ∀x{∀y[( ) ∨ ( )]}

∀x[( ) ⇒ ∀y( )]    ∀x[∀y( ) ⇒ ( )]    ∀x{∀y[( ) ⇒ ( )]}

∀x[( ) ⇔ ∀y( )]    ∀x[∀y( ) ⇔ ( )]    ∀x{∀y[( ) ⇔ ( )]}

¬∀y[∀x( )]   ∀y[¬∀x( )]   ∀y[∀x(¬ )]     ¬∀y[¬∀x( )]  ¬∀y[∀x(¬ )]   ∀y[¬∀x(¬ )]   ¬∀y[¬∀x(¬ )]

∀y[( ) ∧ ∀x( )]    ∀y[∀x( ) ∧ ( )]    ∀y{∀x[( ) ∧ ( )]}

∀y[( ) ∨ ∀x( )]    ∀y[∀x( ) ∨ ( )]    ∀y{∀x[( ) ∨ ( )]}

∀y[( ) ⇒ ∀x( )]    ∀y[∀x( ) ⇒ ( )]    ∀y{∀x[( ) ⇒ ( )]}

∀y[( ) ⇔ ∀x( )]    ∀y[∀x( ) ⇔ ( )]    ∀y{∀x[( ) ⇔ ( )]}

¬∀x[∃y( )]   ∀x[¬∃y( )]   ∀x[∃y(¬ )]    ¬∀x[¬∃y( )]  ¬∀x[∃y(¬ )]   ∀x[¬∃y(¬ )]   ¬∀x[¬∃y(¬ )]

∀x[( ) ∧ ∃y( )]    ∀x[∃y( ) ∧ ( )]    ∀x{∃y[( ) ∧ ( )]}

∀x[( ) ∨ ∃y( )]    ∀x[∃y( ) ∨ ( )]    ∀x{∃y[( ) ∨ ( )]}

∀x[( ) ⇒ ∃y( )]    ∀x[∃y( ) ⇒ ( )]    ∀x{∃y[( ) ⇒ ( )]}

∀x[( ) ⇔ ∃y( )]    ∀x[∃y( ) ⇔ ( )]    ∀x{∃y[( ) ⇔ ( )]}

¬∀y[∃x( )]   ∀y[¬∃x( )]   ∀y[∃x(¬ )]   ¬∀y[¬∃x( )]  ¬∀y[∃x(¬ )]   ∀y[¬∃x(¬ )]   ¬∀y[¬∃x(¬ )]

∀y[( ) ∧ ∃x( )]    ∀y[∃x( ) ∧ ( )]    ∀y{∃x[( ) ∧ ( )]}

∀y[( ) ∨ ∃x( )]    ∀y[∃x( ) ∨ ( )]    ∀y{∃x[( ) ∨ ( )]}

∀y[( ) ⇒ ∃x( )]    ∀y[∃x( ) ⇒ ( )]    ∀y{∃x[( ) ⇒ ( )]}

∀y[( ) ⇔ ∃x( )]    ∀y[∃x( ) ⇔ ( )]    ∀y{∃x[( ) ⇔ ( )]}

¬∃x[∀y( )]   ∃x[¬∀y( )]   ∃x[∀y(¬ )]   ¬∃x[¬∀y( )]  ¬∃x[∀y(¬ )]   ∃x[¬∀y(¬ )]   ¬∃x[¬∀y(¬ )]

∃x[( ) ∧ ∀y( )]    ∃x[∀y( ) ∧ ( )]    ∃x{∀y[( ) ∧ ( )]}

∃x[( ) ∨ ∀y( )]    ∃x[∀y( ) ∨ ( )]    ∃x{∀y[( ) ∨ ( )]}

∃x[( ) ⇒ ∀y( )]    ∃x[∀y( ) ⇒ ( )]    ∃x{∀y[( ) ⇒ ( )]}

∃x[( ) ⇔ ∀y( )]    ∃x[∀y( ) ⇔ ( )]    ∃x{∀y[( ) ⇔ ( )]}

¬∃y[∀x( )]   ∃y[¬∀x( )]   ∃y[∀x(¬ )]   ¬∃y[¬∀x( )]  ¬∃y[∀x(¬ )]   ∃y[¬∀x(¬ )]   ¬∃y[¬∀x(¬ )]

∃y[( ) ∧ ∀x( )]    ∃y[∀x( ) ∧ ( )]    ∃y{∀x[( ) ∧ ( )]}

∃y[( ) ∨ ∀x( )]    ∃y[∀x( ) ∨ ( )]    ∃y{∀x[( ) ∨ ( )]}

∃y[( ) ⇒ ∀x( )]    ∃y[∀x( ) ⇒ ( )]    ∃y{∀x[( ) ⇒ ( )]}

∃y[( ) ⇔ ∀x( )]    ∃y[∀x( ) ⇔ ( )]    ∃y{∀x[( ) ⇔ ( )]}

¬∃x[∃y( )]   ∃x[¬∃y( )]   ∃x[∃y(¬ )]  ¬∃x[¬∃y( )]  ¬∃x[∃y(¬ )]   ∃x[¬∃y(¬ )]   ¬∃x[¬∃y(¬ )]

∃x[( ) ∧ ∃y( )]    ∃x[∃y( ) ∧ ( )]    ∃x{∃y[( ) ∧ ( )]}

∃x[( ) ∨ ∃y( )]    ∃x[∃y( ) ∨ ( )]    ∃x{∃y[( ) ∨ ( )]}

∃x[( ) ⇒ ∃y( )]    ∃x[∃y( ) ⇒ ( )]    ∃x{∃y[( ) ⇒ ( )]}

∃x[( ) ⇔ ∃y( )]    ∃x[∃y( ) ⇔ ( )]    ∃x{∃y[( ) ⇔ ( )]}

¬∃y[∃x( )]   ∃y[¬∃x( )]   ∃y[∃x(¬ )]   ¬∃y[¬∃x( )]  ¬∃y[∃x(¬ )]   ∃y[¬∃x(¬ )]   ¬∃y[¬∃x(¬ )]

∃y[( ) ∧ ∃x( )]    ∃y[∃x( ) ∧ ( )]    ∃y{∃x[( ) ∧ ( )]}

∃y[( ) ∨ ∃x( )]    ∃y[∃x( ) ∨ ( )]    ∃y{∃x[( ) ∨ ( )]}

∃y[( ) ⇒ ∃x( )]    ∃y[∃x( ) ⇒ ( )]    ∃y{∃x[( ) ⇒ ( )]}

∃y[( ) ⇔ ∃x( )]    ∃y[∃x( ) ⇔ ( )]    ∃y{∃x[( ) ⇔ ( )]}