<На страницу назад | На страницу вперед>

А.3.1.2 Неопределенный объект
Две приведенные ниже схемы аксиом характеризуют неопределенный объект и его связи с функциями и отношениями.

Атомарное предложение, включающее терм, обозначающий неопределенный объект, должно быть ложным.
(An atomic sentence that contains a term denoting the null object must be false):

(forall (?r ?var₁ . . . ?var_n : (relation ?r) (or (= ?var₁ null) . . . (= ?var_n null)))
(not (?r ?var₁ . . . ?var_n)))

Терм функции, включающий терм, обозначающий неопределенный объект, сам должен обозначать неопределенный объект.
(A function term that includes a term denoting the null object must itself denote the null object):

(forall (?f ?var₁ . . . ?var_n : (function ?f) (or (= ?var₁ null) . . . (= ?var_n null)))
(= (?f ?s1 . . . ?s_n) null))

<На страницу назад | На страницу вперед>