:: Propositional Calculus for Boolean Valued Functions, I
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999-2026 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, SUBSET_1, MARGREL1, BVFUNC_1, XBOOLEAN, FUNCT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1, FUNCT_1,
FUNCT_2, BVFUNC_1;
constructors BVFUNC_1, NUMBERS;
registrations XBOOLEAN, MARGREL1;
requirements NUMERALS;
definitions FUNCT_2;
equalities XBOOLEAN;
theorems MARGREL1, BINARITH, BVFUNC_1, XBOOLEAN;
begin
::Chap. 1 Propositional Calculus
reserve Y for non empty set;
theorem
for a,b being Function of Y,BOOLEAN holds a=I_el(Y) & b=I_el(Y)
iff (a '&' b)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
now
assume
A1: a '&' b=I_el(Y);
per cases;
suppose
a=I_el(Y) & b=I_el(Y);
hence a=I_el(Y) & b=I_el(Y);
end;
suppose
a=I_el(Y) & b<>I_el(Y);
hence a=I_el(Y) & b=I_el(Y) by A1,BVFUNC_1:6;
end;
suppose
a<>I_el(Y) & b=I_el(Y);
hence a=I_el(Y) & b=I_el(Y) by A1,BVFUNC_1:6;
end;
suppose
A2: a<>I_el(Y) & b<>I_el(Y);
for x being Element of Y holds a.x=TRUE
proof
let x be Element of Y;
(a '&' b).x=TRUE by A1,BVFUNC_1:def 11;
then a.x '&' b.x=TRUE by MARGREL1:def 20;
hence thesis by MARGREL1:12;
end;
hence a=I_el(Y) & b=I_el(Y) by A2,BVFUNC_1:def 11;
end;
end;
hence thesis;
end;
theorem Th2:
for b being Function of Y,BOOLEAN st (I_el(Y) 'imp' b)=I_el
(Y) holds b=I_el(Y)
proof
set a=I_el(Y);
let b be Function of Y,BOOLEAN;
assume
A1: a 'imp' b=I_el(Y);
for x being Element of Y holds b.x=TRUE
proof
let x be Element of Y;
(a 'imp' b).x=TRUE by A1,BVFUNC_1:def 11;
then a.x=TRUE & ('not' a.x) 'or' b.x=TRUE by BVFUNC_1:def 8,def 11;
then FALSE 'or' b.x=TRUE by MARGREL1:11;
hence thesis by BINARITH:3;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN st a=I_el(Y) holds (a 'or' b
)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
assume
A1: a=I_el(Y);
for x being Element of Y holds (a 'or' b).x=TRUE
proof
let x be Element of Y;
a.x=TRUE by A1,BVFUNC_1:def 11;
then (a 'or' b).x =TRUE 'or' b.x by BVFUNC_1:def 4
.=TRUE by BINARITH:10;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN st b=I_el(Y) holds (a 'imp'
b)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
assume
A1: b=I_el(Y);
for x being Element of Y holds (a 'imp' b).x=TRUE
proof
let x be Element of Y;
b.x=TRUE by A1,BVFUNC_1:def 11;
then (a 'imp' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8
.=TRUE by BINARITH:10;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN st ('not' a)=I_el(Y) holds (
a 'imp' b)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
assume
A1: 'not' a=I_el(Y);
for x being Element of Y holds (a 'imp' b).x=TRUE
proof
let x be Element of Y;
('not' a).x=TRUE by A1,BVFUNC_1:def 11;
then 'not' a.x=TRUE by MARGREL1:def 19;
then (a 'imp' b).x =TRUE 'or' b.x by BVFUNC_1:def 8
.=TRUE by BINARITH:10;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a being Function of Y,BOOLEAN holds 'not' (a '&' 'not' a)= I_el(Y)
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
thus ('not' (a '&' 'not' a)).x = 'not' (a '&' 'not' a).x by MARGREL1:def 19
.= 'not' (a.x '&' ('not' a).x) by MARGREL1:def 20
.= 'not' (a.x '&' 'not' a.x) by MARGREL1:def 19
.= TRUE by XBOOLEAN:102
.= I_el(Y).x by BVFUNC_1:def 11;
end;
theorem :: Identity law
for a being Function of Y,BOOLEAN holds a 'imp' a = I_el Y
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
A1: (a 'imp' a).x = ('not' a.x) 'or' a.x & (I_el Y).x=TRUE by BVFUNC_1:def 8
,def 11;
A2: 'not' FALSE=TRUE by MARGREL1:11;
now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence thesis by A1,BINARITH:10;
end;
case
a.x=FALSE;
hence thesis by A2,A1,BINARITH:10;
end;
end;
hence thesis;
end;
theorem
for a,b being Function of Y,BOOLEAN holds (a 'imp' b)=I_el(Y)
iff ('not' b 'imp' 'not' a)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
A1: now
assume
A2: ('not' b 'imp' 'not' a)=I_el(Y);
for x being Element of Y holds (a 'imp' b).x=TRUE
proof
let x be Element of Y;
('not' b 'imp' 'not' a).x=TRUE by A2,BVFUNC_1:def 11;
then ('not' ('not' b).x) 'or' ('not' a).x=TRUE by BVFUNC_1:def 8;
then ('not' 'not' b.x) 'or' ('not' a).x=TRUE by MARGREL1:def 19;
then
A3: ('not' 'not' b.x) 'or' 'not' a.x=TRUE by MARGREL1:def 19;
A4: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3;
now
per cases by A3,A4,BINARITH:3;
case
('not' a.x)=TRUE;
then (a 'imp' b).x =TRUE 'or' b.x by BVFUNC_1:def 8
.=TRUE by BINARITH:10;
hence thesis;
end;
case
b.x=TRUE;
then (a 'imp' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8
.=TRUE by BINARITH:10;
hence thesis;
end;
end;
hence thesis;
end;
hence a 'imp' b=I_el(Y) by BVFUNC_1:def 11;
end;
now
assume
A5: (a 'imp' b)=I_el(Y);
for x being Element of Y holds ('not' b 'imp' 'not' a).x=TRUE
proof
let x be Element of Y;
(a 'imp' b).x=TRUE by A5,BVFUNC_1:def 11;
then
A6: ('not' a.x) 'or' b.x=TRUE by BVFUNC_1:def 8;
A7: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3;
now
per cases by A6,A7,BINARITH:3;
case
A8: ('not' a.x)=TRUE;
('not' b 'imp' 'not' a).x =('not' ('not' b).x) 'or' ('not' a).x
by BVFUNC_1:def 8
.=('not' ('not' b).x) 'or' TRUE by A8,MARGREL1:def 19
.=TRUE by BINARITH:10;
hence thesis;
end;
case
A9: b.x=TRUE;
('not' b).x='not' b.x by MARGREL1:def 19;
then ('not' b 'imp' 'not' a).x =('not' 'not' b.x) 'or' ('not' a).x
by BVFUNC_1:def 8
.=TRUE by A9,BINARITH:10;
hence thesis;
end;
end;
hence thesis;
end;
hence 'not' b 'imp' 'not' a=I_el(Y) by BVFUNC_1:def 11;
end;
hence thesis by A1;
end;
theorem
for a,b,c being Function of Y,BOOLEAN st (a 'imp' b)=I_el(Y) & (
b 'imp' c)=I_el(Y) holds (a 'imp' c)=I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
assume that
A1: (a 'imp' b)=I_el(Y) and
A2: (b 'imp' c)=I_el(Y);
for x being Element of Y holds (a 'imp' c).x=TRUE
proof
let x be Element of Y;
A3: ('not' b.x)=TRUE or ('not' b.x)=FALSE by XBOOLEAN:def 3;
A4: (a 'imp' c).x=('not' a.x) 'or' c.x by BVFUNC_1:def 8;
(b 'imp' c).x=TRUE by A2,BVFUNC_1:def 11;
then
A5: ('not' b.x) 'or' c.x=TRUE by BVFUNC_1:def 8;
(a 'imp' b).x=TRUE by A1,BVFUNC_1:def 11;
then
A6: ('not' a.x) 'or' b.x=TRUE by BVFUNC_1:def 8;
A7: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3;
now
per cases by A6,A7,A5,A3,BINARITH:3;
case
('not' a.x)=TRUE & ('not' b.x)=TRUE;
hence thesis by A4,BINARITH:10;
end;
case
('not' a.x)=TRUE & c.x=TRUE;
hence thesis by A4;
end;
case
b.x=TRUE & ('not' b.x)=TRUE;
hence thesis by MARGREL1:11;
end;
case
b.x=TRUE & c.x=TRUE;
hence thesis by A4,BINARITH:10;
end;
end;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN st (a 'imp' b)=I_el(Y) & (a
'imp' 'not' b)=I_el(Y) holds 'not' a=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
assume that
A1: (a 'imp' b)=I_el(Y) and
A2: (a 'imp' 'not' b)=I_el(Y);
for x being Element of Y holds ('not' a).x=TRUE
proof
let x be Element of Y;
(a 'imp' b).x=TRUE by A1,BVFUNC_1:def 11;
then
A3: ('not' a.x) 'or' b.x=TRUE by BVFUNC_1:def 8;
(a 'imp' 'not' b).x=TRUE by A2,BVFUNC_1:def 11;
then
A4: ('not' a.x) 'or' ('not' b).x=TRUE by BVFUNC_1:def 8;
A5: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3;
now
per cases by A3,A5,A4,BINARITH:3;
case
('not' a.x)=TRUE & ('not' a.x)=TRUE;
hence thesis by MARGREL1:def 19;
end;
case
('not' a.x)=TRUE & ('not' b).x=TRUE;
hence thesis by MARGREL1:def 19;
end;
case
b.x=TRUE & ('not' a.x)=TRUE;
hence thesis by MARGREL1:def 19;
end;
case
A6: b.x=TRUE & ('not' b).x=TRUE;
then 'not' b.x=TRUE by MARGREL1:def 19;
hence thesis by A6,MARGREL1:11;
end;
end;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a being Function of Y,BOOLEAN holds ('not' a 'imp' a) 'imp'
a = I_el(Y)
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
A1: 'not' ('not' ('not' a).x 'or' a.x) = 'not' (a.x 'or' a.x) by
MARGREL1:def 19
.= 'not' a.x;
A2: ('not' a 'imp' a 'imp' a).x =('not' ('not' a 'imp' a).x) 'or' a.x by
BVFUNC_1:def 8
.='not' a.x 'or' a.x by A1,BVFUNC_1:def 8;
A3: (I_el Y).x=TRUE by BVFUNC_1:def 11;
now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence thesis by A2,A3,BINARITH:10;
end;
case
a.x=FALSE;
then ('not' a 'imp' a 'imp' a).x =TRUE 'or' FALSE by A2,MARGREL1:11
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
end;
hence thesis;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (
'not' (b '&' c) 'imp' 'not' (a '&' c)) =I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
let x be Element of Y;
A1: ((a 'imp' b) 'imp' ('not' (b '&' c) 'imp' 'not' (a '&' c))).x = 'not'
(a 'imp' b).x 'or' ('not' (b '&' c) 'imp' 'not' (a '&' c)).x by BVFUNC_1:def 8
.= 'not' (a 'imp' b).x 'or' (('not' ('not' (b '&' c)).x) 'or' ('not' (
a '&' c)).x) by BVFUNC_1:def 8;
A2: ('not' (a '&' c)).x =(('not' a) 'or' ('not' c)).x by BVFUNC_1:14
.=('not' a).x 'or' ('not' c).x by BVFUNC_1:def 4
.='not' a.x 'or' ('not' c).x by MARGREL1:def 19
.='not' a.x 'or' 'not' c.x by MARGREL1:def 19;
now
per cases by XBOOLEAN:def 3;
case
c.x=TRUE;
hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10;
end;
case
c.x=FALSE;
then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' c.x 'or' c.x)=TRUE;
end;
end;
then ('not' a.x 'or' ('not' c.x 'or' c.x)) =TRUE by BINARITH:10;
then
A3: (('not' a.x 'or' 'not' c.x) 'or' b.x) '&' ('not' a.x 'or' ('not' c.x
'or' c.x)) = (('not' a.x 'or' 'not' c.x) 'or' b.x) by MARGREL1:14;
A4: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
A5: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
'not' ('not' (b '&' c)).x ='not' 'not' (b '&' c).x by MARGREL1:def 19
.=b.x '&' c.x by MARGREL1:def 20;
then
A6: ('not' ('not' (b '&' c)).x) 'or' ('not' (a '&' c)).x =(('not' a.x 'or'
'not' c.x) 'or' b.x) '&' (('not' a.x 'or' 'not' c.x) 'or' c.x) by A2,
XBOOLEAN:9
.=(('not' a.x 'or' 'not' c.x) 'or' b.x) '&' ('not' a.x 'or' ('not' c.x
'or' c.x)) by BINARITH:11;
'not' (a 'imp' b).x ='not' (('not' a.x) 'or' b.x) by BVFUNC_1:def 8
.=a.x '&' 'not' b.x;
then 'not' (a 'imp' b).x 'or' (('not' ('not' (b '&' c)).x) 'or' ('not' (a
'&' c)).x) =((('not' a.x 'or' 'not' c.x) 'or' b.x) 'or' a.x) '&' ((('not' a.x
'or' 'not' c.x) 'or' b.x) 'or' 'not' b.x) by A6,A3,XBOOLEAN:9
.=((('not' a.x 'or' 'not' c.x) 'or' b.x) 'or' a.x) '&' (('not' a.x
'or' 'not' c.x) 'or' (b.x 'or' 'not' b.x)) by BINARITH:11
.=((('not' c.x 'or' 'not' a.x) 'or' a.x) 'or' b.x) '&' (('not' a.x
'or' 'not' c.x) 'or' (b.x 'or' 'not' b.x)) by BINARITH:11
.=(('not' c.x 'or' ('not' a.x 'or' a.x)) 'or' b.x) '&' (('not' a.x
'or' 'not' c.x) 'or' (b.x 'or' 'not' b.x)) by BINARITH:11;
then 'not' (a 'imp' b).x 'or' (('not' ('not' (b '&' c)).x) 'or' ('not' (a
'&' c)).x) =(TRUE 'or' b.x) '&' (('not' a.x 'or' 'not' c.x) 'or' TRUE) by
A4,A5,BINARITH:10
.=TRUE '&' (('not' a.x 'or' 'not' c.x) 'or' TRUE) by BINARITH:10
.=TRUE '&' TRUE by BINARITH:10
.=TRUE;
hence thesis by A1,BVFUNC_1:def 11;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((
b 'imp' c) 'imp' (a 'imp' c))=I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
let x be Element of Y;
A1: ((a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c))).x =('not' (a 'imp'
b).x) 'or' ((b 'imp' c) 'imp' (a 'imp' c)).x by BVFUNC_1:def 8
.=('not' (a 'imp' b).x) 'or' ('not' (b 'imp' c).x 'or' (a 'imp' c).x)
by BVFUNC_1:def 8;
A2: 'not' (b 'imp' c).x ='not' ('not' b.x 'or' c.x) by BVFUNC_1:def 8
.=b.x '&' 'not' c.x;
A3: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
A4: (a 'imp' c).x ='not' a.x 'or' c.x by BVFUNC_1:def 8;
A5: now
per cases by XBOOLEAN:def 3;
case
c.x=TRUE;
hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10;
end;
case
c.x=FALSE;
then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' c.x 'or' c.x)=TRUE;
end;
end;
A6: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
'not' (a 'imp' b).x ='not' ('not' a.x 'or' b.x) by BVFUNC_1:def 8
.=a.x '&' 'not' b.x;
then ('not' (a 'imp' b).x) 'or' ('not' (b 'imp' c).x 'or' (a 'imp' c).x )
=(((b.x '&' 'not' c.x) 'or' ('not' a.x 'or' c.x)) 'or' a.x) '&' (((b.x '&'
'not' c.x) 'or' ('not' a.x 'or' c.x)) 'or' 'not' b.x) by A2,A4,XBOOLEAN:9
.=((b.x '&' 'not' c.x) 'or' ((c.x 'or' 'not' a.x) 'or' a.x)) '&' (((b.
x '&' 'not' c.x) 'or' ('not' a.x 'or' c.x)) 'or' 'not' b.x) by BINARITH:11
.=((b.x '&' 'not' c.x) 'or' (c.x 'or' ('not' a.x 'or' a.x))) '&' (((
'not' a.x 'or' c.x) 'or' (b.x '&' 'not' c.x)) 'or' 'not' b.x) by BINARITH:11
.=((b.x '&' 'not' c.x) 'or' (c.x 'or' ('not' a.x 'or' a.x))) '&' ((
'not' a.x 'or' c.x) 'or' (('not' c.x '&' b.x) 'or' 'not' b.x)) by BINARITH:11
.=((b.x '&' 'not' c.x) 'or' (c.x 'or' ('not' a.x 'or' a.x))) '&' ((
'not' a.x 'or' c.x) 'or' (('not' b.x 'or' 'not' c.x) '&' ('not' b.x 'or' b.x)))
by XBOOLEAN:9
.=((b.x '&' 'not' c.x) 'or' TRUE) '&' (('not' a.x 'or' c.x) 'or' ((
'not' b.x 'or' 'not' c.x) '&' TRUE)) by A3,A6,BINARITH:10
.=TRUE '&' (('not' a.x 'or' c.x) 'or' (('not' b.x 'or' 'not' c.x) '&'
TRUE)) by BINARITH:10
.=(('not' a.x 'or' c.x) 'or' (TRUE '&' ('not' b.x 'or' 'not' c.x))) by
MARGREL1:14
.=('not' a.x 'or' c.x) 'or' ('not' c.x 'or' 'not' b.x) by MARGREL1:14
.=(('not' a.x 'or' c.x) 'or' 'not' c.x) 'or' 'not' b.x by BINARITH:11
.=('not' a.x 'or' TRUE) 'or' 'not' b.x by A5,BINARITH:11
.=TRUE 'or' 'not' b.x by BINARITH:10
.=TRUE by BINARITH:10;
hence thesis by A1,BVFUNC_1:def 11;
end;
theorem Th14:
for a,b,c being Function of Y,BOOLEAN st (a 'imp' b)=I_el(
Y) holds (b 'imp' c) 'imp' (a 'imp' c)=I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
assume
A1: a 'imp' b=I_el(Y);
for x being Element of Y holds ((b 'imp' c) 'imp' (a 'imp' c)).x=TRUE
proof
let x be Element of Y;
A2: ((b 'imp' c) 'imp' (a 'imp' c)).x =('not' (b 'imp' c).x) 'or' (a 'imp'
c).x by BVFUNC_1:def 8
.='not' ('not' b.x 'or' c.x) 'or' (a 'imp' c).x by BVFUNC_1:def 8
.=('not' a.x 'or' c.x) 'or' (b.x '&' 'not' c.x) by BVFUNC_1:def 8;
A3: now
per cases by XBOOLEAN:def 3;
case
c.x=TRUE;
hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10;
end;
case
c.x=FALSE;
then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' c.x 'or' c.x)=TRUE;
end;
end;
(a 'imp' b).x=TRUE by A1,BVFUNC_1:def 11;
then
A4: 'not' a.x 'or' b.x=TRUE by BVFUNC_1:def 8;
A5: 'not' a.x=TRUE or 'not' a.x=FALSE by XBOOLEAN:def 3;
now
per cases by A4,A5,BINARITH:3;
case
'not' a.x=TRUE;
then ((b 'imp' c) 'imp' (a 'imp' c)).x =TRUE 'or' (b.x '&' 'not' c.x)
by A2,BINARITH:10
.=TRUE by BINARITH:10;
hence thesis;
end;
case
b.x=TRUE;
then ((b 'imp' c) 'imp' (a 'imp' c)).x =('not' a.x 'or' c.x) 'or'
'not' c.x by A2,MARGREL1:14
.='not' a.x 'or' TRUE by A3,BINARITH:11
.=TRUE by BINARITH:10;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem Th15:
for a,b being Function of Y,BOOLEAN holds b 'imp' (a 'imp' b) =I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
(b 'imp' (a 'imp' b)).x =('not' b.x) 'or' (a 'imp' b).x by BVFUNC_1:def 8
.=('not' b.x) 'or' (b.x 'or' 'not' a.x) by BVFUNC_1:def 8
.=TRUE 'or' 'not' a.x by A1,BINARITH:11
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' c
) 'imp' (b 'imp' c)=I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
b 'imp' (a 'imp' b) =I_el(Y) by Th15;
hence thesis by Th14;
end;
theorem
for a,b being Function of Y,BOOLEAN holds b 'imp' ((b 'imp' a)
'imp' a)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
A2: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
(b 'imp' ((b 'imp' a) 'imp' a)).x = 'not' b.x 'or' ((b 'imp' a) 'imp'
a).x by BVFUNC_1:def 8
.= 'not' b.x 'or' ('not' (b 'imp' a).x 'or' a.x) by BVFUNC_1:def 8
.= 'not' b.x 'or' ('not' ('not' b.x 'or' a.x) 'or' a.x) by BVFUNC_1:def 8
.= 'not' b.x 'or' ((a.x 'or' b.x) '&' TRUE) by A2,XBOOLEAN:9
.= 'not' b.x 'or' (a.x 'or' b.x) by MARGREL1:14
.= 'not' b.x 'or' b.x 'or' a.x by BINARITH:11
.=TRUE by A1,BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem :: Contraposition
for a,b,c being Function of Y,BOOLEAN holds (c 'imp' (b 'imp' a)
) 'imp' (b 'imp' (c 'imp' a))=I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
A2: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
A3: now
per cases by XBOOLEAN:def 3;
case
c.x=TRUE;
hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10;
end;
case
c.x=FALSE;
then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' c.x 'or' c.x)=TRUE;
end;
end;
((c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a))).x =('not' (c
'imp' (b 'imp' a)).x) 'or' (b 'imp' (c 'imp' a)).x by BVFUNC_1:def 8
.=('not' ('not' c.x 'or' (b 'imp' a).x)) 'or' (b 'imp' (c 'imp' a)).x
by BVFUNC_1:def 8
.=('not' ('not' c.x 'or' ('not' b.x 'or' a.x))) 'or' (b 'imp' (c 'imp'
a)).x by BVFUNC_1:def 8
.=('not' ('not' c.x 'or' ('not' b.x 'or' a.x))) 'or' ('not' b.x 'or' (
c 'imp' a).x) by BVFUNC_1:def 8
.=((c.x '&' ('not' 'not' b.x '&' 'not' a.x))) 'or' ('not' b.x 'or' (
'not' c.x 'or' a.x)) by BVFUNC_1:def 8
.=(('not' c.x 'or' a.x) 'or' 'not' b.x) 'or' (b.x '&' (c.x '&' 'not' a
.x)) by MARGREL1:16
.=((('not' c.x 'or' a.x) 'or' 'not' b.x) 'or' b.x) '&' ((('not' c.x
'or' a.x) 'or' 'not' b.x) 'or' (c.x '&' 'not' a.x)) by XBOOLEAN:9
.=(('not' c.x 'or' a.x) 'or' TRUE) '&' ((('not' c.x 'or' a.x) 'or'
'not' b.x) 'or' (c.x '&' 'not' a.x)) by A1,BINARITH:11
.=TRUE '&' ((('not' c.x 'or' a.x) 'or' 'not' b.x) 'or' (c.x '&' 'not'
a.x)) by BINARITH:10
.=((('not' c.x 'or' a.x) 'or' 'not' b.x) 'or' (c.x '&' 'not' a.x)) by
MARGREL1:14
.=(((a.x 'or' 'not' b.x) 'or' 'not' c.x) 'or' (c.x '&' 'not' a.x)) by
BINARITH:11
.=((a.x 'or' 'not' b.x) 'or' ('not' c.x 'or' (c.x '&' 'not' a.x))) by
BINARITH:11
.=((a.x 'or' 'not' b.x) 'or' (TRUE '&' ('not' c.x 'or' 'not' a.x))) by A3
,XBOOLEAN:9
.=('not' b.x 'or' a.x) 'or' ('not' c.x 'or' 'not' a.x) by MARGREL1:14
.=(('not' b.x 'or' a.x) 'or' 'not' a.x) 'or' 'not' c.x by BINARITH:11
.=('not' b.x 'or' TRUE) 'or' 'not' c.x by A2,BINARITH:11
.=TRUE 'or' 'not' c.x by BINARITH:10
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' ((
a 'imp' b) 'imp' (a 'imp' c))=I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
A2: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
A3: now
per cases by XBOOLEAN:def 3;
case
c.x=TRUE;
hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10;
end;
case
c.x=FALSE;
then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' c.x 'or' c.x)=TRUE;
end;
end;
((b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))).x ='not' (b 'imp'
c).x 'or' ((a 'imp' b) 'imp' (a 'imp' c)).x by BVFUNC_1:def 8
.='not' (b 'imp' c).x 'or' ('not' (a 'imp' b).x 'or' (a 'imp' c).x) by
BVFUNC_1:def 8
.='not' ('not' b.x 'or' c.x) 'or' ('not' (a 'imp' b).x 'or' (a 'imp' c
).x) by BVFUNC_1:def 8
.='not' ('not' b.x 'or' c.x) 'or' ('not' ('not' a.x 'or' b.x) 'or' (a
'imp' c).x) by BVFUNC_1:def 8
.=(b.x '&' 'not' c.x) 'or' (('not' 'not' a.x '&' 'not' b.x) 'or' (
'not' a.x 'or' c.x)) by BVFUNC_1:def 8
.=(((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) 'or' 'not' c.x) '&'
(((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) 'or' b.x) by XBOOLEAN:9
.=((a.x '&' 'not' b.x) 'or' (('not' a.x 'or' c.x) 'or' 'not' c.x)) '&'
(((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) 'or' b.x) by BINARITH:11
.=((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' TRUE)) '&' (((a.x '&'
'not' b.x) 'or' ('not' a.x 'or' c.x)) 'or' b.x) by A3,BINARITH:11
.=((a.x '&' 'not' b.x) 'or' TRUE) '&' (((a.x '&' 'not' b.x) 'or' (
'not' a.x 'or' c.x)) 'or' b.x) by BINARITH:10
.=TRUE '&' (((a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) 'or' b.x)
by BINARITH:10
.=(('not' b.x '&' a.x) 'or' ('not' a.x 'or' c.x)) 'or' b.x by MARGREL1:14
.=((('not' a.x 'or' c.x) 'or' 'not' b.x) '&' (('not' a.x 'or' c.x)
'or' a.x)) 'or' b.x by XBOOLEAN:9
.=((('not' a.x 'or' c.x) 'or' 'not' b.x) '&' (c.x 'or' ('not' a.x 'or'
a.x))) 'or' b.x by BINARITH:11
.=((('not' a.x 'or' c.x) 'or' 'not' b.x) '&' TRUE) 'or' b.x by A1,
BINARITH:10
.=(('not' a.x 'or' c.x) 'or' 'not' b.x) 'or' b.x by MARGREL1:14
.=('not' a.x 'or' c.x) 'or' TRUE by A2,BINARITH:11
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem :: A Hilbert axiom
for a,b,c being Function of Y,BOOLEAN holds (b 'imp' (b 'imp' c)
) 'imp' (b 'imp' c)=I_el(Y)
proof let a,b,c be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
A2: now
per cases by XBOOLEAN:def 3;
case
c.x=TRUE;
hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10;
end;
case
c.x=FALSE;
then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' c.x 'or' c.x)=TRUE;
end;
end;
((b 'imp' (b 'imp' c)) 'imp' (b 'imp' c)).x ='not' (b 'imp' (b 'imp'
c)).x 'or' (b 'imp' c).x by BVFUNC_1:def 8
.='not' ('not' b.x 'or' (b 'imp' c).x) 'or' (b 'imp' c).x by
BVFUNC_1:def 8
.='not' ('not' b.x 'or' ('not' b.x 'or' c.x)) 'or' (b 'imp' c).x by
BVFUNC_1:def 8
.=(b.x '&' ('not' 'not' b.x '&' 'not' c.x)) 'or' ('not' b.x 'or' c.x)
by BVFUNC_1:def 8
.=((b.x '&' b.x) '&' 'not' c.x) 'or' ('not' b.x 'or' c.x) by MARGREL1:16
.=((c.x 'or' 'not' b.x) 'or' b.x) '&' (('not' b.x 'or' c.x) 'or' 'not'
c.x) by XBOOLEAN:9
.=(c.x 'or' TRUE) '&' (('not' b.x 'or' c.x) 'or' 'not' c.x) by A1,
BINARITH:11
.=TRUE '&' (('not' b.x 'or' c.x) 'or' 'not' c.x) by BINARITH:10
.=(('not' b.x 'or' c.x) 'or' 'not' c.x) by MARGREL1:14
.='not' b.x 'or' TRUE by A2,BINARITH:11
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem Th21: :: Frege's law
for a,b,c being Function of Y,BOOLEAN holds (a 'imp' (b
'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))=I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
A2: now
per cases by XBOOLEAN:def 3;
case
c.x=TRUE;
hence ('not' c.x 'or' c.x)=TRUE by BINARITH:10;
end;
case
c.x=FALSE;
then 'not' c.x 'or' c.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' c.x 'or' c.x)=TRUE;
end;
end;
A3: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
((a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))).x =
'not' (a 'imp' (b 'imp' c)).x 'or' ((a 'imp' b) 'imp' (a 'imp' c)).x by
BVFUNC_1:def 8
.='not' ('not' a.x 'or' (b 'imp' c).x) 'or' ((a 'imp' b) 'imp' (a
'imp' c)).x by BVFUNC_1:def 8
.='not' ('not' a.x 'or' ('not' b.x 'or' c.x)) 'or' ((a 'imp' b) 'imp'
(a 'imp' c)).x by BVFUNC_1:def 8
.='not' ('not' a.x 'or' ('not' b.x 'or' c.x)) 'or' ('not' (a 'imp' b).
x 'or' (a 'imp' c).x) by BVFUNC_1:def 8
.='not' ('not' a.x 'or' ('not' b.x 'or' c.x)) 'or' ('not' ('not' a.x
'or' b.x) 'or' (a 'imp' c).x) by BVFUNC_1:def 8
.=('not' 'not' a.x '&' ('not' 'not' b.x '&' 'not' c.x)) 'or' (('not'
'not' a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x)) by BVFUNC_1:def 8
.=(a.x '&' (b.x '&' 'not' c.x)) 'or' (((c.x 'or' 'not' a.x) 'or' a.x)
'&' ((c.x 'or' 'not' a.x) 'or' 'not' b.x)) by XBOOLEAN:9
.=(a.x '&' (b.x '&' 'not' c.x)) 'or' ((c.x 'or' TRUE) '&' ((c.x 'or'
'not' a.x) 'or' 'not' b.x)) by A1,BINARITH:11
.=(a.x '&' (b.x '&' 'not' c.x)) 'or' (TRUE '&' ((c.x 'or' 'not' a.x)
'or' 'not' b.x)) by BINARITH:10
.=((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' (a.x '&' (b.x '&' 'not' c
.x)) by MARGREL1:14
.=(((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' a.x) '&' (((c.x 'or'
'not' a.x) 'or' 'not' b.x) 'or' (b.x '&' 'not' c.x)) by XBOOLEAN:9
.=(((c.x 'or' 'not' a.x) 'or' a.x) 'or' 'not' b.x) '&' (((c.x 'or'
'not' a.x) 'or' 'not' b.x) 'or' (b.x '&' 'not' c.x)) by BINARITH:11
.=((c.x 'or' TRUE) 'or' 'not' b.x) '&' (((c.x 'or' 'not' a.x) 'or'
'not' b.x) 'or' (b.x '&' 'not' c.x)) by A1,BINARITH:11
.=(TRUE 'or' 'not' b.x) '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x)
'or' (b.x '&' 'not' c.x)) by BINARITH:10
.=TRUE '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' (b.x '&' 'not'
c.x)) by BINARITH:10
.=(((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' (b.x '&' 'not' c.x)) by
MARGREL1:14
.=(((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' b.x) '&' (((c.x 'or'
'not' a.x) 'or' 'not' b.x) 'or' 'not' c.x) by XBOOLEAN:9
.=((c.x 'or' 'not' a.x) 'or' TRUE) '&' (((c.x 'or' 'not' a.x) 'or'
'not' b.x) 'or' 'not' c.x) by A3,BINARITH:11
.=TRUE '&' (((c.x 'or' 'not' a.x) 'or' 'not' b.x) 'or' 'not' c.x) by
BINARITH:10
.=(('not' b.x 'or' (c.x 'or' 'not' a.x)) 'or' 'not' c.x) by MARGREL1:14
.=((('not' b.x 'or' 'not' a.x) 'or' c.x) 'or' 'not' c.x) by BINARITH:11
.=(('not' b.x 'or' 'not' a.x) 'or' TRUE) by A2,BINARITH:11
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN holds a=I_el(Y) implies (a
'imp' b) 'imp' b=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
assume
A1: a=I_el(Y);
for x being Element of Y holds ((a 'imp' b) 'imp' b).x=TRUE
proof
let x be Element of Y;
A2: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
A3: a.x=TRUE by A1,BVFUNC_1:def 11;
((a 'imp' b) 'imp' b).x ='not' (a 'imp' b).x 'or' b.x by BVFUNC_1:def 8
.='not' ('not' a.x 'or' b.x) 'or' b.x by BVFUNC_1:def 8
.=(b.x 'or' TRUE) '&' TRUE by A3,A2,XBOOLEAN:9
.=b.x 'or' TRUE by MARGREL1:14
.=TRUE by BINARITH:10;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds c 'imp' (b 'imp' a)=
I_el(Y) implies b 'imp' (c 'imp' a)=I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
assume
A1: c 'imp' (b 'imp' a)=I_el(Y);
for x being Element of Y holds (b 'imp' (c 'imp' a)).x=TRUE
proof
let x be Element of Y;
(c 'imp' (b 'imp' a)).x=TRUE by A1,BVFUNC_1:def 11;
then 'not' c.x 'or' (b 'imp' a).x=TRUE by BVFUNC_1:def 8;
then
A2: 'not' c.x 'or' ('not' b.x 'or' a.x)=TRUE by BVFUNC_1:def 8;
(b 'imp' (c 'imp' a)).x ='not' b.x 'or' (c 'imp' a).x by BVFUNC_1:def 8
.='not' b.x 'or' ('not' c.x 'or' a.x) by BVFUNC_1:def 8
.=TRUE by A2,BINARITH:11;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds c 'imp' (b 'imp' a)=
I_el(Y) & b=I_el(Y) implies c 'imp' a=I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
assume that
A1: c 'imp' (b 'imp' a)=I_el(Y) and
A2: b=I_el(Y);
for x being Element of Y holds (c 'imp' a).x=TRUE
proof
let x be Element of Y;
(c 'imp' (b 'imp' a)).x=TRUE by A1,BVFUNC_1:def 11;
then 'not' c.x 'or' (b 'imp' a).x=TRUE by BVFUNC_1:def 8;
then
A3: 'not' c.x 'or' ('not' b.x 'or' a.x)=TRUE by BVFUNC_1:def 8;
'not' c.x 'or' (FALSE 'or' a.x)=TRUE by A3,A2,BVFUNC_1:def 11,MARGREL1:11;
then 'not' c.x 'or' a.x=TRUE by BINARITH:3;
hence thesis by BVFUNC_1:def 8;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem Th25:
for a being Function of Y,BOOLEAN holds I_el Y 'imp' (I_el
Y 'imp' a)=I_el Y implies a=I_el Y
proof
let a be Function of Y,BOOLEAN;
assume I_el Y 'imp' (I_el Y 'imp' a)=I_el(Y);
then I_el Y 'imp' a=I_el(Y) by Th2;
hence thesis by Th2;
end;
theorem
for b,c being Function of Y,BOOLEAN holds b 'imp' (b 'imp' c)=
I_el(Y) implies b 'imp' c = I_el(Y)
proof
let b,c be Function of Y,BOOLEAN;
assume
A1: b 'imp' (b 'imp' c)=I_el(Y);
for x being Element of Y holds (b 'imp' c).x=TRUE
proof
let x be Element of Y;
A2: (b 'imp' c).x='not' b.x 'or' c.x by BVFUNC_1:def 8;
(b 'imp' (b 'imp' c)).x=TRUE by A1,BVFUNC_1:def 11;
then 'not' b.x 'or' (b 'imp' c).x=TRUE by BVFUNC_1:def 8;
then 'not' b.x 'or' ('not' b.x 'or' c.x)=TRUE by BVFUNC_1:def 8;
then
A3: ('not' b.x 'or' 'not' b.x) 'or' c.x=TRUE by BINARITH:11;
A4: 'not' b.x=TRUE or 'not' b.x=FALSE by XBOOLEAN:def 3;
now
per cases by A3,A4,BINARITH:3;
case
'not' b.x=TRUE;
hence thesis by A2,BINARITH:10;
end;
case
c.x=TRUE;
hence thesis by A2,BINARITH:10;
end;
end;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)
) = I_el(Y) implies (a 'imp' b) 'imp' (a 'imp' c) = I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
assume
A1: a 'imp' (b 'imp' c)=I_el(Y);
for x being Element of Y holds ((a 'imp' b) 'imp' (a 'imp' c)).x=TRUE
proof
let x be Element of Y;
A2: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
(a 'imp' (b 'imp' c)).x=TRUE by A1,BVFUNC_1:def 11;
then 'not' a.x 'or' (b 'imp' c).x=TRUE by BVFUNC_1:def 8;
then
A3: 'not' a.x 'or' ('not' b.x 'or' c.x)=TRUE by BVFUNC_1:def 8;
((a 'imp' b) 'imp' (a 'imp' c)).x ='not' (a 'imp' b).x 'or' (a 'imp'
c).x by BVFUNC_1:def 8
.='not' ('not' a.x 'or' b.x) 'or' (a 'imp' c).x by BVFUNC_1:def 8
.=('not' 'not' a.x '&' 'not' b.x) 'or' ('not' a.x 'or' c.x) by
BVFUNC_1:def 8
.=(('not' a.x 'or' c.x) 'or' a.x) '&' (('not' a.x 'or' c.x) 'or' 'not'
b.x) by XBOOLEAN:9
.=TRUE '&' (('not' a.x 'or' c.x) 'or' a.x) by A3,BINARITH:11
.=(c.x 'or' 'not' a.x) 'or' a.x by MARGREL1:14
.=c.x 'or' TRUE by A2,BINARITH:11
.=TRUE by BINARITH:10;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)
) = I_el(Y) & a 'imp' b = I_el(Y) implies a 'imp' c = I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
assume a 'imp' (b 'imp' c)=I_el(Y) & a 'imp' b = I_el(Y);
then I_el Y 'imp' (I_el Y 'imp' (a 'imp' c))=I_el Y by Th21;
hence thesis by Th25;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)
) = I_el(Y) & a 'imp' b = I_el(Y) & a = I_el(Y) implies c = I_el(Y)
proof
let a,b,c be Function of Y,BOOLEAN;
assume that
A1: (a 'imp' (b 'imp' c)) = I_el(Y) and
A2: a 'imp' b = I_el(Y) and
A3: a = I_el(Y);
for x being Element of Y holds c.x=TRUE
proof
let x be Element of Y;
(a 'imp' (b 'imp' c)).x=TRUE by A1,BVFUNC_1:def 11;
then 'not' a.x 'or' (b 'imp' c).x=TRUE by BVFUNC_1:def 8;
then
A4: 'not' a.x 'or' ('not' b.x 'or' c.x)=TRUE by BVFUNC_1:def 8;
(a 'imp' b).x=TRUE by A2,BVFUNC_1:def 11;
then 'not' a.x 'or' b.x=TRUE by BVFUNC_1:def 8;
then FALSE 'or' b.x=TRUE by A3,BVFUNC_1:def 11,MARGREL1:11;
then b.x=TRUE by BINARITH:3;
then FALSE 'or' ('not' TRUE 'or' c.x)=TRUE
by A4,A3,BVFUNC_1:def 11,MARGREL1:11;
then FALSE 'or' (FALSE 'or' c.x)=TRUE by MARGREL1:11;
then (FALSE 'or' c.x)=TRUE by BINARITH:3;
hence thesis by BINARITH:3;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b,c,d being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c
) = I_el(Y) & a 'imp' (c 'imp' d) = I_el(Y) implies a 'imp' (b 'imp' d) = I_el(
Y)
proof
let a,b,c,d be Function of Y,BOOLEAN;
assume that
A1: a 'imp' (b 'imp' c) = I_el(Y) and
A2: a 'imp' (c 'imp' d) = I_el(Y);
for x being Element of Y holds (a 'imp' (b 'imp' d)).x=TRUE
proof
let x be Element of Y;
A3: (a 'imp' (b 'imp' d)).x ='not' a.x 'or' (b 'imp' d).x by BVFUNC_1:def 8
.='not' a.x 'or' ('not' b.x 'or' (d).x) by BVFUNC_1:def 8;
(a 'imp' (c 'imp' d)).x=TRUE by A2,BVFUNC_1:def 11;
then 'not' a.x 'or' (c 'imp' d).x=TRUE by BVFUNC_1:def 8;
then
A4: 'not' a.x 'or' ('not' c.x 'or' (d).x)=TRUE by BVFUNC_1:def 8;
(a 'imp' (b 'imp' c)).x=TRUE by A1,BVFUNC_1:def 11;
then 'not' a.x 'or' (b 'imp' c).x=TRUE by BVFUNC_1:def 8;
then
A5: 'not' a.x 'or' ('not' b.x 'or' c.x)=TRUE by BVFUNC_1:def 8;
A6: 'not' a.x=TRUE or 'not' a.x=FALSE by XBOOLEAN:def 3;
now
per cases by A5,A6,A4,BINARITH:3;
case
'not' a.x=TRUE & 'not' a.x=TRUE;
hence thesis by A3,BINARITH:10;
end;
case
'not' a.x=TRUE & ('not' c.x 'or' (d).x)=TRUE;
hence thesis by A3,BINARITH:10;
end;
case
('not' b.x 'or' c.x)=TRUE & 'not' a.x=TRUE;
hence thesis by A3,BINARITH:10;
end;
case
A7: ('not' b.x 'or' c.x)=TRUE & ('not' c.x 'or' (d).x)=TRUE;
A8: 'not' c.x=TRUE or 'not' c.x=FALSE by XBOOLEAN:def 3;
A9: 'not' b.x=TRUE or 'not' b.x=FALSE by XBOOLEAN:def 3;
now
per cases by A7,A9,A8,BINARITH:3;
case
'not' b.x=TRUE & 'not' c.x=TRUE;
then (a 'imp' (b 'imp' d)).x ='not' a.x 'or' TRUE by A3,BINARITH:10
.=TRUE by BINARITH:10;
hence thesis;
end;
case
'not' b.x=TRUE & (d).x=TRUE;
hence thesis by A3,BINARITH:10;
end;
case
c.x=TRUE & 'not' c.x=TRUE;
hence thesis by MARGREL1:11;
end;
case
c.x=TRUE & (d).x=TRUE;
then (a 'imp' (b 'imp' d)).x ='not' a.x 'or' TRUE by A3,BINARITH:10
.=TRUE by BINARITH:10;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN holds ('not' a 'imp' 'not' b
) 'imp' (b 'imp' a) = I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
A2: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
(('not' a 'imp' 'not' b) 'imp' (b 'imp' a)).x ='not' ('not' a 'imp'
'not' b).x 'or' (b 'imp' a).x by BVFUNC_1:def 8
.='not' ('not' ('not' a).x 'or' ('not' b).x) 'or' (b 'imp' a).x by
BVFUNC_1:def 8
.=('not' 'not' ('not' a).x '&' 'not' ('not' b).x) 'or' ('not' b.x 'or'
a.x) by BVFUNC_1:def 8
.=(('not' b.x 'or' a.x) 'or' ('not' a).x) '&' (('not' b.x 'or' a.x)
'or' 'not' ('not' b).x) by XBOOLEAN:9
.=('not' b.x 'or' (a.x 'or' ('not' a).x)) '&' (('not' b.x 'or' a.x)
'or' 'not' ('not' b).x) by BINARITH:11
.=('not' b.x 'or' TRUE) '&' (('not' b.x 'or' a.x) 'or' 'not' ('not' b)
.x) by A1,MARGREL1:def 19
.=TRUE '&' (('not' b.x 'or' a.x) 'or' 'not' ('not' b).x) by BINARITH:10
.=((a.x 'or' 'not' b.x) 'or' 'not' ('not' b).x) by MARGREL1:14
.=(a.x 'or' ('not' b.x 'or' 'not' ('not' b).x)) by BINARITH:11
.=(a.x 'or' TRUE) by A2,MARGREL1:def 19
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (
'not' b 'imp' 'not' a)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
A2: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
((a 'imp' b) 'imp' ('not' b 'imp' 'not' a)).x ='not' (a 'imp' b).x
'or' ('not' b 'imp' 'not' a).x by BVFUNC_1:def 8
.='not' ('not' a.x 'or' b.x) 'or' ('not' b 'imp' 'not' a).x by
BVFUNC_1:def 8
.=('not' 'not' a.x '&' 'not' b.x) 'or' ('not' ('not' b).x 'or' ('not'
a).x) by BVFUNC_1:def 8
.=(a.x '&' 'not' b.x) 'or' ('not' 'not' b.x 'or' ('not' a).x) by
MARGREL1:def 19
.=(b.x 'or' 'not' a.x) 'or' (a.x '&' 'not' b.x) by MARGREL1:def 19
.=((b.x 'or' 'not' a.x) 'or' a.x) '&' ((b.x 'or' 'not' a.x) 'or' 'not'
b.x) by XBOOLEAN:9
.=(b.x 'or' TRUE) '&' ((b.x 'or' 'not' a.x) 'or' 'not' b.x) by A1,
BINARITH:11
.=TRUE '&' ((b.x 'or' 'not' a.x) 'or' 'not' b.x) by BINARITH:10
.=(('not' a.x 'or' b.x) 'or' 'not' b.x) by MARGREL1:14
.=('not' a.x 'or' TRUE) by A2,BINARITH:11
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN holds (a 'imp' 'not' b)
'imp' (b 'imp' 'not' a)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
A2: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
((a 'imp' 'not' b) 'imp' (b 'imp' 'not' a)).x ='not' (a 'imp' 'not' b
).x 'or' (b 'imp' 'not' a).x by BVFUNC_1:def 8
.='not' ('not' a.x 'or' ('not' b).x) 'or' (b 'imp' 'not' a).x by
BVFUNC_1:def 8
.=('not' 'not' a.x '&' 'not' ('not' b).x) 'or' ('not' b.x 'or' ('not'
a).x) by BVFUNC_1:def 8
.=(a.x '&' 'not' 'not' b.x) 'or' ('not' b.x 'or' ('not' a).x) by
MARGREL1:def 19
.=('not' b.x 'or' 'not' a.x) 'or' (a.x '&' b.x) by MARGREL1:def 19
.=(('not' b.x 'or' 'not' a.x) 'or' a.x) '&' (('not' b.x 'or' 'not' a.x
) 'or' b.x) by XBOOLEAN:9
.=('not' b.x 'or' TRUE) '&' (('not' b.x 'or' 'not' a.x) 'or' b.x) by A1,
BINARITH:11
.=TRUE '&' (('not' b.x 'or' 'not' a.x) 'or' b.x) by BINARITH:10
.=(('not' a.x 'or' 'not' b.x) 'or' b.x) by MARGREL1:14
.=('not' a.x 'or' TRUE) by A2,BINARITH:11
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN holds ('not' a 'imp' b)
'imp' ('not' b 'imp' a)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
A2: now
per cases by XBOOLEAN:def 3;
case
b.x=TRUE;
hence ('not' b.x 'or' b.x)=TRUE by BINARITH:10;
end;
case
b.x=FALSE;
then 'not' b.x 'or' b.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' b.x 'or' b.x)=TRUE;
end;
end;
(('not' a 'imp' b) 'imp' ('not' b 'imp' a)).x ='not' ('not' a 'imp' b
).x 'or' ('not' b 'imp' a).x by BVFUNC_1:def 8
.='not' ('not' ('not' a).x 'or' b.x) 'or' ('not' b 'imp' a).x by
BVFUNC_1:def 8
.=('not' 'not' ('not' a).x '&' 'not' b.x) 'or' ('not' ('not' b).x 'or'
a.x) by BVFUNC_1:def 8
.=('not' a.x '&' 'not' b.x) 'or' ('not' ('not' b).x 'or' a.x) by
MARGREL1:def 19
.=(b.x 'or' a.x) 'or' ('not' a.x '&' 'not' b.x) by MARGREL1:def 19
.=((b.x 'or' a.x) 'or' 'not' a.x) '&' ((b.x 'or' a.x) 'or' 'not' b.x)
by XBOOLEAN:9
.=(b.x 'or' TRUE) '&' ((b.x 'or' a.x) 'or' 'not' b.x) by A1,BINARITH:11
.=TRUE '&' ((b.x 'or' a.x) 'or' 'not' b.x) by BINARITH:10
.=((a.x 'or' b.x) 'or' 'not' b.x) by MARGREL1:14
.=(a.x 'or' TRUE) by A2,BINARITH:11
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a being Function of Y,BOOLEAN holds (a 'imp' 'not' a) 'imp'
'not' a=I_el(Y)
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
((a 'imp' 'not' a) 'imp' 'not' a).x ='not' (a 'imp' 'not' a).x 'or' (
'not' a).x by BVFUNC_1:def 8
.='not' ('not' a.x 'or' ('not' a).x) 'or' ('not' a).x by BVFUNC_1:def 8
.=(a.x '&' 'not' 'not' a.x) 'or' ('not' a).x by MARGREL1:def 19
.=TRUE by A1,MARGREL1:def 19;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN holds 'not' a 'imp' (a 'imp'
b)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
per cases by XBOOLEAN:def 3;
case
a.x=TRUE;
hence ('not' a.x 'or' a.x)=TRUE by BINARITH:10;
end;
case
a.x=FALSE;
then 'not' a.x 'or' a.x =TRUE 'or' FALSE by MARGREL1:11
.=TRUE by BINARITH:10;
hence ('not' a.x 'or' a.x)=TRUE;
end;
end;
('not' a 'imp' (a 'imp' b)).x ='not' ('not' a).x 'or' (a 'imp' b).x by
BVFUNC_1:def 8
.='not' ('not' a).x 'or' ('not' a.x 'or' b.x) by BVFUNC_1:def 8
.=a.x 'or' ('not' a.x 'or' b.x) by MARGREL1:def 19
.=TRUE 'or' b.x by A1,BINARITH:11
.=TRUE by BINARITH:10;
hence thesis by BVFUNC_1:def 11;
end;
theorem ::De'Morgan
for a,b,c being Function of Y,BOOLEAN holds 'not' (a '&' b '&' c
)=('not' a) 'or' ('not' b) 'or' ('not' c)
proof
let a,b,c be Function of Y,BOOLEAN;
'not' (a '&' b '&' c) ='not' (a '&' b) 'or' ('not' c) by BVFUNC_1:14
.=('not' a) 'or' ('not' b) 'or' ('not' c) by BVFUNC_1:14;
hence thesis;
end;
theorem ::De'Morgan
for a,b,c being Function of Y,BOOLEAN holds 'not' (a 'or' b 'or'
c)=('not' a) '&' ('not' b) '&' ('not' c)
proof
let a,b,c be Function of Y,BOOLEAN;
'not' (a 'or' b 'or' c) ='not' (a 'or' b) '&' ('not' c) by BVFUNC_1:13
.=('not' a) '&' ('not' b) '&' ('not' c) by BVFUNC_1:13;
hence thesis;
end;
theorem ::Distributive
for a,b,c,d being Function of Y,BOOLEAN holds a 'or' (b '&' c
'&' d) = (a 'or' b) '&' (a 'or' c) '&' (a 'or' d)
proof
let a,b,c,d be Function of Y,BOOLEAN;
a 'or' (b '&' c '&' d) =(a 'or' (b '&' c)) '&' (a 'or' d) by BVFUNC_1:11
.=((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d) by BVFUNC_1:11;
hence thesis;
end;
theorem ::Distributive
for a,b,c,d being Function of Y,BOOLEAN holds a '&' (b 'or' c
'or' d) = (a '&' b) 'or' (a '&' c) 'or' (a '&' d)
proof
let a,b,c,d be Function of Y,BOOLEAN;
a '&' (b 'or' c 'or' d) =(a '&' (b 'or' c)) 'or' (a '&' d) by BVFUNC_1:12
.=(a '&' b) 'or' (a '&' c) 'or' (a '&' d) by BVFUNC_1:12;
hence thesis;
end;