Skolem-Funktion / Skolem-Konstante: Scope eines Allquantors

Question

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 :)

Answer 1

Im Allgemeinen ist die Skolemform einer Aussage dann wohldefiniert, wenn sie in Pränexform vorliegt.

Deine Aussage in Pränexform ist:

\(\forall n \exists m : (n\in\mathbb{N}\implies(m\in\mathbb{N}\land m>n)).\)

Jetzt kann man die Skolemform quasi ablesen. Um deine Frage zu beantworten: Was du intuitiv als "Scope" eines Quantors beschreibst, wirkt auf mich genau wie die Quantoren, die in Pränexform später kommen. Somit würde ich behaupten, dass du richtig liegst, weil so gesehen die Skolemisierung für jeden Existenzquantoren genau die Allquantoren betrachtet, in deren Scopes er liegt.

Übrigens: Es gibt keinen fundamentalen Unterschied zwischen einer Skolemkonstante und einer Skolemfunktion. Steht ein Existenzquantor rechts von \(n\) vielen Allquantoren, so tauschst du die Variable durch ein n-stelliges Funktionssymbol aus. Steht ein Existenzquantor ganz links, so ist dein Existenzquantor im Scope von null vielen Allquantoren und du ersetzt deine Variable eben mit einem 0-stelligen Funktionssymbol (i.e. einer Konstante). Jacke wie Hose.