Hallo zusammen,
ich befasse mich gerade mit der Skolemisierung und hatte mich hinsichtlich einer Skolem-Funktion und einer Skolem-Konstante folgendes gefragt:
Eine Skolem-Funktion wird genau dann verwendet, wenn ein Allquantor vor einem Existenzquantor steht und eine Skolem-Konstante genau dann, wenn kein Allquantor vor einem Existenzquantor steht. Also:
Skolem-Funktion für y:
$$\forall x \exists y$$
Skolem-Konstante für y:
$$\exists y \forall x$$
In wie fern spielt hier der Scope eines Existenzquantors eine Rolle? Im folgenden Beispiel liegt der Existenzquantor meiner Meinung nach innerhalb des Scopes des Allquantors und ich hätte dementsprechend hier eine Skolem-Funktion verwendet. Ist das so richtig? Hier das Beispiel:
$$\forall n :(n \in \mathbb{N} \implies (\exists m \in \mathbb{N} \land m > n))$$
Vielen Dank im Voraus :)
