<На страницу назад | На страницу вперед>
A.5.2.2 Аксиомы для термов инфонов
При наличии понятия отношения первого порядка можно привести аксиомы, выражающие
то, что требуется для того, чтобы терм инфона обозначал правомерный инфон (в
отличие от неопределенного (null) объекта).
Базовый терм инфона обозначает инфон тогда и только тогда,
когда он включает терм, обозначающий n-местное отношение первого порядка, после
которого следует n термов, обозначающих индивиды, и один терм, обозначающий
полярность.
(A basic infon term denotes an infon if and only if it consists of a term denoting
an n-place first-order relation followed by n terms denoting individuals and
a term denoting a polarity).
(forall (?rel var1 . . . varn ?pol)
(<=> (infon (?r var1 . . . varn ?pol))
(and (FO-relation ?r)
(individual var1)
. . .
(individual varn)
(polarity ?p))))
Конъюнктивный (дизъюнктивный) терм инфона обозначает инфон
тогда и только тогда, когда каждый конъюнкт (дизъюнкт) обозначает инфон.
(A conjunctive (disjunctive) infon term denotes an infon if and only if each
conjunt (disjunct) denotes an infon).
(forall (?inf1 ?inf2)
(<=> (and (infon (and ?inf1 ?inf2)))
(and (infon ?inf1) (infon ?inf2))))(forall (?inf1 ?inf2)
(<=> (and (infon (or ?inf1 ?inf2)))
(and (infon ?inf1) (infon ?inf2))))
Аналогичные аксиомы для связанных кванторами инфонов должны быть выражены в виде схемы. Пусть Q представляет любой квантор, var - любую переменную, infterm - любой терм инфона. Если var входит свободным как первый терм в любой атомарный инфон в infterm, то
(<=> (infon (Q var infterm))
(Q (var : (FO-relation var)) (infon infterm)))).
Подобным образом, если var не входит свободным как первый терм в какой-либо терм атомарного инфона в infterm (т.е. входят связанным или входит свободным где-то еще как первый терм в терме атомарного инфона в infterm, или вообще не входит в infterm), то
(<=> (infon (Q var infterm))
(Q (var : (individual var)) (infon infterm)))).