:: Preliminaries to the Lambek Calculus
:: by Wojciech Zielonka
::
:: Received February 13, 1991
:: Copyright (c) 1991-2017 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);