Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Preliminaries to the Lambek Calculus

**by****Wojciech Zielonka**- Received February 13, 1991
- MML identifier: PRELAMB

- [ Mizar article, MML identifier index ]

environ vocabulary BINOP_1, FINSEQ_1, BOOLE, FUNCT_1, SEQ_1, FINSET_1, TREES_1, ORDINAL1, CARD_1, FUNCT_3, RELAT_1, TREES_2, FUNCOP_1, MCART_1, RLVECT_1, MIDSP_1, PRELAMB; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1, CARD_1, BINOP_1, RELSET_1, STRUCT_0, FINSEQ_1, FINSEQ_2, FINSET_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, FUNCOP_1, MIDSP_1, RVSUM_1, NAT_1, TREES_1, TREES_2; constructors BINOP_1, FUNCT_3, MIDSP_1, RVSUM_1, NAT_1, TREES_2, REAL_1, MEMBERED, XBOOLE_0, ARYTM_3, INT_1, RAT_1; clusters SUBSET_1, FINSEQ_1, TREES_1, RELSET_1, TREES_2, FINSET_1, STRUCT_0, FUNCOP_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2, NUMBERS; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: PROOFS AND CUT-FREEDOM reserve D for non empty set; definition struct(1-sorted) typealg(#carrier->set, left_quotient, right_quotient, inner_product->BinOp of the carrier #); end; definition cluster non empty strict typealg; end; definition let s be non empty typealg; mode type of s is Element of s; end; reserve s for non empty typealg, T,X,Y,T',X',Y' for FinSequence of the carrier of s, x,y,z,y',z' for type of s; definition let s,x,y; func x\y -> type of s equals :: PRELAMB:def 1 (the left_quotient of s).(x,y); func x/"y -> type of s equals :: PRELAMB:def 2 (the right_quotient of s).(x,y); func x*y -> type of s equals :: PRELAMB:def 3 (the inner_product of s).(x,y); end; definition let Tr be finite Tree, v be Element of Tr; cluster succ v -> finite; end; definition let Tr be finite Tree, v be Element of Tr; func branchdeg v equals :: PRELAMB:def 4 card succ v; end; definition cluster finite DecoratedTree; end; definition let D be non empty set; cluster finite DecoratedTree of D; end; definition let s; mode PreProof of s is finite DecoratedTree of [:[: (the carrier of s)* , the carrier of s :], NAT :]; end; reserve Tr for PreProof of s; definition let R be finite Relation; cluster dom R -> finite; end; definition let s , Tr; let v be Element of dom Tr; attr v is correct means :: PRELAMB:def 5 branchdeg v = 0 & ex x st (Tr.v)`1 = [<*x*>,x] if (Tr.v)`2 = 0, branchdeg v = 1 & ex T,x,y st (Tr.v)`1 = [T,x/"y] & (Tr.(v^<*0*>))`1 = [T^<*y*>,x] if (Tr.v)`2 = 1, branchdeg v = 1 & ex T,x,y st (Tr.v)`1 = [T,y\x] & (Tr.(v^<*0*>))`1 = [<*y*>^T,x] if (Tr.v)`2 = 2, branchdeg v = 2 & ex T,X,Y,x,y,z st (Tr.v)`1 = [X^<*x/"y*>^T^Y,z] & (Tr.(v^<*0*>))`1 = [T,y] & (Tr.(v^<*1*>))`1 = [X^<*x*>^Y,z] if (Tr.v)`2 = 3, branchdeg v = 2 & ex T,X,Y,x,y,z st (Tr.v)`1 = [X^T^<*y\x*>^Y,z] & (Tr.(v^<*0*>))`1 = [T,y] & (Tr.(v^<*1*>))`1 = [X^<*x*>^Y,z] if (Tr.v)`2 = 4, branchdeg v = 1 & ex X,x,y,Y st (Tr.v)`1 = [X^<*x*y*>^Y,z] & (Tr.(v^<*0*>))`1 = [X^<*x*>^<*y*>^Y,z] if (Tr.v)`2 = 5, branchdeg v = 2 & ex X,Y,x,y st (Tr.v)`1 = [X^Y,x*y] & (Tr.(v^<*0*>))`1 = [X,x] & (Tr.(v^<*1*>))`1 = [Y,y] if (Tr.v)`2 = 6, branchdeg v = 2 & ex T,X,Y,y,z st (Tr.v)`1 = [X^T^Y,z] & (Tr.(v^<*0*>))`1 = [T,y] & (Tr.(v^<*1*>))`1 = [X^<*y*>^Y,z] if (Tr.v)`2 = 7 otherwise contradiction; end; definition let s; let IT be type of s; attr IT is left means :: PRELAMB:def 6 ex x,y st IT = x\y; attr IT is right means :: PRELAMB:def 7 ex x,y st IT = x/"y; attr IT is middle means :: PRELAMB:def 8 ex x,y st IT = x*y; end; definition let s; let IT be type of s; attr IT is primitive means :: PRELAMB:def 9 not (IT is left or IT is right or IT is middle); end; definition let s; let Tr be finite DecoratedTree of the carrier of s; let v be Element of dom Tr; redefine func Tr.v -> type of s; end; definition let s; let Tr be finite DecoratedTree of the carrier of s, x; pred Tr represents x means :: PRELAMB:def 10 dom Tr is finite & for v being Element of dom Tr holds (branchdeg v = 0 or branchdeg v = 2) & (branchdeg v = 0 implies Tr.v is primitive) & (branchdeg v = 2 implies ex y,z st (Tr.v = y/"z or Tr.v = y\z or Tr.v = y*z) & Tr.(v^<*0*>) = y & Tr.(v^<*1*>)= z); antonym Tr does_not_represent x; end; definition let IT be non empty typealg; attr IT is free means :: PRELAMB:def 11 not (ex x being type of IT st x is left right or x is left middle or x is right middle) & for x being type of IT ex Tr being finite DecoratedTree of the carrier of IT st for Tr1 being finite DecoratedTree of the carrier of IT holds Tr1 represents x iff Tr = Tr1; end; definition let s,x such that s is free; func repr_of x -> finite DecoratedTree of the carrier of s means :: PRELAMB:def 12 for Tr being finite DecoratedTree of the carrier of s holds Tr represents x iff it = Tr; end; definition let s; let f be FinSequence of the carrier of s; let t be type of s; redefine func [f,t] -> Element of [:(the carrier of s)*, the carrier of s:]; end; definition let s; mode Proof of s -> PreProof of s means :: PRELAMB:def 13 dom it is finite & for v being Element of dom it holds v is correct; end; reserve p for Proof of s, v for Element of dom p, n,k for Nat; theorem :: PRELAMB:1 branchdeg v = 1 implies v^<*0*> in dom p; theorem :: PRELAMB:2 branchdeg v = 2 implies v^<*0*> in dom p & v^<*1*> in dom p; theorem :: PRELAMB:3 (p.v)`2 = 0 implies ex x st (p.v)`1 = [<*x*>,x]; theorem :: PRELAMB:4 (p.v)`2 = 1 implies ex w being Element of dom p, T,x,y st w = v^<*0*> & (p.v)`1 = [T,x/"y] & (p.w)`1 = [T^<*y*>,x]; theorem :: PRELAMB:5 (p.v)`2 = 2 implies ex w being Element of dom p, T,x,y st w = v^<*0*> & (p.v)`1 = [T,y\x] & (p.w)`1 = [<*y*>^T,x]; theorem :: PRELAMB:6 (p.v)`2 = 3 implies ex w,u being Element of dom p, T,X,Y,x,y,z st w = v^<*0*> & u = v^<*1*> & (p.v)`1 = [X^<*x/"y*>^T^Y,z] & (p.w)`1 = [T,y] & (p.u)`1 = [X^<*x*>^Y,z]; theorem :: PRELAMB:7 (p.v)`2 = 4 implies ex w,u being Element of dom p, T,X,Y,x,y,z st w = v^<*0*> & u = v^<*1*> & (p.v)`1 = [X^T^<*y\x*>^Y,z] & (p.w)`1 = [T,y] & (p.u)`1 = [X^<*x*>^Y,z]; theorem :: PRELAMB:8 (p.v)`2 = 5 implies ex w being Element of dom p, X,x,y,Y st w = v^<*0*> & (p.v)`1 = [X^<*x*y*>^Y,z] & (p.w)`1 = [X^<*x*>^<*y*>^Y,z]; theorem :: PRELAMB:9 (p.v)`2 = 6 implies ex w,u being Element of dom p, X,Y,x,y st w = v^<*0*> & u = v^<*1*> & (p.v)`1 = [X^Y,x*y] & (p.w)`1 = [X,x] & (p.u)`1 = [Y,y]; theorem :: PRELAMB:10 (p.v)`2 = 7 implies ex w,u being Element of dom p, T,X,Y,y,z st w = v^<*0 *> & u = v^<*1*> & (p.v)`1 = [X^T^Y,z] & (p.w)`1 = [T,y] & (p.u)`1 = [X^<*y*>^Y,z]; theorem :: PRELAMB:11 (p.v)`2 = 0 or (p.v)`2 = 1 or (p.v)`2 = 2 or (p.v)`2 = 3 or (p.v)`2 = 4 or (p.v)`2 = 5 or (p.v)`2 = 6 or (p.v)`2 = 7; definition let s; let IT be PreProof of s; attr IT is cut-free means :: PRELAMB:def 14 for v being Element of dom IT holds (IT.v)`2 <> 7; end; definition let s; func size_w.r.t. s -> Function of the carrier of s, NAT means :: PRELAMB:def 15 for x holds it.x = card dom repr_of x; end; definition let D be non empty set, T be FinSequence of D, f be Function of D,NAT; redefine func f*T -> FinSequence of REAL; end; definition let s; let p be Proof of s; func cutdeg p -> Nat means :: PRELAMB:def 16 ex T,X,Y,y,z st (p.{})`1 = [X^T^Y,z] & (p.<*0*>)`1 = [T,y] & (p.<*1*>)`1 = [X^<*y*>^Y,z] & it = (size_w.r.t. s).y + (size_w.r.t. s).z + Sum((size_w.r.t. s)*(X^T^Y)) if (p.{})`2 = 7 otherwise it = 0; end; ::MODELS FOR THE LAMBEK CALCULUS reserve A for non empty set, a,a1,a2,b for Element of A*; definition let s,A; mode Model of s,A -> Function of the carrier of s, bool (A*) means :: PRELAMB:def 17 for x,y holds it.(x*y) = { a ^ b : a in it.x & b in it.y } & it.(x/"y) = { a1 : for b st b in it.y holds a1 ^ b in it.x } & it.(y\x) = {a2: for b st b in it.y holds b ^ a2 in it.x }; end; ::AXIOMS, RULES, AND SOME OF THEIR CONSEQUENCES definition let a,b be non empty set; cluster non empty Relation of a,b; end; definition struct(typealg) typestr (# carrier->set, left_quotient, right_quotient, inner_product->BinOp of the carrier, derivability -> Relation of (the carrier)*,the carrier #); end; definition cluster non empty strict typestr; end; reserve s for non empty typestr, x for type of s; definition let s; let f be FinSequence of the carrier of s, x; pred f ==>. x means :: PRELAMB:def 18 [f,x] in the derivability of s; end; definition let IT be non empty typestr; attr IT is SynTypes_Calculus-like means :: PRELAMB:def 19 (for x being type of IT holds <*x*> ==>. x) & (for T being FinSequence of the carrier of IT, x,y being type of IT st T^<*y*> ==>. x holds T ==>. x/"y) & (for T being FinSequence of the carrier of IT, x,y being type of IT st <*y*>^T ==>. x holds T ==>. y\x) & (for T,X,Y being FinSequence of the carrier of IT, x,y,z being type of IT st T ==>. y & X^<*x*>^Y ==>. z holds X^<*x/"y*>^T^Y ==>. z) & (for T,X,Y being FinSequence of the carrier of IT, x,y,z being type of IT st T ==>. y & X^<*x*>^Y ==>. z holds X^T^<*y\x*>^Y ==>. z) & (for X,Y being FinSequence of the carrier of IT, x,y,z being type of IT st X^<*x*>^<*y*>^Y ==>. z holds X^<*x*y*>^Y ==>.z) & (for X,Y being FinSequence of the carrier of IT, x,y being type of IT st X ==>. x & Y ==>. y holds X^Y ==>. x*y); end; definition cluster SynTypes_Calculus-like (non empty typestr); end; definition mode SynTypes_Calculus is SynTypes_Calculus-like (non empty typestr); end; reserve s for SynTypes_Calculus, T,X,Y for FinSequence of the carrier of s, x,y,z for type of s; theorem :: PRELAMB:12 <*x/"y*>^<*y*> ==>. x & <*y*>^<*y\x*> ==>. x; theorem :: PRELAMB:13 <*x*> ==>. y/"(x\y) & <*x*> ==>. (y/"x)\y; theorem :: PRELAMB:14 <*x/"y*> ==>. (x/"z)/"(y/"z); theorem :: PRELAMB:15 <*y\x*> ==>. (z\y)\(z\x); theorem :: PRELAMB:16 <*x*> ==>. y implies <*x/"z*> ==>. y/"z & <*z\x*> ==>. z\y; theorem :: PRELAMB:17 <*x*> ==>. y implies <*z/"y*> ==>. z/"x & <*y\z*> ==>. x\z; theorem :: PRELAMB:18 <*y/"((y/"x)\y)*> ==>. y/"x; theorem :: PRELAMB:19 <*x*> ==>. y implies <*>the carrier of s ==>. y/"x & <*>the carrier of s ==>. x\y; theorem :: PRELAMB:20 <*>the carrier of s ==>. x/"x & <*>the carrier of s ==>. x\x; theorem :: PRELAMB:21 <*>the carrier of s ==>. (y/"(x\y))/"x & <*>the carrier of s ==>. x\((y/"x)\y ); theorem :: PRELAMB:22 <*>the carrier of s ==>. ((x/"z)/"(y/"z))/"(x/"y) & <*>the carrier of s ==>. (y\x)\((z\y)\(z\x)); theorem :: PRELAMB:23 <*>the carrier of s ==>. x implies <*>the carrier of s ==>. y/"(y/"x) & <*>the carrier of s ==>. (x\y)\y; theorem :: PRELAMB:24 <*x/"(y/"y)*> ==>. x; definition let s,x,y; pred x <==>. y means :: PRELAMB:def 20 <*x*> ==>. y & <*y*> ==>. x; end; theorem :: PRELAMB:25 x <==>. x; theorem :: PRELAMB:26 x/"y <==>. x/"((x/"y)\x); theorem :: PRELAMB:27 x/"(z*y) <==>. (x/"y)/"z; theorem :: PRELAMB:28 <*x*(y/"z)*> ==>. (x*y)/"z; theorem :: PRELAMB:29 <*x*> ==>. (x*y)/"y & <*x*> ==>. y\(y*x); theorem :: PRELAMB:30 x*y*z <==>. x*(y*z);

Back to top