Erbranovi strukturi

ЕРБРАНОВИ СТРУКТУРИ

Множеството на всички затворени термове ще означаваме с H и ще го наричаме Ербранов универсум - по името на логика Жак Ербран (Jacques Herbrand). Очевидно H№Ж точно тогава, когато W₀№Ж; затова в случаите, когато използваме Ербрановия универсум, обикновено ще изискваме да съществува поне един нулместен функционален символ. На всеки функционален символ w от W ние ще поставим в съответствие една операция в H, която ще наричаме Ербранова интерпретация на w и ще означаваме с w^H. А именно, ако wОW₀, то полагаме w^H да бъде нулместната операция w в H, а ако wОW_n, където n>0, то означаваме с w^H n-местната операция в H, преобразуваща произволна n-орка (t₁,...,t_n) от затворени термове в затворения терм w(t₁,...,t_n).¹ Ербранова структура ще наричаме всяка структура (C,I), удовлетворяваща условията, че C е Ербрановият универсум и за всеки функционален символ w от W имаме равенството I(w)=w^H (разбира се, такива структури съществуват при H№Ж, т.е при W₀№Ж).

Основна лема за Ербрановите структури. Нека W₀№Ж и нека S е произволна Ербранова структура. Тогава t^S=t за всеки затворен терм t.

Доказателство. Ще използваме индукция, съобразена с индуктивната дефиниция на понятието затворен терм. Нека I е интерпретиращото съответствие на S. Ако wОW₀, то w^S=I(w)=w^H=w. Да предположим сега, че wОW_n, където n>0, и t₁, ..., t_n са затворени термове, за които имаме равенствата t₁^S=t₁, ..., t_n^S=t_n. Тогава

w(t₁,...,t_n)^S=I(w)(t₁^S,...,t_n^S)=w^H(t₁,...,t_n)=w(t₁,...,t_n).

Следствие. При предположенията на горната лема всеки два различни затворени терма (ако съществуват такива) имат различни стойности в S.

Забележка. Уговорката, добавена в скоби в горното следствие, е по повод на това, че би могло да се случи да имаме равенството W=W₀ и същевременно множеството W₀ да се състои точно от един елемент - очевидно в такъв случай споменатият единствен елемент на W₀ би бил и единственият затворен терм.

Ще направим аналогични разглеждания и за случая на конфигурация. Множеството на всички термове ще наричаме разширен Ербранов универсум и ще го означаваме с Hў (това множество със сигурност не е празно). На всеки функционален символ w съпоставяме негова разширена Ербранова интерпретация w^Hў, аналогично на направеното преди малко съпоставяне на Ербранова интерпретация, но с тази разлика, че вместо за затворени термове сега става дума за произволни термове. Ербранова конфигурация ще наричаме всяка конфигурация от вида (S,v), където носител на S е разширеният Ербранов универсум, интерпретиращото съответствие на S съпоставя на всеки функционален символ от W неговата разширена Ербранова интерпретация, a v e тъждественото изображение на множеството X в себе си.

Основна лема за Ербрановите конфигурации. Нека (S,v) е произволна Ербранова конфигурация. Тогава t^S,v=t за всеки терм t.

Доказателство. Ще използваме индукция, съобразена с индуктивната дефиниция на понятието терм. Нека I е интерпретиращото съответствие на S. Ако wОW₀, то w^S,v=I(w)=w^Hў=w. Ако xОX, то x^S,v=v(x)=x. Да предположим сега, че wОW_n, където n>0, и t₁, ..., t_n са термове, за които имаме равенствата t₁^S,v=t₁, ..., t_n^S,v=t_n. Тогава

w(t₁,...,t_n)^S,v=I(w)(t₁^S,v,...,t_n^S,v)=w^Hў(t₁,...,t_n)=w(t₁,...,t_n).

Следствие. При предположението на горната лема всеки два различни терма имат различни стойности в (S,v).

Бележка

¹ Обръщаме внимание на твърде различния смисъл, който има означението (t₁,...,t_n) при първото и при второто си появяване в току-що написаното изречение. Първия път имаме обичайното математическо означение на n-ка от обекти (тези обекти са n-те думи t₁, ..., t_n), а втория път имаме означение на една дума, получена чрез конкатенация от думите t₁, ..., t_n и от буквите лява скоба, дясна скоба и запетая (при n=1 запетая фактически не участва). По-прецизно би било да напишем, че w^H преобразува (t₁,...,t_n) в w"("t₁","...","t_n")".

Последно изменение: 9.01.2001 г.

Previous Next Contents