関数などの定義の方法

Mizarは（潜在的には）イプシロン記号で関数を定義している。同じ方法で定義するとして、

1. 関数
2. 部分関数
3. スコーレム関数

定義形式は仮にだが、

function foo:X->Y := λx∈X.εy∈Y.P(x, y)

partial function foo:X->Y := λx∈X.εy∈Y.P(x, y)

Skolem function foo:X->Y := λx∈X.εy∈Y.P(x, y)

キーワード以外同じだが、正当化〈justification〉の方法が違う。

function foo:X->Y := λx∈X.εy∈Y.P(x, y)
 justification
   existence ∀x∈X.∃y∈Y. P(x, y)
   uniquencess ∀x∈X.∀y, y'∈Y. P(x, y)∧P(x, y')⊃(y = y')
 end

partial function foo:X->Y := λx∈X.εy∈Y.P(x, y)
 justification
   uniquencess ∀x∈X.∀y, y'∈Y. P(x, y)∧P(x, y')⊃(y = y')
 end

Skolem function foo:X->Y := λx∈X.εy∈Y.P(x, y)
 justification
   existence ∀x∈X.∃y∈Y. P(x, y)
 end

部分関数は、単葉性〈univalence | 一価性〉だけが要求される。スコーレム関数では存在だけが要求される。部分関数は、値があるとこでは一意性が必要だが、全域性は必要ない。スコーレム関数の場合は、全域だが値が確定しないので、各点ごとで値を選択する選択関数を意味する。スコーレム関数自体が確定した関数ではない。

上記のようにして定義したとき、

1. fooは、二項述語P(x, y)の関数である。
2. fooは、二項述語P(x, y)の部分関数である。
3. fooは、二項述語P(x, y)のスコーレム関数である。

のように言う。正当化部分の証明がないときは、定義は成立しない。