Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### 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