Ja, unbedingt, sonst ist ja die Formel nicht mehr logisch äquivalent! Oder alternativ, du darfst das negationszeichen dass du in der zweiten Zeile einführst nur direkt hinter das „\forall X“ packen.
Was du im prinzip machst ist:
\neg \exists X\forall Y\exists Z\exists W…
= \forall X \neg\forall Y\exists Z\exists W…
= \forall X\exists Y\neg\exists Z\exists W…
= \forall X\existsY\forall Z\neg\exists W…
Generelle Frage: kann es sein, dass es manchmal gar nicht notwendig ist zu skolemiesieren? Wie hier für Aufgabe 10.2…
Edit: Ach! mir fällt gerade auf das ist ein illegaler Move von Zeile 1 auf Zeile 2. Sooorrrryyyy
Gut, das erklärt einiges <_< Danke! Dann hier also noch mal die korrekte Umformung für alle:
Hmm, deinen wechsel zwischen T und F und negationen finde ich extrem verwirrend. Es ist nicht falsch was da passiert, aber mir ist nicht ganz klar, warum du das so augenscheinlich kompliziert machst…
ist das der versuch, das absolut rigoros und schritt-für-schritt nach den regeln für den CNF-algorithmus zu machen? Ich sollte in dem Fall nämlich deutlich darauf hinweisen, dass das so durchexorziert extrem zeitaufwendig aussieht und ihr euch vermutlich nicht unbedingt einen Gefallen damit tut wenn ihr so vorgeht.
…außer natürlich es geht nur darum den algorithmus zu verstehen, dann befürworte ich das absolut 
Ja genau, habe versucht die Schritte nachzuvollziehen und zu verstehen, was der Algorithmus da eigentlich tut. In der Klausur würde ich das natürlich in einem Schritt machen 
Ah, sehr gut, dann bin ich jetzt auch weniger von der Frage an sich verwirrt 