PRELAMB: Preliminaries to the Lambek Calculus

attr v is correct means :Def4: :: PRELAMB:def 4
( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] ) if (Tr . v) `2 = 0
( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st
( (Tr . v) `1 = [T,(x /" y)] & (Tr . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) ) if (Tr . v) `2 = 1
( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s 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 being FinSequence of s ex x, y, z being type of s 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 being FinSequence of s ex x, y, z being type of s 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
for z being type of s holds
( branchdeg v = 1 & ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s 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 being FinSequence of s ex x, y being type of s 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 being FinSequence of s ex y, z being type of s 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;

correctness ;

end;

:: deftheorem Def4 defines correct PRELAMB:def 4 :

definition

let s be non empty typealg ;
let IT be type of s;

attr IT is left means :: PRELAMB:def 5
ex x, y being type of s st IT = x \ y;

attr IT is right means :: PRELAMB:def 6
ex x, y being type of s st IT = x /" y;

attr IT is middle means :: PRELAMB:def 7
ex x, y being type of s st IT = x * y;

end;

:: deftheorem defines left PRELAMB:def 5 :

:: deftheorem defines right PRELAMB:def 6 :

:: deftheorem defines middle PRELAMB:def 7 :

definition

let s be non empty typealg ;
let IT be type of s;

attr IT is primitive means :: PRELAMB:def 8
( not IT is left & not IT is right & not IT is middle );

end;

:: deftheorem defines primitive PRELAMB:def 8 :

definition

let s be non empty typealg ;
let Tr be finite DecoratedTree of the carrier of s;
let v be Element of dom Tr;
:: original: .
redefine func Tr . v -> type of s;
coherence

proof end;

end;

definition

let s be non empty typealg ;
let Tr be finite DecoratedTree of the carrier of s;
let x be type of s;

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 being type of s st
( ( Tr . v = y /" z or Tr . v = y \ z or Tr . v = y * z ) & Tr . (v ^ <*0*>) = y & Tr . (v ^ <*1*>) = z ) ) ) ) );

end;

:: deftheorem defines represents PRELAMB:def 9 :

notation

let s be non empty typealg ;
let Tr be finite DecoratedTree of the carrier of s;
let x be type of s;
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
( ( for x being type of IT holds
( not ( x is left & x is right ) & not ( x is left & x is middle ) & not ( x is right & x is 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;

:: deftheorem defines free PRELAMB:def 10 :

definition

let s be non empty typealg ;
let x be type of s;
assume A1: 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 );

existence by A1;
uniqueness ;

end;

:: deftheorem defines repr_of PRELAMB:def 11 :

definition

let s be non empty typealg ;
let f be FinSequence of s;
let t be type of s;
:: original: [
redefine func [f,t] -> Element of [:( the carrier of s *), the carrier of s:];
coherence

proof end;

end;

definition

let s be non empty typealg ;

mode Proof of s -> PreProof of s means :Def12: :: PRELAMB:def 12
( dom it is finite & ( for v being Element of dom it holds v is correct ) );

existence

proof end;

end;

:: deftheorem Def12 defines Proof PRELAMB:def 12 :

theorem Th1: :: PRELAMB:1

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st branchdeg v = 1 holds
v ^ <*0*> in dom p

proof end;

theorem Th2: :: PRELAMB:2

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st branchdeg v = 2 holds
( v ^ <*0*> in dom p & v ^ <*1*> in dom p )

proof end;

theorem :: PRELAMB:3

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st (p . v) `2 = 0 holds
ex x being type of s st (p . v) `1 = [<*x*>,x]

proof end;

theorem :: PRELAMB:4

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st (p . v) `2 = 1 holds
ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st
( w = v ^ <*0*> & (p . v) `1 = [T,(x /" y)] & (p . w) `1 = [(T ^ <*y*>),x] )

proof end;

theorem :: PRELAMB:5

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st (p . v) `2 = 2 holds
ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st
( w = v ^ <*0*> & (p . v) `1 = [T,(y \ x)] & (p . w) `1 = [(<*y*> ^ T),x] )

proof end;

theorem :: PRELAMB:6

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st (p . v) `2 = 3 holds
ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s 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] )

proof end;

theorem :: PRELAMB:7

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st (p . v) `2 = 4 holds
ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s 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] )

proof end;

theorem :: PRELAMB:8

for s being non empty typealg
for z being type of s
for p being Proof of s
for v being Element of dom p st (p . v) `2 = 5 holds
ex w being Element of dom p ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st
( w = v ^ <*0*> & (p . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (p . w) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] )

proof end;

theorem :: PRELAMB:9

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st (p . v) `2 = 6 holds
ex w, u being Element of dom p ex X, Y being FinSequence of s ex x, y being type of s st
( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(X ^ Y),(x * y)] & (p . w) `1 = [X,x] & (p . u) `1 = [Y,y] )

proof end;

theorem Th10: :: PRELAMB:10

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st (p . v) `2 = 7 holds
ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex y, z being type of s 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] )

proof end;

theorem :: PRELAMB:11

for s being non empty typealg
for p being Proof of s
for v being Element of dom p holds
not not (p . v) `2 = 0 & ... & not (p . v) `2 = 7

proof end;

definition

let s be non empty typealg ;
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;

:: deftheorem defines cut-free PRELAMB:def 13 :

definition

let s be non empty typealg ;

func size_w.r.t. s -> Function of the carrier of s,NAT means :: PRELAMB:def 14
for x being type of s holds it . x = card (dom (repr_of x));

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines size_w.r.t. PRELAMB:def 14 :

definition

let D be non empty set ;
let T be FinSequence of D;
let f be Function of D,NAT;
:: original: (#)
redefine func f * T -> FinSequence of REAL ;
coherence

proof end;

end;

definition

let s be non empty typealg ;
let p be Proof of s;

func cutdeg p -> Nat means :: PRELAMB:def 15
ex T, X, Y being FinSequence of s ex y, z being type of s 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 ;

existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem defines cutdeg PRELAMB:def 15 :

definition

let s be non empty typealg ;
let A be non empty set ;

mode Model of s,A -> Function of the carrier of s,(bool (A *)) means :: PRELAMB:def 16
for x, y being type of s holds
( it . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in it . x & b in it . y ) } & it . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in it . y holds
a1 ^ b in it . x } & it . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in it . y holds
b ^ a2 in it . x } );

existence

proof end;

end;

:: deftheorem defines Model PRELAMB:def 16 :

definition

attr c₁ is strict ;
struct typestr -> typealg ;
aggr typestr(# carrier, left_quotient, right_quotient, inner_product, derivability #) -> typestr ;
sel derivability c₁ -> Relation of ( the carrier of c₁ *), the carrier of c₁;

end;

registration

cluster non empty strict for typestr ;

existence

proof end;

end;

definition

let s be non empty typestr ;
let f be FinSequence of s;
let x be type of s;

pred f ==>. x means :: PRELAMB:def 17
[f,x] in the derivability of s;

end;

:: deftheorem defines ==>. PRELAMB:def 17 :

definition

let IT be non empty typestr ;

attr IT is SynTypes_Calculus-like means :Def18: :: PRELAMB:def 18
( ( for x being type of IT holds <*x*> ==>. x ) & ( for T being FinSequence of IT
for x, y being type of IT st T ^ <*y*> ==>. x holds
T ==>. x /" y ) & ( for T being FinSequence of IT
for x, y being type of IT st <*y*> ^ T ==>. x holds
T ==>. y \ x ) & ( for T, X, Y being FinSequence of IT
for 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
for 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
for 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
for x, y being type of IT st X ==>. x & Y ==>. y holds
X ^ Y ==>. x * y ) );

end;

:: deftheorem Def18 defines SynTypes_Calculus-like PRELAMB:def 18 :

registration

cluster non empty SynTypes_Calculus-like for typestr ;

existence

proof end;

end;

theorem Th12: :: PRELAMB:12

for s being SynTypes_Calculus
for x, y being type of s holds
( <*(x /" y)*> ^ <*y*> ==>. x & <*y*> ^ <*(y \ x)*> ==>. x )

proof end;

theorem Th13: :: PRELAMB:13

for s being SynTypes_Calculus
for x, y being type of s holds
( <*x*> ==>. y /" (x \ y) & <*x*> ==>. (y /" x) \ y )

proof end;

theorem Th14: :: PRELAMB:14

for s being SynTypes_Calculus
for x, y, z being type of s holds <*(x /" y)*> ==>. (x /" z) /" (y /" z)

proof end;

theorem Th15: :: PRELAMB:15

for s being SynTypes_Calculus
for x, y, z being type of s holds <*(y \ x)*> ==>. (z \ y) \ (z \ x)

proof end;

theorem :: PRELAMB:16

for s being SynTypes_Calculus
for x, y, z being type of s st <*x*> ==>. y holds
( <*(x /" z)*> ==>. y /" z & <*(z \ x)*> ==>. z \ y )

proof end;

theorem Th17: :: PRELAMB:17

for s being SynTypes_Calculus
for x, y, z being type of s st <*x*> ==>. y holds
( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z )

proof end;

theorem Th18: :: PRELAMB:18

for s being SynTypes_Calculus
for x, y being type of s holds <*(y /" ((y /" x) \ y))*> ==>. y /" x

proof end;

theorem Th19: :: PRELAMB:19

for s being SynTypes_Calculus
for x, y being type of s st <*x*> ==>. y holds
( <*> the carrier of s ==>. y /" x & <*> the carrier of s ==>. x \ y )

proof end;

theorem Th20: :: PRELAMB:20

for s being SynTypes_Calculus
for x being type of s holds
( <*> the carrier of s ==>. x /" x & <*> the carrier of s ==>. x \ x )

proof end;

theorem :: PRELAMB:21

for s being SynTypes_Calculus
for x, y being type of s holds
( <*> the carrier of s ==>. (y /" (x \ y)) /" x & <*> the carrier of s ==>. x \ ((y /" x) \ y) )

proof end;

theorem :: PRELAMB:22

for s being SynTypes_Calculus
for x, y, z being type of s holds
( <*> the carrier of s ==>. ((x /" z) /" (y /" z)) /" (x /" y) & <*> the carrier of s ==>. (y \ x) \ ((z \ y) \ (z \ x)) )

proof end;

theorem :: PRELAMB:23

for s being SynTypes_Calculus
for x, y being type of s st <*> the carrier of s ==>. x holds
( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y )

proof end;

theorem :: PRELAMB:24

for s being SynTypes_Calculus
for x, y being type of s holds <*(x /" (y /" y))*> ==>. x

proof end;

definition

let s be SynTypes_Calculus;
let x, y be type of s;

pred x <==>. y means :: PRELAMB:def 19
( <*x*> ==>. y & <*y*> ==>. x );

reflexivity by Def18;
symmetry ;

end;

:: deftheorem defines <==>. PRELAMB:def 19 :

theorem :: PRELAMB:25

for s being SynTypes_Calculus
for x, y being type of s holds x /" y <==>. x /" ((x /" y) \ x) by Th13, Th18;

theorem :: PRELAMB:26

for s being SynTypes_Calculus
for x, y, z being type of s holds x /" (z * y) <==>. (x /" y) /" z

proof end;

theorem :: PRELAMB:27

for s being SynTypes_Calculus
for x, y, z being type of s holds <*(x * (y /" z))*> ==>. (x * y) /" z

proof end;

theorem :: PRELAMB:28

for s being SynTypes_Calculus
for x, y being type of s holds
( <*x*> ==>. (x * y) /" y & <*x*> ==>. y \ (y * x) )

proof end;

theorem :: PRELAMB:29

for s being SynTypes_Calculus
for x, y, z being type of s holds (x * y) * z <==>. x * (y * z)

proof end;