[Tableaukalkül] Existenzquantor

Hi

Ich hätte mal eine allgemeine Frage zum Tableaukalkül mit PL1 (schon ein wenig her wo ich den gelernt hab):

Wenn ich in einem Ast die Prädikate

P(a)
 |
P(b)
 |
Exists x ~P(x)

Dann müsste ich für den Existenzquantor eine neue Skolem einführen - e.g. P(c) oder? D.h. Existenzquantor kann mir hier keinen Widerspruch liefern

Danke
LG

Perfekt - das beantwortet meine Frage zu 100% - danke