:: 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;
definitions TARSKI, STRUCT_0, XBOOLE_0;
equalities TARSKI;
expansions TARSKI;
theorems FINSEQ_1, ZFMISC_1, TREES_2, FUNCOP_1, FUNCT_2, TARSKI, CARD_1,
TREES_1, NAT_1, CARD_2, RVSUM_1, RELAT_1, FINSEQ_2;
schemes FUNCT_2, FINSEQ_2;
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;
existence
proof
set l = the BinOp of {{}};
take typealg(#{{}},l,l,l#);
thus the carrier of typealg(#{{}},l,l,l#) is non empty;
thus thesis;
end;
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
(the left_quotient of s).(x,y);
coherence;
func x/"y -> type of s equals
(the right_quotient of s).(x,y);
coherence;
func x*y -> type of s equals
(the inner_product of s).(x,y);
coherence;
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
:Def4:
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;
correctness;
end;
definition
let s;
let IT be type of s;
attr IT is left means
ex x,y st IT = x\y;
attr IT is right means
ex x,y st IT = x/"y;
attr IT is middle means
ex x,y st IT = x*y;
end;
definition
let s;
let IT be type of s;
attr IT is primitive means
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;
coherence
proof
reconsider Tr as DecoratedTree of the carrier of s;
reconsider v as Element of dom Tr;
Tr.v is type of s;
hence thesis;
end;
end;
definition
let s;
let Tr be finite DecoratedTree of the carrier of s, x;
pred Tr represents x means
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
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
A1: s is free;
func repr_of x -> finite DecoratedTree of the carrier of s means
for Tr being finite DecoratedTree of the carrier of s holds
Tr represents x iff it = Tr;
existence by A1;
uniqueness;
end;
deffunc PAIRSOF(typealg) = [: (the carrier of $1)*, the carrier of $1 :];
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:];
coherence
proof
f in (the carrier of s)* by FINSEQ_1:def 11;
hence thesis by ZFMISC_1:87;
end;
end;
definition
let s;
mode Proof of s -> PreProof of s means
:Def12:
dom it is finite & for v being Element of dom it holds v is correct;
existence
proof
set x = the type of s;
set Tr = {{}} --> [[<*x*>,x],0];
A1: dom Tr = {{}} by FUNCOP_1:13;
reconsider Tr as finite DecoratedTree
by TREES_1:23;
A2: [[<*x*>,x],0] in [:PAIRSOF(s), NAT:] by ZFMISC_1:87;
{[[<*x*>,x],0]} = rng Tr by FUNCOP_1:8;
then rng Tr c= [:PAIRSOF(s), NAT:] by A2,ZFMISC_1:31;
then reconsider Tr as PreProof of s by RELAT_1:def 19;
take Tr;
thus dom Tr is finite;
let v be Element of dom Tr;
A3: v = {} by A1,TARSKI:def 1;
A4: now set x = the Element of dom Tr-level 1;
assume dom Tr-level 1 <> {};
then x in dom Tr-level 1;
then x in {w where w is Element of dom Tr: len w = 1} by TREES_2:def 6;
then ex w being Element of dom Tr st ( x = w)&( len w = 1);
hence contradiction by A1,CARD_1:27,TARSKI:def 1;
end;
A5: branchdeg v = card succ v by TREES_2:def 12
.= 0 by A3,A4,CARD_1:27,TREES_2:13;
A6: Tr.v = [[<*x*>,x],0] by A1,FUNCOP_1:7;
then
A7: (Tr.v)`1 = [<*x*>,x];
(Tr.v)`2 = 0 by A6;
hence thesis by A5,A7,Def4;
end;
end;
reserve p for Proof of s,
v for Element of dom p;
theorem Th1:
branchdeg v = 1 implies v^<*0*> in dom p
proof
assume branchdeg v = 1;
then
A1: succ v <> {} by CARD_1:27,TREES_2:def 12;
set x = the Element of succ v;
x in succ v by A1;
then x in {v^<*n*> where n is Nat: v^<*n*> in dom p}
by TREES_2:def 5;
then consider n being Nat such that x = v^<*n*> and
A2: v^<*n*> in dom p;
thus thesis by A2,TREES_1:def 3;
end;
theorem Th2:
branchdeg v = 2 implies v^<*0*> in dom p & v^<*1*> in dom p
proof
A1: succ v = {v^<*n*> where n is Nat: v^<*n*> in dom p}
by TREES_2:def 5;
assume branchdeg v = 2;
then card succ v = 2 by TREES_2:def 12;
then consider x,y being object such that
A2: x <> y and
A3: succ v = {x,y} by CARD_2:60;
x in succ v by A3,TARSKI:def 2;
then consider n being Nat such that
A4: x = v^<*n*> and
A5: v^<*n*> in dom p by A1;
y in succ v by A3,TARSKI:def 2;
then consider k being Nat such that
A6: y = v^<*k*> and
A7: v^<*k*> in dom p by A1;
n <> 0 or k <> 0 by A2,A4,A6;
then
A8: n > 0 or k > 0;
thus v^<*0*> in dom p by A5,TREES_1:def 3;
n >= 0+1 or k >= 0+1 by A8,NAT_1:13;
hence thesis by A5,A7,TREES_1:def 3;
end;
theorem
(p.v)`2 = 0 implies ex x st (p.v)`1 = [<*x*>,x]
proof
v is correct by Def12;
hence thesis by Def4;
end;
theorem
(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]
proof
A1: v is correct by Def12;
assume
A2: (p.v)`2 = 1;
then
A3: ex T,x,y st (p.v)`1 = [T,x/"y] & (p.(v^<*0*>))`1 = [T^<*y*>,x] by A1,Def4;
branchdeg v = 1 by A1,A2,Def4;
then v^<*0*> in dom p by Th1;
hence thesis by A3;
end;
theorem
(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]
proof
A1: v is correct by Def12;
assume
A2: (p.v)`2 = 2;
then
A3: ex T,x,y st (p.v)`1 = [T,y\x] & (p.(v^<*0*>))`1 = [<*y*>^T,x] by A1,Def4;
branchdeg v = 1 by A1,A2,Def4;
then v^<*0*> in dom p by Th1;
hence thesis by A3;
end;
theorem
(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]
proof
A1: v is correct by Def12;
assume
A2: (p.v)`2 = 3;
then
A3: ex T,X,Y,x,y,z st (p.v)`1 = [X^<*x/"y*>^T^Y,z] &
(p.(v^<*0*>))`1 = [T,y] & (p.(v^<*1*>))`1 = [X^<*x*>^Y,z] by A1,Def4;
A4: branchdeg v = 2 by A1,A2,Def4;
then
A5: v^<*0*> in dom p by Th2;
v^<*1*> in dom p by A4,Th2;
hence thesis by A3,A5;
end;
theorem
(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]
proof
A1: v is correct by Def12;
assume
A2: (p.v)`2 = 4;
then
A3: ex T,X,Y,x,y,z st (p.v)`1 = [X^T^<*y\x*>^Y,z] &
(p.(v^<*0*>))`1 = [T,y] & (p.(v^<*1*>))`1 = [X^<*x*>^Y,z] by A1,Def4;
A4: branchdeg v = 2 by A1,A2,Def4;
then
A5: v^<*0*> in dom p by Th2;
v^<*1*> in dom p by A4,Th2;
hence thesis by A3,A5;
end;
theorem
(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]
proof
A1: v is correct by Def12;
assume
A2: (p.v)`2 = 5;
then
A3: ex X,x,y,Y st (p.v)`1 = [X^<*x*y*>^Y,z] & (p.(v^<*0*>))`1 =
[X^<*x*>^<*y*>^Y,z] by A1,Def4;
branchdeg v = 1 by A1,A2,Def4;
then v^<*0*> in dom p by Th1;
hence thesis by A3;
end;
theorem
(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]
proof
A1: v is correct by Def12;
assume
A2: (p.v)`2 = 6;
then
A3: ex X,Y,x,y st (p.v)`1 = [X^Y,x*y] & (p.(v^<*0*>))`1 = [X,x] &
(p.(v^<*1*>))`1 = [Y,y] by A1,Def4;
A4: branchdeg v = 2 by A1,A2,Def4;
then
A5: v^<*0*> in dom p by Th2;
v^<*1*> in dom p by A4,Th2;
hence thesis by A3,A5;
end;
theorem Th10:
(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]
proof
A1: v is correct by Def12;
assume
A2: (p.v)`2 = 7;
then
A3: ex T,X,Y,y,z st (p.v)`1 = [X^T^Y,z] & (p.(v^<*0*>))`1 = [T,y] &
(p.(v^<*1*>))`1 = [X^<*y*>^Y,z] by A1,Def4;
A4: branchdeg v = 2 by A1,A2,Def4;
then
A5: v^<*0*> in dom p by Th2;
v^<*1*> in dom p by A4,Th2;
hence thesis by A3,A5;
end;
theorem
(p.v)`2 = 0 or ... or (p.v)`2 = 7
proof
v is correct by Def12;
hence thesis by Def4;
end;
definition
let s;
let IT be PreProof of s;
attr IT is cut-free means
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
for x holds it.x = card dom repr_of x;
existence
proof
deffunc F(type of s) = card dom repr_of $1;
thus ex S be Function of the carrier of s, NAT st
for x holds S.x = F(x) from FUNCT_2:sch 4;
end;
uniqueness
proof
let f,g be Function of the carrier of s, NAT;
deffunc F(type of s) = card dom repr_of $1;
assume that
A1: f.x = F(x) and
A2: g.x = F(x);
now
let c be Element of s;
thus f.c = F(c) by A1
.= g.c by A2;
end;
hence f = g by FUNCT_2:63;
end;
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;
coherence
proof
A1: f*T is FinSequence of NAT by FINSEQ_2:32;
rng (f*T) c= REAL;
hence thesis by A1,FINSEQ_1:def 4;
end;
end;
Lm1: for D being non empty set, T being FinSequence of D
for f being Function of D, NAT holds Sum(f*T) is Nat
proof
let D be non empty set, T be FinSequence of D;
let f be Function of D, NAT;
defpred P[FinSequence of REAL] means
$1 is FinSequence of NAT implies Sum $1 is Nat;
A1: P[<*>REAL] by RVSUM_1:72;
A2: for p be FinSequence of REAL, x be Element of REAL
st P[p] holds P[p^<*x*>]
proof
let p be FinSequence of REAL, x be Element of REAL;
assume
A3: P[p];
assume p^<*x*> is FinSequence of NAT;
then
A4: rng (p^<*x*>) c= NAT by FINSEQ_1:def 4;
rng p c= rng (p^<*x*>) by FINSEQ_1:29;
then
A5: rng p c= NAT by A4;
rng <*x*> c= rng (p^<*x*>) by FINSEQ_1:30;
then
A6: rng <*x*> c= NAT by A4;
rng <*x*> = {x} by FINSEQ_1:38;
then reconsider n=x as Element of NAT by A6,ZFMISC_1:31;
reconsider s = Sum p as Nat by A3,A5,FINSEQ_1:def 4;
Sum(p^<*x*>) = s + n by RVSUM_1:74;
hence thesis;
end;
A7: for p being FinSequence of REAL holds P[p] from FINSEQ_2:sch 2(A1,A2);
f*T is FinSequence of NAT by FINSEQ_2:32;
hence thesis by A7;
end;
definition
let s;
let p be Proof of s;
func cutdeg p -> Nat means
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;
existence
proof
thus (p.{})`2 = 7 implies ex r being Nat st
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] & r = (size_w.r.t. s).y + (size_w.r.t. s).z
+ Sum((size_w.r.t. s)*(X^T^Y))
proof
A1: {}^<*0*> = <*0*> by FINSEQ_1:34;
A2: {}^<*1*> = <*1*> by FINSEQ_1:34;
reconsider v = {} as Element of dom p by TREES_1:22;
assume (p.{})`2 = 7;
then consider w,u being Element of dom p, T,X,Y,y,z such that
A3: w = v^<*0*> and
A4: u = v^<*1*> and
A5: (p.v)`1 = [X^T^Y,z] and
A6: (p.w)`1 = [T,y] and
A7: (p.u)`1 = [X^<*y*>^Y,z] by Th10;
reconsider a = Sum((size_w.r.t. s)*(X^T^Y)) as Nat by Lm1;
reconsider tt = (size_w.r.t. s).y + (size_w.r.t. s).z + a
as Nat;
take tt;
thus thesis by A1,A2,A3,A4,A5,A6,A7;
end;
thus thesis;
end;
uniqueness
proof
let r1,r2 be Nat;
thus (p.{})`2 = 7 &
(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] & r1 = (size_w.r.t. s).y + (size_w.r.t. s).z
+ Sum((size_w.r.t. s)*(X^T^Y)))
& (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] & r2 = (size_w.r.t. s).y + (size_w.r.t. s).z
+ Sum((size_w.r.t. s)*(X^T^Y))) implies r1 = r2
proof
assume (p.{})`2 = 7;
given T,X,Y,y,z such that
A8: (p.{})`1 = [X^T^Y,z] and
A9: (p.<*0*>)`1 = [T,y] and (p.<*1*>)`1 = [X^<*y*>^Y,z] and
A10: r1 = (size_w.r.t. s).y + (size_w.r.t. s).z + Sum((size_w.r.t. s)*(X
^T^Y));
given T9,X9,Y9,y9,z9 such that
A11: (p.{})`1 = [X9^T9^Y9,z9] and
A12: (p.<*0*>)`1 = [T9,y9] and (p.<*1*>)`1 = [X9^<*y9*>^Y9,z9] and
A13: r2 = (size_w.r.t. s).y9 + (size_w.r.t. s).z9 + Sum((size_w.r.t. s)*
(X9^T9^Y9));
A14: X^T^Y = [X^T^Y,z]`1
.= [X9^T9^Y9,z9]`1 by A8,A11
.= X9^T9^Y9;
A15: y = [T,y]`2
.= [T9,y9]`2 by A9,A12
.= y9;
z = [X^T^Y,z]`2
.= [X9^T9^Y9,z9]`2 by A8,A11
.= z9;
hence thesis by A10,A13,A14,A15;
end;
thus thesis;
end;
consistency;
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
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 };
existence
proof
{} in A* by FINSEQ_1:49;
then {{}} c= A* by ZFMISC_1:31;
then reconsider f = (the carrier of s) --> {{}}
as Function of the carrier of s, bool (A*) by FUNCOP_1:45;
A1: for t being set st t in f.x holds t = {}
proof
let t be set;
assume t in f.x;
then t in {{}} by FUNCOP_1:7;
hence thesis by TARSKI:def 1;
end;
A2: {} in f.x
proof
f.x = {{}} by FUNCOP_1:7;
hence thesis by TARSKI:def 1;
end;
A3: {} is Element of A* by FINSEQ_1:49;
take f;
let x,y;
thus f.(x*y) = { a ^ b : a in f.x & b in f.y }
proof
thus f.(x*y) c= { a ^ b : a in f.x & b in f.y }
proof
let t be object;
assume t in f.(x*y);
then
A4: t = {} by A1;
A5: t = {}^{} by A4;
A6: {} in f.x by A2;
{} in f.y by A2;
hence thesis by A5,A6;
end;
let t be object;
assume t in { a ^ b : a in f.x & b in f.y };
then consider a,b such that
A7: t = a ^ b and
A8: a in f.x and
A9: b in f.y;
A10: a = {} by A1,A8;
b = {} by A1,A9;
then a ^ b = {} by A10,FINSEQ_1:34;
hence thesis by A2,A7;
end;
thus f.(x/"y) = { a : for b st b in f.y holds a ^ b in f.x }
proof
thus f.(x/"y) c= { a : for b st b in f.y holds a ^ b in f.x }
proof
let t be object;
assume t in f.(x/"y);
then
A11: t = {} by A1;
now
let b;
assume b in f.y;
then b = {} by A1;
then {} ^ b = {} by FINSEQ_1:34;
hence {} ^ b in f.x by A2;
end;
hence thesis by A3,A11;
end;
let t be object;
assume t in { a : for b st b in f.y holds a ^ b in f.x };
then consider a such that
A12: t = a and
A13: for b st b in f.y holds a ^ b in f.x;
{} in f.y by A2;
then a ^ {} in f.x by A13;
then a = {} by A1;
hence thesis by A2,A12;
end;
thus f.(y\x) = { a : for b st b in f.y holds b ^ a in f.x }
proof
thus f.(y\x) c= { a : for b st b in f.y holds b ^ a in f.x }
proof
let t be object;
assume t in f.(y\x);
then
A14: t = {} by A1;
now
let b;
assume b in f.y;
then b = {} by A1;
then b ^ {} = {} by FINSEQ_1:34;
hence b ^ {} in f.x by A2;
end;
hence thesis by A3,A14;
end;
let t be object;
assume t in { a : for b st b in f.y holds b ^ a in f.x };
then consider a such that
A15: t = a and
A16: for b st b in f.y holds b ^ a in f.x;
{} in f.y by A2;
then {} ^ a in f.x by A16;
then a = {} by A1;
hence thesis by A2,A15;
end;
end;
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;
existence
proof
set l = the BinOp of {{}},d = the Relation of {{}}*,{{}};
take typestr(#{{}},l,l,l,d#);
thus the carrier of typestr(#{{}},l,l,l,d#) is non empty;
thus thesis;
end;
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
[f,x] in the derivability of s;
end;
definition
let IT be non empty typestr;
attr IT is SynTypes_Calculus-like means
:Def18:
(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;
existence
proof
[:{0}*,{0}:] c= [:{0}*,{0}:];
then reconsider DER = [:{0}*,{0}:] as non empty Relation of {0}*,{0};
reconsider EM = typestr (#{0},op2,op2,op2,DER#) as non empty typestr;
take EM;
thus for x being type of EM holds <*x*> ==>. x;
thus thesis;
end;
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;
deffunc e(typestr) = <*>the carrier of $1;
Lm2: T ==>. y & X^<*x*> ==>. z implies X^<*x/"y*>^T ==>. z
proof
assume that
A1: T ==>. y and
A2: X^<*x*> ==>. z;
X^<*x*>^e(s) ==>. z by A2,FINSEQ_1:34;
then X^<*x/"y*>^T^e(s) ==>. z by A1,Def18;
hence thesis by FINSEQ_1:34;
end;
Lm3: T ==>. y & <*x*>^Y ==>. z implies <*x/"y*>^T^Y ==>. z
proof
assume that
A1: T ==>. y and
A2: <*x*>^Y ==>. z;
e(s)^<*x*>^Y ==>. z by A2,FINSEQ_1:34;
then e(s)^<*x/"y*>^T^Y ==>. z by A1,Def18;
hence thesis by FINSEQ_1:34;
end;
Lm4: T ==>. y & <*x*> ==>. z implies <*x/"y*>^T ==>. z
proof
assume that
A1: T ==>. y and
A2: <*x*> ==>. z;
e(s)^<*x*> ==>. z by A2,FINSEQ_1:34;
then e(s)^<*x/"y*>^T ==>. z by A1,Lm2;
hence thesis by FINSEQ_1:34;
end;
Lm5: T ==>. y & X^<*x*> ==>. z implies X^T^<*y\x*> ==>. z
proof
assume that
A1: T ==>. y and
A2: X^<*x*> ==>. z;
X^<*x*>^e(s) ==>. z by A2,FINSEQ_1:34;
then X^T^<*y\x*>^e(s) ==>. z by A1,Def18;
hence thesis by FINSEQ_1:34;
end;
Lm6: T ==>. y & <*x*>^Y ==>. z implies T^<*y\x*>^Y ==>. z
proof
assume that
A1: T ==>. y and
A2: <*x*>^Y ==>. z;
e(s)^<*x*>^Y ==>. z by A2,FINSEQ_1:34;
then e(s)^T^<*y\x*>^Y ==>. z by A1,Def18;
hence thesis by FINSEQ_1:34;
end;
Lm7: T ==>. y & <*x*> ==>. z implies T^<*y\x*> ==>. z
proof
assume that
A1: T ==>. y and
A2: <*x*> ==>. z;
e(s)^<*x*> ==>. z by A2,FINSEQ_1:34;
then e(s)^T^<*y\x*> ==>. z by A1,Lm5;
hence thesis by FINSEQ_1:34;
end;
Lm8: <*x*>^<*y*>^Y ==>. z implies <*x*y*>^Y ==>. z
proof
assume <*x*>^<*y*>^Y ==>. z;
then e(s)^<*x*>^<*y*>^Y ==>. z by FINSEQ_1:34;
then e(s)^<*x*y*>^Y ==>. z by Def18;
hence thesis by FINSEQ_1:34;
end;
Lm9: X^<*x*>^<*y*> ==>. z implies X^<*x*y*> ==>. z
proof
assume X^<*x*>^<*y*> ==>. z;
then X^<*x*>^<*y*>^e(s) ==>. z by FINSEQ_1:34;
then X^<*x*y*>^e(s) ==>. z by Def18;
hence thesis by FINSEQ_1:34;
end;
Lm10: <*x*>^<*y*> ==>. z implies <*x*y*> ==>. z
proof
assume <*x*>^<*y*> ==>. z;
then e(s)^<*x*>^<*y*> ==>. z by FINSEQ_1:34;
then e(s)^<*x*y*> ==>. z by Lm9;
hence thesis by FINSEQ_1:34;
end;
theorem Th12:
<*x/"y*>^<*y*> ==>. x & <*y*>^<*y\x*> ==>. x
proof
A1: <*x*> ==>. x by Def18;
<*y*> ==>. y by Def18;
hence thesis by A1,Lm4,Lm7;
end;
theorem Th13:
<*x*> ==>. y/"(x\y) & <*x*> ==>. (y/"x)\y
proof
A1: <*y/"x*>^<*x*> ==>. y by Th12;
<*x*>^<*x\y*> ==>. y by Th12;
hence thesis by A1,Def18;
end;
theorem Th14:
<*x/"y*> ==>. (x/"z)/"(y/"z)
proof
A1: <*x/"y*>^<*y*> ==>. x by Th12;
<*z*> ==>. z by Def18;
then <*x/"y*>^<*y/"z*>^<*z*> ==>. x by A1,Lm2;
then <*x/"y*>^<*y/"z*> ==>. x/"z by Def18;
hence thesis by Def18;
end;
theorem Th15:
<*y\x*> ==>. (z\y)\(z\x)
proof
A1: <*y*>^<*y\x*> ==>. x by Th12;
<*z*> ==>. z by Def18;
then <*z*>^<*z\y*>^<*y\x*> ==>. x by A1,Lm6;
then <*z*>^(<*z\y*>^<*y\x*>) ==>. x by FINSEQ_1:32;
then <*z\y*>^<*y\x*> ==>. z\x by Def18;
hence thesis by Def18;
end;
theorem
<*x*> ==>. y implies <*x/"z*> ==>. y/"z & <*z\x*> ==>. z\y
proof
assume
A1: <*x*> ==>. y;
A2: <*z*> ==>. z by Def18;
then
A3: <*x/"z*>^<*z*> ==>. y by A1,Lm4;
<*z*>^<*z\x*> ==>. y by A1,A2,Lm7;
hence thesis by A3,Def18;
end;
theorem Th17:
<*x*> ==>. y implies <*z/"y*> ==>. z/"x & <*y\z*> ==>. x\z
proof
assume
A1: <*x*> ==>. y;
A2: <*z*> ==>. z by Def18;
then
A3: <*z/"y*>^<*x*> ==>. z by A1,Lm4;
<*x*>^<*y\z*> ==>. z by A1,A2,Lm7;
hence thesis by A3,Def18;
end;
theorem Th18:
<*y/"((y/"x)\y)*> ==>. y/"x
proof
<*x*> ==>. (y/"x)\y by Th13;
hence thesis by Th17;
end;
theorem Th19:
<*x*> ==>. y implies
<*>the carrier of s ==>. y/"x & <*>the carrier of s ==>. x\y
proof
assume
A1: <*x*> ==>. y;
A2: e(s)^<*x*> = <*x*> by FINSEQ_1:34;
<*x*>^e(s) = <*x*> by FINSEQ_1:34;
hence thesis by A1,A2,Def18;
end;
theorem Th20:
<*>the carrier of s ==>. x/"x & <*>the carrier of s ==>. x\x
proof
<*x*> ==>. x by Def18;
hence thesis by Th19;
end;
theorem
<*>the carrier of s ==>. (y/"(x\y))/"x &
<*>the carrier of s ==>. x\((y/"x)\ y )
proof
A1: <*x*> ==>. y/"(x\y) by Th13;
<*x*> ==>. (y/"x)\y by Th13;
hence thesis by A1,Th19;
end;
theorem
<*>the carrier of s ==>. ((x/"z)/"(y/"z))/"(x/"y) &
<*>the carrier of s ==>. (y\x)\((z\y)\(z\x))
proof
A1: <*x/"y*> ==>. (x/"z)/"(y/"z) by Th14;
<*y\x*> ==>. (z\y)\(z\x) by Th15;
hence thesis by A1,Th19;
end;
theorem
<*>the carrier of s ==>. x implies
<*>the carrier of s ==>. y/"(y/"x) & <*>the carrier of s ==>. (x\y)\y
proof
A1: <*y*> ==>. y by Def18;
then
A2: e(s)^<*y*> ==>. y by FINSEQ_1:34;
A3: <*y*>^e(s) ==>. y by A1,FINSEQ_1:34;
assume
A4: e(s) ==>. x;
then
A5: e(s)^<*y/"x*>^e(s) ==>. y by A2,Lm2;
A6: e(s)^<*x\y*>^e(s) ==>. y by A3,A4,Lm6;
A7: e(s)^<*y/"x*> ==>. y by A5,FINSEQ_1:34;
<*x\y*>^e(s) ==>. y by A6,FINSEQ_1:34;
hence thesis by A7,Def18;
end;
theorem
<*x/"(y/"y)*> ==>. x
proof
<*x*> ==>. x by Def18;
then <*x/"(y/"y)*>^e(s) ==>. x by Lm4,Th20;
hence thesis by FINSEQ_1:34;
end;
definition
let s,x,y;
pred x <==>. y means
<*x*> ==>. y & <*y*> ==>. x;
reflexivity by Def18;
symmetry;
end;
theorem
x/"y <==>. x/"((x/"y)\x)
by Th13,Th18;
theorem
x/"(z*y) <==>. (x/"y)/"z
proof
A1: <*z*> ==>. z by Def18;
A2: <*y*> ==>. y by Def18;
A3: <*x*> ==>. x by Def18;
<*z*>^<*y*> ==>. z*y by A1,A2,Def18;
then <*x/"(z*y)*>^(<*z*>^<*y*>) ==>. x by A3,Lm4;
then <*x/"(z*y)*>^<*z*>^<*y*> ==>. x by FINSEQ_1:32;
then <*x/"(z*y)*>^<*z*> ==>. x/"y by Def18;
then
A4: <*x/"(z*y)*> ==>. (x/"y)/"z by Def18;
<*x/"y*>^<*y*> ==>. x by A2,A3,Lm4;
then <*(x/"y)/"z*>^<*z*>^<*y*> ==>. x by A1,Lm3;
then <*(x/"y)/"z*>^<*z*y*> ==>. x by Lm9;
then <*(x/"y)/"z*> ==>. x/"(z*y) by Def18;
hence thesis by A4;
end;
theorem
<*x*(y/"z)*> ==>. (x*y)/"z :: and analogously <*z\y*x*> > z\(y*x)
proof
A1: <*x*> ==>. x by Def18;
<*y*> ==>. y by Def18; then
A2: <*x*>^<*y*> ==>. x*y by A1,Def18;
<*z*> ==>. z by Def18;
then <*x*>^<*y/"z*>^<*z*> ==>. x*y by A2,Lm2;
then <*x*(y/"z)*>^<*z*> ==>. x*y by Lm8;
hence thesis by Def18;
end;
theorem
<*x*> ==>. (x*y)/"y & <*x*> ==>. y\(y*x)
proof
A1: <*x*> ==>.x by Def18;
A2: <*y*> ==>.y by Def18;
then
A3: <*x*>^<*y*> ==>. x*y by A1,Def18;
<*y*>^<*x*> ==>. y*x by A1,A2,Def18;
hence thesis by A3,Def18;
end;
theorem
x*y*z <==>. x*(y*z)
proof
A1: <*x*> ==>. x by Def18;
A2: <*y*> ==>. y by Def18;
A3: <*z*> ==>. z by Def18;
<*x*>^<*y*> ==>. x*y by A1,A2,Def18;
then <*x*>^<*y*>^<*z*> ==>. (x*y)*z by A3,Def18;
then <*x*>^<*y*z*> ==>. (x*y)*z by Lm9;
then
A4: <*x*(y*z)*> ==>. (x*y)*z by Lm10;
<*y*>^<*z*> ==>. y*z by A2,A3,Def18;
then <*x*>^(<*y*>^<*z*>) ==>. x*(y*z) by A1,Def18;
then <*x*>^<*y*>^<*z*> ==>. x*(y*z) by FINSEQ_1:32;
then <*x*y*>^<*z*> ==>. x*(y*z) by Lm8;
then <*x*y*z*> ==>. x*(y*z) by Lm10;
hence thesis by A4;
end;