See Henson Graves. A Practical Doctrine for Mathematical Applications. 2.1.1. Water
"Формула воды" Один из подходов - это предикат.
Вар-1. В этой теории у нас один предметный сорт - Atom.
H2O_(x y z) ≝ Oxygen(x)∧Hydrogen(y)∧Hydrogen(z)∧y≠z∧ch_bonded(x y)∧ch_bonded(x z).
АЗ надо знать куда подставлять Oxy - иначе получишь False!!!
Либо добавляется инструкция: 3 нечто есть H2O если они в каком-то порядке удовлетворяют Вар-1. Конечно это можно записать перестановками:
H2O(x y z) ≝ H2O_(x y z)∨H2O_(x z y)...
По простому возникает многосортица:
Вар-2. В этой теории у нас столько предметных сортов сколько атомов. И теперь ch_bonded не просто первичный предикат теории, но ещё и применим к любым сортам, т.е. спец предикат!
Sorts Oxygen Hydrogen...
Declaration H2O Oxygen Hydrogen Hydrogen. --predicate.
Definition H2O(x y z) (y≠z∧ch_bonded(x y)∧ch_bonded(x z)).
We need axioms to proof TH_1: There is no other atom ch_bonded with H2O-ed.
Theorem TH_1 H2O(x y z) ∧ diff(u x y z) → ¬(ch_bonded(u x)∨ch_bonded(u y)∨ch_bonded(u z))).
Free vars subsume ∀.
!!!Из некоторых хим аксиом можно доказать что не существует других атомов связанных с этими 3-мя.
Замечание: Любопытна эта потеря порядка аргументов при уходе от многосортности: в Вар-2 синтаксически ясно что имея три атома надо Oxy пихать на первое место. В Вар-1 это ни откуда не следует!
Про хим связь см. в Википедии.