polyadic algebra
A polyadic algebra is a quadruple (B,V,∃,S), where (B,V,∃) is a quantifier algebra, and S is a function from the set of functions on V to the set of endomorphisms on the Boolean algebra
B, in other words
S:VV→End(B) |
such that
-
1.
S(1V)=1B,
-
2.
S(f∘g)=S(f)∘S(g),
-
3.
S(f)∘∃(I)=S(g)∘∃(I) if f(V-I)=g(V-I),
-
4.
∃(I)∘S(f)=S(f)∘∃(f-1(I)) if f is one-to-one when restricted to f-1(I).
Explanation of notations: 1V,1B are identity functions on V,B respectively; f,g are functions on V, and I is a subset of V. The circle ∘ represents functional compositions.
The degree and local finiteness of a polyadic algebra are defined as the degree and local finiteness of the underlying quantifier algebra.
Heuristically, the function S can be thought of as changes to propositional functions due to a “substitution” of variables (elements of V). Let us see some examples. Let V={x0,x1,…} be a countably indexed set of variables. For any propositional function φ, define S(f)(φ) to be the propositional function φ1 obtained by replacing each variable x that occurs in it by f(x). Below are two examples illustrating how S(f) changes propositional functions:
-
•
Let f:V→V be the function given by f(x0)=f(x1)=x0 and f(xi)=xi+1 for all i>1. If φ is the propositional function x20-x1+x2/x3, then S(f)(φ) is the propositional function x20-x0+x3/x4.
-
•
Let f:V→V be the function given by f(x0)=x2, and f(xi)=xi for all i≠0. Then the propositional function “∃x0,x1,x2(x0≠x1∧x1≠x2∧x2≠x0)” becomes “∃x2,x1,x2(x2≠x1∧x1≠x2∧x2≠x2)” under S(f).
It is not hard to see from the examples above that S(f) respects Boolean operations ∧ and ′, which is why we want to make S(f) an endomorphism on B. Furthermore, the four conditions above can be interpreted as
-
1.
if there are no substitutions of variables, then there should be no corresponding changes to the propositional functions
-
2.
applying substitutions f∘g of varaibles in a propositional function φ should have the same effect as applying substitutions g of variables in φ, followed by substitutions f of variables in S(g)(φ)
-
3.
a substitution f of variables should have no effect to a propositional function beginning with ∃ if every variable bound by ∃ is fixed by f. For example, if we replace f in the second example above by f(x3)=x2 and f(xi)=xi otherwise, then
``∃x0,x1,x2(x0≠x1∧x1≠x2∧x2≠x0)" is unchanged by S(f), since x0,x1,x2 are all fixed by f.
-
4.
Let φ=∃Iψ(I,J) be a propositional function, where I,J are sets of variables with I bound by ∃ and J free. If no two variables I get mapped to the same variable, and no free variable
(in J) becomes bound (in f(I)) under the substitution, then ∃Iψ(f(I),f(J)) and ∃f(I)ψ(f(I),f(J)) are semantically the same, which is exactly the statement in the condition.
Remarks.
-
•
Paul Halmos first introduced the notion of polyadic algebras. In his Algebraic Logic, a compilation of articles on the subject, he called a function on the set V of variables a transformation
, and the triple (B,V,S) satisfying the first two conditions above a transformation algebra. Therefore, a polyadic algebra is a quadruple (B,V,∃,S) where (B,V,∃) is a quantifier algebra and (B,V,S) is a transformation algebra, such that conditions 3 and 4 above are satisfied.
-
•
The notion of polyadic algebras generalizes the notion of monadic algebras. Indeed, a monadic algebra is a polyadic algebra where V is a singleton.
-
•
Just as a Lindenbaum-Tarski algebra is the algebraic counterpart of a classical propositional logic
, a polyadic algebra is the algebraic counterpart of a classical first order logic without equality. A variant of the polyadic algebra is what is known as a cylindric algebra, which algebratizes a classical first order logic with equality.
References
- 1 P. Halmos, Algebraic Logic, Chelsea Publishing Co. New York (1962).
-
2
B. Plotkin, Universal Algebra
, Algebraic Logic, and Databases, Kluwer Academic Publishers (1994).
Title | polyadic algebra |
---|---|
Canonical name | PolyadicAlgebra |
Date of creation | 2013-03-22 17:50:39 |
Last modified on | 2013-03-22 17:50:39 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 13 |
Author | CWoo (3771) |
Entry type | Definition |
Classification | msc 03G15 |
Related topic | QuantifierAlgebra |
Related topic | MonadicAlgebra |
Related topic | CylindricAlgebra |
Defines | transformation algebra |