.Open Three or More Infix operators The basis is ALGEBRA::=Net{ Set:Sets, ... }. to this a number of binary and unary operators are added and certain axioms assumed. These generate a rich set of results. Tarski turns up in most specialized systems. .Open High School Identities .Source Burris & Lee 93, Stanley Burris and Simon Lee, "Tarski's High School Identities", American Math Monthly V100n3(Mar 93) pp231-236 HSI_bar::=Net{ abstracted from the high school algebra of integers wthout powers. $ALGEBRA. +::infix(Set). *::infix(Set). (STANDARD)|- (*) higher_priority_than (+). 1::Set. For x,y,z:Set. |- (HS1): x+y=y+x. |- (HS2): x+(y+z)=(x+y)+z. |- (HS3): x*1=x. |- (HS4): x*y=y*x. |- (HS5): x*(y*z)=(x*y)*z. |- (HS6): x*(y+z)=(x*y)+(x*z). }=::HSI_bar. HSI::=Net{ abstracted from the high school algebra of integers with powers. |- (basis): HSI_bar. (^) ::infix(A). |- (priority): (^) higher_priority_then (*). |- (HS7): 1^x = 1, |- (HS8): x^1 = x, |- (HS9): x^(y+z) = (x^y) * (x^z), |- (HS10): (x*y)^z = (x^z) * (y^z), |- (HS11): (x^y)^z = x^(y*z). .Hole }=::HSI. ()|- (Nat, +, *,^,1) in$ $HSI_bar. ()|- For many H:$ $HSI (H<>(Nat, +, *,^, 1)). Suppose that NAT is the system of logic that describes the natuural numbers: Nat=$ $NAT. ()|- theorems(NAT)<<=theorems(HSI). Consider{ .Source Wilkie 80, "On exponentiation - a solution to Tarski's high school algebra problem", preprint, Oxford University, 1980. W(x,y) ::=( ((1+x)^y+(1+x+x^2)^y)^x*((1+x^3)^x+(1+x^2+x^4)^x)^y) = ((1+x)^x +(1+x+x^2)^x)^y * ((1+x^3)^y + (1+x^2+x^4)^y)^x). if NAT then W(x,y). Some HSI and not W. } ()|- not HSI_bar in decidable_algebras. Because there are no nice normal forms for HSI_bar. . Constructions of HSI modified finite quotients of Nat -> (tail+loop) Heyting algebra(H, ....,0,1) without 0. Add (1st) to distributive lattice, semilattices, boolean rings,... 44 3-element HSI_algebras .Hole . Polynomials For n:Nat0, c:set^(0..n), x:set, poly(c)(x) ::set= +( c*(x^Id(0..n))). .Close High School Identities .Roadworks_Ahead .Open Modules .Hole .Close Modules .Open K-Algebras .Hole .Close K-Algebras .Open Vector Spaces VECTOR::=following .Net Scalar::$Field=given. Vector:: Sets=goal. |- (VS0): $GROUP(Vector, +, 0, -) and Abelian. For a,b:Scalar, u,v,w:Vector. *::infix(Scalar, Vector, Vector). ()|- a * v in Vector. |- (VS1): a * (u+v) = a*u+b*v. |- (VS2): (a+b)*v = a*v + b*v. |- (VS3): (a*b)*v = a*(b*v). |- (VS4): 1 * v = v Many theorems follow for example ()|-(VS5): 0*v = 0. ()|-(VS6): -1 * v = -v. More Results: .Hole . Proof of VS5 .Let v:$Vector, (VS2)|- (0+1)*v = 0*v + 1*v, (VS4)|- (0+1)*v = 0*v +v, (Field)|- 1*v = 0*v + v, (-1)|- v = 0*v +v, (GROUP)|- 0*v = v-v = 0 .Close.Let . Proof of VS6 .Let |-(let): v:$Vector. (Scalar, Field)|- 1 in$Scalar, (-1)|- -1 in $Scalar, (-2)|- 1 + -1 = 0, (-1)|- (1+ -1)*v = 0 * v, (-1, VS5)|- 1*v + (-1)*v = 0, (-1)|- v + (-1)*v =0, (-1, GROUP)|- (-1)*v = -v. .Close.Let .Close.Net . Simple Scalar Products and Inner Products For Scalar:$Field, x,y: $VECTOR(Scalar), ::Scalar. .Hole Also see example: .See ./math_95_Function_Spaces.html#Hilbert Space . Linear maps on Vector Spaces Given two vector spaces V1 and V2 LINEAR::=following .Net Scalar::Sets=given. V1::$VECTOR(Scalar)=given. V2::$VECTOR(Scalar)=given. f::V1->V2=goal. For x,y:V1, a:$Scalar. |- for all x,y (f(x+y)=f(x)+f(y)). |- for all a, x ( f(a*x) = a*f(x)). .Close.Net . Dual Spaces and Inner Products For a Scalar:$Field, Vector space V:$VECTOR(Scalar) then define V*:the set of linear maps from V into $Scalar is the dual vector space. DUAL ::=following, .Net Scalar::Sets=given. Vector::$VECTOR(Scalar)=goal. For x,y:V, a:$Scalar. Dual::={ f: Vector->Scalar . for all x,y (f(x+y)=f(x)+f(y))), for all a, x ( f(a*x) = a*f(x)) } For f,g:Dual. f+g::= map[x]( f(x)+g(x)). a * f::= map[x] a*f(x). ()|-Dual in$VECTOR(Scalar). .Close.Net For Scalar:$Field, V1:$VECTOR(Scalar), x:V,y: V*, ::Scalar. .Open Linear Maps . Linear, quadratic, etc .Hole . Matrices Matrices were invented as a a convenient way to express how linear equations work. They are no more than a rectangular array of numbers provided with a cleverly chosen set of operations so that they form a complex algebra with addition, zero, subtraction, partial non-commutative multiplication, units, and partially existing inverses. We can have matrices made up of any kind of numbers: integers, rationals, reals, and complex numbers. See .See http://en.wikipedia.org/wiki/Matrix_(mathematics) on the Wikipedia for the traditional approach. .Net Numbers:: Field=given. Given a couple of Indexes we can put: matrices::= Index1 >< Index2 >-> Numbers. All finite matrices have a finite number of rows(R) and collumns(C): Mat(R,C)::@Matrices, set of R><(1..C) >-> Numbers. Traditionally we use subscripts to indicate particular elements in a matrix. So in MATHS we put the subscripts in square brackets. A[r,c] = the element in row r and column c. When there is one row we call the matrix a row vector: Row(R)::=Mat(R,1). When there is one column we call the matrix a column vector: Col(C)::=Mat(1,C). One simple notation is to use a table: Q::Mat(n,n)=following, .Table .Row (n-1)a+b (n-1)b 0 0 ... 0 0 .Row 2 a (n-2)a+2 b (n-2)b 0 ... 0 0 .Row 0 3 a (n-3)a+3 b (n-3)b ... 0 0 .Row 0 0 4 a (n-4)a+4 b ... 0 0 .Row ... ... ... ... ... ... ... .Row 0 0 0 0 ... a+(n-1)b b .Row 0 0 0 0 ... n a n b .Close.Table Traditionally we associate a vector it R elements with a row matrix in Row(R). In maths we can introduce a pair of coercions: x+>X where X[r,1] = x[r], y+>Y where Y[1,c] = y[c]. A matrix with R rows and C columns represents a linear map from the Linear space with R dimensions to a vector space od C dimensions. Let x be an R-diemsional vector and y the corresponding C dimensional vector then y[c] = +[r:R] (x[r] * A[r,c]) Given this a simple generalization and some experiments with composing linear maps leads to matrix algebra. Sums and products are only defined between matrices of the right sizes... .Key Sum of two matrices (A+B)[r,c] = A[r,c] + B[r,c]. .Key Product of two matrices with R>B. |- (BA1): for all x,y:B( x= -(-x+ -y)+ -(-x+y) ). ()|-(BA3i): x+ -x = y+ -y. ()|-(BA3ii): - -x = x. ()|-(BA3iii): -x= -(x+y) + -(x+ -y). ()|-(BA3iv): x+(y+ -y) = z+ -z. ()|-(BA3v): x+x = x+ -(y+ -y). ()|-(BA3vi):x+x = x. For x,y:B, x*y::=-(-x+ -y). (STANDARD)|- (*) higher_priority_than (+). ()|-(BA3vii): x*x =x. ()|-(BA3viii): x*y=y*x. ()|-(BA3ix): (x*y)*z=x*(y*z). ()|-ABELIAN_SEMIGROUP(B,*). ()|-(BA3x): (x+y)*x=x. ()|-(BA3xi): x = x*y +(x * -y). ()|-(BA3xii): x=(x+ -y)*(x+y). ()|-(BA3xiii): (x+y)* -x=y* -x. ()|-(BA3xiv): x+x*y=x. ()|-(BA3xv): x*(y+z)=x*y+x*z. ()|-(BA3xvi): -(x+y)= -x * -y. ()|-(BA3xvii): -(x*y)= -x + -y. ()|-(BA3xviii): x+(y*z) = (x+y)*(x+z). ()|-(BA3xix): ((-x)*y)+(x*z)=(x+y)*(-x+y). ()|-(BA3xx): (v*w+ -v*x)* -(v*y+ -v*z) = v*w* -y + -v * x* -z. ()|-(BA3xxi): x+y=x+(-x)*y. Proofs are on pages 8 to 10 of .See [Maddox96] where (BA3xx) for example is his 3(xx). (BA2i)|- one $img(x:B. x+ -x) and one$img(x:B. -(x+ -x)). 1::=the img(x:B. x+ -x). 0::=the img(x:B. -(x+ -x)). ()|-(BA5i): 1 = x+ -x. ()|-(BA5ii): 0 = x*(-x). ()|-(BA5iii): -1 = 0. ()|-(BA5iv): -0 = 1. ()|-(BA5v): x.1 =1. ()|-(BA5vi): x.0 = 0. ()|-(BA5vii): x+0 = 0. ()|-(BA5viii): x.1 = x. x<=y ::= x+y=y. x>=y ::= y<=x. ()|-(BA7i): $POSET(B, <=). ()|-(BA7ii): 0<=x<=1. ()|-(BA7iii): if x<=y then x+z<=y+z and x*y<=y*z. ()|-(BA7iv):$LATTICE(B, +, *). ()|-(BA7v): x<=y iff -y <= -x iff x+y=y iff x*y=x iff -y+x=x iff -x+y=1 iff x*- y=0. ()|-(BA7vi): x.y<=z iff y<= -x +z. (STANDARD)|- For I:Sets, X:I->B, +X::=sum of all X, *X::=product of all X, -X::= map[i:I](-X(i)). + and * are only partial maps from (I->B) into B. +X and/or *X may not exist. ()|-(BA8i):if I={} then +X=0 and *X=1. ()|-(BA8ii): if +X exists then *(-X) exists and -(+X)=*(-X). ()|-(BA8iii): if *X exists then +(-X) exists and -(*X)=+(-X). ()|-(BA8iv): For every y, *{x. x>=y} and +{x, x<=y} exist and are equal to y. (LATTICE): complete=existence of sums and products of any set of elements. ()|- If complete then for all I,X(*X and +X exist). For I:Sets, X,Y:I->B. (STANDARD)|- X+Y ::= map[i](X(i)+Y(i). (STANDARD)|- X*Y ::= map[i](X(i)*Y(i). ()|-(BA9i): If +X and +Y exist then +(X+Y)= (+X)+(+Y). ()|-(BA9ii): If *X and *Y exits then *(X*Y) = (*X)*(*Y). ()|-(BA9iii): If for all i(X(i)<= Y(i)) then (if +X and +Y exist then +X<= +Y) and (if *X and *Y exist then *X<= *Y). For T:Types, I,J:Sets(T), X:(I|J)->B, XI:=map[i:I]X(i), XJ:=map[i:J](X(i)). ()|-(BA10i): if +XI and +XJ exist then +X=+XI + +XJ. ()|-(BA10ii): BA10i((+)=>(*)). ()|-(BA10iii): if +XI and +XJ exist and I==>J then +XI <= +XJ. ()|-(BA10iv): BA10iii((+)=>(*)). . Operators Dual functions: For all f:B->B, dual(f) ::= -(f(-(_))). ()|-(BA11): dual o dual = Id. For f, conjugates(f)={g. for all x,y(f(x)*y =0 iff x.g(y)=0}. ()|-(BA14i): for all g,h:conjugates(f)(g=h). ()|-(BA14ii): f in conjugates(g) iff g in conjugates(f). (f and g are conjugate) ::= f in conjugate(g). normal::@(B->B)={f. f(0)=0}. monotonic::={f. for all x<=y(f(x)<=f(y)}. additive::={f. f(x+y)=f(x)+f(y)}. multiplicative::={f. f(x*y)=f(x)*f(y)}. completely_additive::={f. for all I:Sets, X:I->B(if +X exists and I<>{} then +f(X) exists and +f(X) = f(+X))}. Similarly for complete_multiplicative. universally_additive::= completely_additive & normal, universally_multiplicative::=completely_multiplicative & {f. f(1)=1}. ()|-(BA16): for all x, (x*_) and (_*x) are universally_additive & completely_multiplicative and (x+_) and (_+X) are universally_multiplicative and completely_additive. ()|-(BA17): completely_additive==>additive==>monotonic and completely_multiplicative==multiplicative==>monotonic. ()|-(BA19iii):for W:{(universally_additive+>universally_multiplicative), (completely_additive+>completely_multiplictive), (finitely_additive+>finitely_multiplicative), f:B->B, w:W, f in w(1) iff dual(f) in w(2). ()|-(BA18i): the congugate(f) = map[y](*{x: y<=dual(f)(x)}) -- if it exists. ()|-(BA18ii): some conjugate(f) iff f in univerally_additive and for all y( *{x. y<=dual(f)(x) } exists). ()|-(BA19): f and g are conjugate iff for all x,y(f(x*-g(y)) <= f(x)*-y) iff for all x,y( g(y* -f(x))<= g(y)&-x) iff f and g are normal and for all z,y(f(y)*z <= f(y*g(z)) and g(z)*y<=g(z*f(y))) ). f^i::=result of composing f with itslef i times. f^0=0. f^(i+1)=f(f^i). ()|-(BA21i): constant_functions are monotonic and Id in monotonic and sum and product of monotonic functions are monotonic. ()|-(BA21ii): if complete then for all f: I->monotonic, +f and *f are monotonic. ()|-(BA21iii):if complete then for all f:B>B(if for all z(f(_,z) in monotonic) then *{z. z>=f(_,z)} and +{z. z<=f(_,z)} are monotonic). . Tarski Fixed Points For X:Sets, f:X->X, fixed(f) ::={x. x=f(x)}. For X:Sets, f:X->X, decreased(f) ::={x. x<=f(x)}. For X:Sets, f:X->X, increased(f) ::={x. x>=f(x)}. BA22::=following .Let $LATTICE(A, <=, complete). f:$monotonic(A->A). ()|-(BA22i):fix(f)<>{} and LATTICE(fix(f), <=). ()|-(BA22ii):+decreased(f) = +fixed(f) in fixed(f). ()|-(BA22iii): *increased(f) = *fixed(f) in fixed(f). .Close.Let .Close.Net .Close Boolean Algebras .Open Relation Algebras Maddux traces this theory Back from Pierce to Boole and De Morgan, and forwrd to Schoder. Tarski also worked on this. RELATION_ALGEBRA::=following .Net |- $BOOLEAN_ALGEBRA(A, +, -). Note: complete in {true,false) is inherited from the Boolean algebra. Semicolon represents an associative operator with a unit: |-$MONOID(A,;, I) (;) higher_priority_than (+) and (*). (;) $distributes_over (+). |-$UNARY(A,(/)). |- (RA4): for all x, /(/x) = x. |- (RA5): /(x+y) = /x + /y. |- (RA6): /(x;y) = /y ; /x. |- (RA7): /x;-(x;y) + -y = -y. |- (RA7): /x;-(x;y) <= -y and /x;-(x;y)*y =0. x \dagger y::= - ( -x * -y). Example::=following .Net U:Sets. ()|-RELATION_ALGEBRA(@(U,U), (+)=>(|), (*)=>(&), 1=>U>Id, 0=>{}). .Close.Net proper::@=the relation algebra is of a set of binary relations: for some U(A=@(U,U) and $Example). representable::@=isomorphic to a$proper relation algebra. However, there are an infinity of relation algebras that are not represented by an @(U,U) for any U. ()|-(RA24i): x <= y iff /x <= /y. ()|-(RA24ii): /0 = 0. ()|-(RA24iii): /1 = 1. ()|-(RA24iv): /(-x) = -(/x). ()|-(RA24v): /(x*y) = (/x)*(/y). ()|-(RA24vi): 0 = /x * y iff 0 = x * /y. ()|-(RA24vii): (/) is universally additive and universally multiplicative. ()|-(RA24viii): /I=I. ()|-(RA24ix): x;(y+z)= x;y + x;z. ()|-(RA24x): if x <= y then z;x <= z;y and x;z <= y;z. ()|-(RA24xi): the functions (x;_) and (/x;_) are conjugate. ()|-(RA24xii): -(x;y);/x <= y. ()|-(RA24xiii): (_;x) conjugate (_;/x). ()|-(RA24xiv): (x;y)*z=0 iff (/x;z)*y=0 iff (z;/y)*x=0. ()|-(RA24xv): (x;_) and (_;x) are universally_additive. ()|-(RA24xvi): (x;y)*z <= x;(y * (/x; z)). ()|-(RA24xvii): (y;x) * z <= (y*(z;/x));x). ()|-(RA24xviii): x;0 = 0 = 0;x. ()|-(RA24xix): x;I = x = x;I. ()|-(RA24xx): x <= x;1. ()|-(RA24xxi): x <= 1;x. ()|-(RA24xxii): 1;1=1. ()|-(RA24xxiii): (x;y_ * -(x;z) = x; (y*-z)*-(x;z). ()|-(RA24xxiv): -(x;y) + (x;z) = -(x;(y&-z)) + x;z. domain_elements::@A={x:A. x;1=x). For e,d:domain_elements. ()|-(RA24xxv): (-e);1= -e. ()|-(RA24xxvi): (e*y);z = e*(y;z). ()|-(RA24xxvii): (e*d) in domain_elements. ()|-(RA24xxviii): (e*I);y=e*y. ()|-(RA24xxix): (y*/e);z=y;(e*z) = (y*/e);(e*z). conditional_elements::@A={c:A. c<=I}. For c,c1:conditional_elements. ()|-(RA24xxx): /c = c. ()|-(RA24xxxi): (c;1)*y = c*y. ()|-(RA24xxxii): -(c;1)*I= (/c)*I. ()|-(RA24xxxiii): c;c1 = c*c1. ()|-(RA24xxxiv): (c;z) * (c;c1) = (c*c1);z. ()|-(RA24xxxv): (c;y)*-z = (c;z)* -(c;z). In the $Example.$domain_elements={ W>U}. ()|- BOOLEAN_ALGEBRA(domain_elements, complete) functional_elements::@A={x. /x;x=I}. $Example.$functional_elements are partial functions. ()|-(RA28i+ii): SEMIGROUP(functional_elements, (;)). ()|-(RA28iii): x in functional_elements iff for all y( (x;y) * (x;-y) = 0). ()|-(RA28iv): conditional_elements ==> functional_elements. For all x:A, i:Natoo, x^0 ::= I, x^(i+1) ::=x;(x^i). For all x:A, if it exists, x^oo ::= +[i:Natoo](x^i). ()|-(RA30): If complete then q^oo;p=*{x. x>=p+q;x} and -(q^oo;-p) = +{x. x<= p*-(q;-x))} and *{x. x>=p+q;x};y = *{x. x>=p;y+q;x}. |- For p,q:A, fixed(p,q)={c. c=p+q;c}. ()|- fixed(p,q) = fixed( p+q:(_) ). |- For p,q:A, decreased(p,q)={c. c<=p+q;c}. |- For p,q:A, increased(p,q)={c. c>=p+q;c}. ()|-(BA31i): for c:fixed(q,t), +decreased(p+q,t)= +decreased(p,t)+c. ()|-(BA31ii): +decreased(p+q,t)=+decreased(p,t)+ +decreased(q,t). ()|-(BA31ii): *increased(p*q,t)=*increased(p,t) * *increased(q,t). . Pseudo-inverses In general there is no y such that x;y=I. Dijkstra's Discipline of Programming turns on defining and using the properties of a kind of pseudo-inverse - the weakest condition needed to guarantee termination with a given property. Maddux defines something like this: wlp(r) ::=map[x]( -(r;-x)). This relation does not allow non-x to occur. Pierce and De Morgan studied -(-x;y). .Close.Net .Close Relation Algebras . Glossary distributes_over::=* distributes over + iff x*(y+z)=(x*y)+(x*z). img(x:X. e(x)) ::= {y. for some x:X(y=e(x))}. If f is a function from X to Y then f(A)=img(a:A. f(a)). Another equivalent form: img(x:X. e) = X.[x](e) . Links STANDARD::=http://www/dick/maths/math_11_STANDARD.html. ABELIAN_SEMIGROUP::=http://www/dick/maths/math_32_Semigroups.html#ABELIAN_SEMIGROUP. SEMIGROUP::=http://www/dick/maths/math_32_Semigroups.html. MONOID::=$SEMIGROUP with u:units(Set,op). GROUP::=http://www/dick/maths/math_34_Groups.html#GROUP. UNARY::=$ALGEBRA with function:Set->Set. .See http://www/dick/maths/math_15_Unary_Algebra.html Field::=http://www/dick/maths/math_41_Two_Operators.html#Field. POSET::=http://www/dick/maths/math_21_Order.html#POSET LATTICE::=http://www/dick/maths/math_41_Two_Operators.html#LATTICE. See_also::=http://www/dick/maths/math_31_One_Associative_Op.html .Close Boolean and Relation Algebras .Open Varieties .See [Maddux96] p23 If an net is defined as an algebra with nothing but equations in its axioms then it "forms a variety". Therefore there are subalgebras, homomorphic images and direct products with the same axioms. .Close Varieties .Close Three or More Infix operators