.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 are at least a convenient way to express how linear equations work. They form a complex algebra with addition, zero, subtraction, partial non-commutative multiplication, unit, with partially existing inverses. We can have matrices made up of any kind of numbers: integers, rationals, reals, and complex numbers. Matrix::@Sets, set of all matrices. Mat(R,C)::@Sets, set of R><(1..C) >-> Numbers. 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 .Hole . Frames of Reference .Hole .Close Linear Maps .Close .Open Boolean and Relation Algebras .See [Maddux96] Relation algebras have a long history and can be used in a natural way to express the semantics of programming languages. This is done by definining the meaning of a statement as a pair of elements in a relation algebra. The first can be any relation and indicates the relationship between the initial anf final states if the program terminates. The second part of the meaning of a statement is a conditional relation that describes when the statement does not terminate. Notice that in this model we can define about programs that would have an effect if they terminated even tho they but do not terminate .Open Boolean Algebras Maddux's minimal axiomatic treatment below($BOOLEAN_ALGEBRA) is consistent with an alternate treatment .See http://www/dick/maths/math_41_Two_Operators.html#BOOLEAN_ALGEBRA BOOLEAN_ALGEBRA::=following .Net |- $ALGEBRA. B::=Set. For x,y,z:B. |- (BA0): $ABELIAN_SEMIGROUP(B, +). (-) ::B->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