Цилиндрическая алгебра

редактировать

Понятие цилиндрической алгебры, изобретенное Альфредом Тарским, естественно возникает в алгебраизация логики первого порядка с равенством. Это сравнимо с ролью булевых алгебр для логики высказываний. В самом деле, цилиндрические алгебры - это булевы алгебры, снабженные дополнительными операциями цилиндрификации, которые моделируют квантификацию и равенство. Они отличаются от полиадических алгебр тем, что последние не моделируют равенство.

Содержание
  • 1 Определение цилиндрической алгебры
  • 2 Цилиндрические алгебры множеств
  • 3 Обобщения
  • 4 Связь с монадической булевой алгеброй
  • 5 См. Также
  • 6 Примечания
  • 7 Ссылки
  • 8 Дополнительная литература
  • 9 Внешние ссылки
Определение цилиндрической алгебры

A цилиндрической алгебры размерности α {\ displaystyle \ alpha}\ альфа (где α {\ displaystyle \ alpha}\ альфа - любое порядковое число ) - алгебраическая структура (A, +, ⋅, -, 0, 1, c κ, d κ λ) κ, λ < α {\displaystyle (A,+,\cdot,-,0,1,c_{\kappa },d_{\kappa \lambda })_{\kappa,\lambda <\alpha }}(A, +, \ cdot, -, 0,1, c _ {\ kappa}, d_ { {\ kappa \ lambda}}) _ {{\ kappa, \ lambda <\ alpha}} такие, что (A, +, ⋅, -, 0, 1) {\ displaystyle (A, +, \ cdot, -, 0,1)}(A, +, \ cdot, -, 0,1) является булевой алгеброй, c κ {\ displaystyle c _ {\ kappa}}c _ {\ kappa} унарным оператором в A {\ displaystyle A}A для каждого κ {\ displaystyle \ kappa}\ каппа (называемого цилиндрификацией) и d κ λ {\ displaystyle d _ {\ kappa \ lambda}}d _ {{\ каппа \ лямбда}} выдающимся элемент A {\ displaystyle A}A для каждого κ {\ displaystyle \ kappa}\ каппа и λ {\ display tyle \ lambda}\ lambda (называется диагональю), так что выполняется следующее:

(C1) c κ 0 = 0 {\ displaystyle c _ {\ kappa} 0 = 0}c _ {\ kappa} 0 = 0
(C2) x ≤ c κ x {\ displaystyle x \ leq c _ {\ kappa} x}x \ leq c _ {\ kappa} x
(C3) c κ (x ⋅ c κ y) = c κ x ⋅ c κ Y {\ Displaystyle c _ {\ kappa} (x \ cdot c _ {\ kappa} y) = c _ {\ kappa} x \ cdot c _ {\ kappa} y}c _ {\ kappa } (х \ cdot c _ {\ kappa} y) = c _ {\ kappa} x \ cdot c _ {\ kappa} y
(C4) c κ c λ x знак равно c λ c κ x {\ displaystyle c _ {\ kappa} c _ {\ lambda} x = c _ {\ lambda} c _ {\ kappa} x}c _ {\ kappa} c _ {\ lambda} x = c _ {\ lambda} c _ {\ kap pa} x
(C5) d κ κ = 1 {\ displaystyle d _ {\ каппа \ каппа} = 1}d _ {{\ каппа \ каппа}} = 1
(C6) Если κ ∉ {λ, μ} {\ displaystyle \ kappa \ notin \ {\ lambda, \ mu \}}\ kappa \ notin \ {\ lambda, \ mu \} , тогда d λ μ знак равно c κ (d λ κ ⋅ d κ μ) {\ displaystyle d _ {\ lambda \ mu} = c _ {\ kappa} (d _ {\ lambda \ kappa} \ cdot d _ {\ kappa \ mu})}d _ {{\ lambda \ mu}} = c _ {\ kappa} (d _ {{\ лямбда \ каппа}} \ cdot d _ {{\ каппа \ mu}})
(C7) Если κ ≠ λ {\ displaystyle \ kappa \ neq \ lambda}\ kappa \ neq \ lambda , то c κ (d κ λ ⋅ x) ⋅ c κ (d κ λ ⋅ - Икс) знак равно 0 {\ displaystyle c _ {\ kappa} (d _ {\ kappa \ lambda} \ cdot x) \ cdot c _ {\ kappa} (d _ {\ kappa \ lambda} \ cdot -x) = 0}c _ {\ kappa} (d_ { {\ kappa \ lambda}} \ cdot x) \ cdot c _ {\ kappa} (d _ {{\ kappa \ lambda}} \ cdot -x) = 0

Предполагая представление логики первого порядка без функции ионные символы, оператор c κ x {\ displaystyle c _ {\ kappa} x}c _ {\ kappa} x модели количественная оценка существования по переменной κ {\ displaystyle \ kappa }\ каппа в формуле x {\ displaystyle x}Икс , а оператор d κ λ {\ displaystyle d _ {\ kappa \ lambda}}d _ {{\ каппа \ лямбда}} моделирует равенство переменных κ {\ displaystyle \ kappa}\ каппа и λ {\ displaystyle \ lambda}\ lambda . Отныне, переформулированные с использованием стандартных логических обозначений, аксиомы читаются как

(C1) ∃ κ. е а л с е ⟺ е а л с е {\ Displaystyle \ существует \ каппа. {\ mathit {false}} \ iff {\ mathit {false}}}{\ displaystyle \ exists \ kappa. {\ mathit {false}} \ iff {\ mathit {false}}}
(C2) х ⟹ ∃ κ. Икс {\ Displaystyle х \ подразумевает \ существует \ каппа. х}{\ displaystyle x \ implies \ exists \ kappa.x}
(C3) ∃ κ. (Икс ∧ ∃ κ. Y) ⟺ (∃ κ. Икс) ∧ (∃ κ. Y) {\ Displaystyle \ существует \ каппа. (х \ клин \ существует \ каппа. y) \ iff (\ существует \ каппа. x) \ клин (\ существует \ kappa.y)}{\ Displaystyle \ существует \ каппа. (х \ клин \ существует \ каппа. y) \ iff (\ существует \ каппа. x) \ wedge (\ exists \ kappa.y)}
(C4) ∃ κ ∃ λ. х ⟺ ∃ λ ∃ κ. Икс {\ Displaystyle \ существует \ каппа \ существует \ лямбда. х \ если \ существует \ лямбда \ существует \ каппа. x}{\ displaystyle \ exists \ kappa \ exists \ лямбда. х \ если \ существует \ лямбда \ существует \ каппа. х}
(C5) κ = κ ⟺ истина {\ Displaystyle \ каппа = \ каппа \ iff {\ mathit {true}}}{\ displaystyle \ kappa = \ kappa \ iff {\ mathit {true}}}
(C6) Если κ {\ displaystyle \ kappa}\ каппа - это переменная, отличная от обоих λ {\ displaystyle \ lambda}\ lambda и μ {\ displaystyle \ mu}\ mu , затем λ = μ ⟺ ∃ κ. (λ = κ ∧ κ = μ) {\ displaystyle \ lambda = \ mu \ iff \ exists \ kappa. (\ lambda = \ kappa \ wedge \ kappa = \ mu)}{\ displaystyle \ lambda = \ mu \ iff \ exists \ kappa. (\ lambda = \ kappa \ wedge \ kappa = \ mu)}
(C7) Если κ {\ displaystyle \ kappa}\ каппа и λ {\ displaystyle \ lambda}\ lambda - разные переменные, тогда ∃ κ. (κ = λ ∧ x) ∧ ∃ κ. (κ знак равно λ ∧ ¬ Икс) ⟺ ложь {\ Displaystyle \ существует \ каппа. (\ каппа = \ лямбда \ клин х) \ клин \ существует \ каппа. (\ каппа = \ лямбда \ клин \ нег х) \ iff { \ mathit {false}}}{\ displaystyle \ существует \ каппа. (\ каппа = \ лямбда \ клин х) \ клин \ существует \ каппа. (\ каппа = \ лямбда \ клин \ отр х) \ iff {\ mathit {false}}}
Цилиндрическая алгебра множеств

A цилиндрическая алгебра множеств размерности α {\ displaystyle \ alpha}\ альфа представляет собой алгебраическую структуру (A, ∪, ∩, -, ∅, X α, c κ, d κ λ) κ, λ < α {\displaystyle (A,\cup,\cap,-,\emptyset,X^{\alpha },c_{\kappa },d_{\kappa \lambda })_{\kappa,\lambda <\alpha }}{\ displaystyle (A, \ cup, \ cap, -, \ emptyset, X ^ {\ alpha}, c _ {\ kappa}, d _ {\ каппа \ лямбда}) _ {\ каппа, \ лямбда <\ альфа}} такие, что ⟨X α, A⟩ {\ displaystyle \ langle X ^ {\ alpha}, A \ rangle }{\ displaystyle \ langle X ^ {\ alpha}, A \ rangle} - поле наборов, c κ S {\ displaystyle c _ {\ kappa} S}{\ displaystyle c _ {\ kappa} S} задается как {y ∈ Икс α ∣ ∃ Икс ∈ S ∀ β ≠ κ Y (β) знак равно Икс (β)} {\ Displaystyle \ {у \ в X ^ {\ альфа} \ середина \ существует х \ в S \ \ forall \ beta \ neq \ kappa \ y (\ beta) = x (\ beta) \}}{\ displaystyle \ {y \ in X ^ {\ alpha} \ mid \ exists x \ in S \ forall \ beta \ neq \ каппа \ y (\ beta) = x (\ beta) \}} , и задано d κ λ {\ displaystyle d _ {\ kappa \ lambda}}d _ {{\ каппа \ лямбда}} по {x ∈ X α ∣ x (κ) = x (λ)} {\ displaystyle \ {x \ in X ^ {\ alpha} \ mid x (\ kappa) = x (\ lambda) \}}{\ displaystyle \ {x \ in X ^ {\ alpha} \ mid x (\ kappa) = x (\ lambda) \}} . Это обязательно подтверждает аксиомы C1 – C7 цилиндрической алгебры с ∪ {\ displaystyle \ cup}\ чашка вместо + {\ displaystyle +}+ , ∩ {\ displaystyle \ cap}\ cap вместо ⋅ {\ displaystyle \ cdot}\ cdot , установить дополнение для дополнения, пусто установить как 0, X α {\ displaystyle X ^ {\ alpha }}{\ displaystyle X ^ {\ alpha}} в качестве единицы измерения и ⊆ {\ displaystyle \ substeq}\ substeq вместо ≤ {\ displaystyle \ leq}\ leq . Множество X называется базой.

Не всякая цилиндрическая алгебра имеет представление в виде цилиндрической алгебры множеств. Легче связать семантику логики предикатов первого порядка с цилиндрической алгеброй множеств. (Подробнее см. Раздел «Дополнительная литература».)

Обобщения

Цилиндрические алгебры были обобщены на случай многосортной логики (Caleiro and Gonçalves 2006), что позволяет лучше моделировать двойственность между формулами и членами первого порядка.

Отношение к монадической булевой алгебре

Когда α = 1 {\ displaystyle \ alpha = 1}\ alpha = 1 и κ, λ {\ displaystyle \ kappa, \ lambda}{\ displaystyle \ kappa, \ lambda} ограничены значением 0, тогда c κ {\ displaystyle c _ {\ kappa}}c _ {\ kappa} становится ∃ {\ displaystyle \ exists}\ существует диагонали можно опустить, и следующая теорема цилиндрической алгебры (Пинтер, 1973):

c κ (x + y) = c κ x + c κ y {\ displaystyle c _ {\ kappa } (x + y) = c _ {\ kappa} x + c _ {\ kappa} y}{\ displaystyle c _ {\ kappa} (x + y) = c_ { \ каппа} х + с _ {\ каппа} y}

превращается в аксиому

∃ (x + y) = ∃ x + ∃ y {\ displaystyle \ exists (x + y) = \ exists x + \ exists y}{\ displaystyle \ exists (x + y) = \ exists x + \ exists y}

из монадической булевой алгебры. Аксиома (C4) выпадает. Таким образом, монадическую булеву алгебру можно рассматривать как ограничение цилиндрической алгебры на случай одной переменной.

См. Также
Примечания
Литература
Дополнительная литература
Внешние ссылки
Последняя правка сделана 2021-05-16 12:51:53
Содержание доступно по лицензии CC BY-SA 3.0 (если не указано иное).
Обратная связь: support@alphapedia.ru
Соглашение
О проекте