Want to show $ ¬∃x (∀ z Q_x,_z →Q_c,_y) ⊢ ∀x∀zQ_t,_z $
and Q is binary, z does not occur in t
I did just basic one..
ETS : ⊢$ ∀x ¬(∀ z Q_x,_z →Q_c,_y) → ∀x∀zQ_t,_z $
ETS : ⊢$ ∀x ( ¬(∀ z Q_x,_z →Q_c,_y) → ∀zQ_t,_z )$
What can I further do..? Maybe I can apply Genralization or Specification. Because z odes not occur in t
I am sorry for a too basic Question.