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);