:: Preliminaries to the Lambek Calculus :: by Wojciech Zielonka :: :: Received February 13, 1991 :: Copyright (c) 1991-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, STRUCT_0, BINOP_1, SUBSET_1, FINSEQ_1, FUNCT_1, VALUED_1, RELAT_1, FINSET_1, TREES_2, ZFMISC_1, NUMBERS, CARD_1, MCART_1, ORDINAL4, FUNCOP_1, TARSKI, ORDINAL1, XXREAL_0, ARYTM_3, CARD_3, NAT_1, FUNCT_5, PRELAMB; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, REAL_1, BINOP_1, RELSET_1, FINSEQ_1, FINSEQ_2, FINSET_1, MCART_1, STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FUNCT_5, RVSUM_1, XCMPLX_0, NAT_1, TREES_1, TREES_2, XXREAL_0; constructors BINOP_1, FUNCT_3, XXREAL_0, NAT_1, RVSUM_1, TREES_2, MIDSP_1, FUNCT_5, RELSET_1, BINOP_2, FUNCOP_1, REAL_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, NUMBERS, MEMBERED, FINSEQ_1, TREES_2, STRUCT_0, VALUED_0, CARD_1, XTUPLE_0, RVSUM_1, XCMPLX_0, NAT_1, XXREAL_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin :: Proofs and cut-freedom definition struct (1-sorted) typealg (#carrier -> set, left_quotient, right_quotient, inner_product -> BinOp of the carrier #); end; registration cluster non empty strict for 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,T9,X9,Y9 for FinSequence of s, x,y,z,y9,z9 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 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 s, Tr; let v be Element of dom Tr; attr v is correct means :: PRELAMB:def 4 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 5 ex x,y st IT = x\y; attr IT is right means :: PRELAMB:def 6 ex x,y st IT = x/"y; attr IT is middle means :: PRELAMB:def 7 ex x,y st IT = x*y; end; definition let s; let IT be type of s; attr IT is primitive means :: PRELAMB:def 8 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 9 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); end; notation let s; let Tr be finite DecoratedTree of the carrier of s, x; antonym Tr does_not_represent x for Tr represents x; end; definition let IT be non empty typealg; attr IT is free means :: PRELAMB:def 10 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 11 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 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 12 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; 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 ... or (p.v)`2 = 7; definition let s; let IT be PreProof of s; attr IT is cut-free means :: PRELAMB:def 13 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 14 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 15 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 16 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 struct(typealg) typestr (# carrier -> set, left_quotient, right_quotient, inner_product -> BinOp of the carrier, derivability -> Relation of (the carrier)*,the carrier #); end; registration cluster non empty strict for typestr; end; reserve s for non empty typestr, x for type of s; definition let s; let f be FinSequence of s, x; pred f ==>. x means :: PRELAMB:def 17 [f,x] in the derivability of s; end; definition let IT be non empty typestr; attr IT is SynTypes_Calculus-like means :: PRELAMB:def 18 (for x being type of IT holds <*x*> ==>. x) & (for T being FinSequence of IT, x,y being type of IT st T^<*y*> ==>. x holds T ==>. x/"y) & (for T being FinSequence of IT, x,y being type of IT st <*y*>^T ==>. x holds T ==>. y\x) & (for T,X,Y being FinSequence 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 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 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 IT, x,y being type of IT st X ==>. x & Y ==>. y holds X^Y ==>. x*y; end; registration cluster SynTypes_Calculus-like for 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 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 19 <*x*> ==>. y & <*y*> ==>. x; reflexivity; symmetry; end; theorem :: PRELAMB:25 x/"y <==>. x/"((x/"y)\x); theorem :: PRELAMB:26 x/"(z*y) <==>. (x/"y)/"z; theorem :: PRELAMB:27 <*x*(y/"z)*> ==>. (x*y)/"z; theorem :: PRELAMB:28 <*x*> ==>. (x*y)/"y & <*x*> ==>. y\(y*x); theorem :: PRELAMB:29 x*y*z <==>. x*(y*z);