:: Basic Formal Properties of Triangular Norms and Conorms
:: by Adam Grabowski
::
:: Received June 27, 2017
:: Copyright (c) 2017-2018 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 NUMBERS, XXREAL_1, REAL_1, XXREAL_0, SUBSET_1, CARD_1, ARYTM_1,
ARYTM_3, FUNCT_1, XBOOLE_0, RELAT_1, XREAL_0, FUNCT_7, FUZNORM1,
ZFMISC_1, BINOP_1, MSAFREE2, MEMBERED;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
MEMBERED, ZFMISC_1, BINOP_1, VALUED_0, RELAT_1, XXREAL_2, XREAL_0,
COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, REAL_1, SEQ_4, RCOMP_1,
PRE_TOPC, TOPS_2, METRIC_1, DOMAIN_1, STRUCT_0, TOPMETR, TSEP_1, TMAP_1,
FUZZY_1, BORSUK_1, MEASURE5;
constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, RCOMP_1, CONNSP_1, TOPS_2,
TMAP_1, TOPMETR, XXREAL_2, BINOP_2, RVSUM_1, PCOMPS_1, BINOP_1, FUZZY_1,
XREAL_0, INTEGRA1, MESFUNC5, EXTREAL1;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, TOPMETR, CONNSP_1,
ORDINAL1, INTEGRA1, INTEGRA2, MEASURE5, EXTREAL1, SUPINF_1, SUPINF_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
registration
cluster [.0,1.] -> non empty;
end;
theorem :: FUZNORM1:1
for a,b being Element of [.0,1.] holds
min (a,b) in [.0,1.];
theorem :: FUZNORM1:2
for a,b being Element of [.0,1.] holds
max (a,b) in [.0,1.];
theorem :: FUZNORM1:3
for a,b being Element of [.0,1.] holds
a * b in [.0,1.];
theorem :: FUZNORM1:4
for a,b being Element of [.0,1.] holds
max (0, a + b - 1) in [.0,1.];
theorem :: FUZNORM1:5
for a,b being Element of [.0,1.] holds
min (a + b, 1) in [.0,1.];
theorem :: FUZNORM1:6
for a,b,c being Element of [.0,1.] holds
max (0,max(0,a+b-1)+c-1) = max (0,a+max(0,b+c-1)-1);
theorem :: FUZNORM1:7
for a being Element of [.0,1.] holds
1 - a in [.0,1.];
theorem :: FUZNORM1:8
for a, b being Element of [.0,1.] holds
a + b - a * b in [.0,1.];
theorem :: FUZNORM1:9
for a, b being Element of [.0,1.] holds
(a * b) / (a + b - a * b) in [.0,1.];
theorem :: FUZNORM1:10
for a,b being Element of [.0,1.] st max (a,b) <> 1 holds
a <> 1 & b <> 1;
theorem :: FUZNORM1:11
for x, y being Element of [.0,1.] holds
x * y = x + y implies x = 0;
theorem :: FUZNORM1:12
for a,b being Element of [.0,1.] holds
max (a,b) = 1 - min (1-a,1-b);
theorem :: FUZNORM1:13
for a,b being Element of [.0,1.] holds
min (a+b,1) = 1 - max (0,1-a+(1-b)-1);
theorem :: FUZNORM1:14
for a,b being Element of [.0,1.] holds
(a + b - 2 * a * b) / (1 - a * b) in [.0,1.];
registration let f be BinOp of [.0,1.];
let a, b be Real;
cluster f.(a,b) -> real;
end;
theorem :: FUZNORM1:15
for a,b being Real,
t being BinOp of [.0,1.] holds
t.(a,b) in [.0,1.];
theorem :: FUZNORM1:16
for f being BinOp of [.0,1.],
a, b being Real holds
1 - f.(1 - a, 1 - b) in [.0,1.];
theorem :: FUZNORM1:17 ::: move theorems from MESFUNC5 to XXREAL_0
for x,y,k being Real st k <= 0 holds
k*min(x,y) = max(k*x,k*y) & k*max(x,y) = min(k*x,k*y);
begin :: Basic Example of a Triangular Norm and Conorm: min and max
definition let A be real-membered set;
let f be BinOp of A;
attr f is monotonic means
:: FUZNORM1:def 1
for a,b,c,d being Element of A st
a <= c & b <= d holds f.(a,b) <= f.(c,d);
attr f is with-1-identity means
:: FUZNORM1:def 2
for a being Element of A holds f.(a,1) = a;
attr f is with-1-annihilating means
:: FUZNORM1:def 3
for a being Element of A holds f.(a,1) = 1;
attr f is with-0-identity means
:: FUZNORM1:def 4
for a being Element of A holds f.(a,0) = a;
attr f is with-0-annihilating means
:: FUZNORM1:def 5
for a being Element of A holds f.(a,0) = 0;
end;
scheme :: FUZNORM1:sch 1
ExBinOp { A() -> non empty real-membered set, F(Real, Real) -> set } :
ex f being BinOp of A() st
for a,b being Element of A() holds f.(a,b) = F(a,b)
provided
for a,b being Element of A() holds F(a,b) in A();
definition
func minnorm -> BinOp of [.0,1.] means
:: FUZNORM1:def 6
for a,b being Element of [.0,1.] holds
it.(a,b) = min (a,b);
end;
registration
cluster minnorm -> commutative associative monotonic with-1-identity;
end;
registration
cluster commutative associative monotonic with-1-identity
for BinOp of [.0,1.];
end;
definition
mode t-norm is
commutative associative monotonic with-1-identity BinOp of [.0,1.];
end;
definition
func maxnorm -> BinOp of [.0,1.] means
:: FUZNORM1:def 7
for a,b being Element of [.0,1.] holds
it.(a,b) = max (a,b);
end;
registration
cluster maxnorm -> commutative associative monotonic with-0-identity;
end;
registration
cluster commutative associative monotonic with-0-identity
for BinOp of [.0,1.];
end;
definition
mode t-conorm is
commutative associative monotonic with-0-identity BinOp of [.0,1.];
end;
theorem :: FUZNORM1:18
for t being commutative monotonic with-1-identity BinOp of [.0,1.] holds
for a being Element of [.0,1.] holds
t.(a,0) = 0;
theorem :: FUZNORM1:19
for t being commutative monotonic with-0-identity BinOp of [.0,1.] holds
for a being Element of [.0,1.] holds
t.(a,1) = 1;
registration
cluster -> with-0-annihilating
for commutative monotonic with-1-identity BinOp of [.0,1.];
cluster -> with-1-annihilating
for commutative monotonic with-0-identity BinOp of [.0,1.];
end;
begin :: Further Examples of Triangular Norms
definition
func prodnorm -> BinOp of [.0,1.] means
:: FUZNORM1:def 8
for a,b being Element of [.0,1.] holds
it.(a,b) = a * b;
end;
registration
cluster prodnorm -> commutative associative monotonic with-1-identity;
end;
definition
func probsum_conorm -> BinOp of [.0,1.] means
:: FUZNORM1:def 9
for a,b being Element of [.0,1.] holds
it.(a,b) = a + b - a * b;
end;
definition
func Lukasiewicz_norm -> BinOp of [.0,1.] means
:: FUZNORM1:def 10
for a,b being Element of [.0,1.] holds
it.(a,b) = max (0, a + b - 1);
end;
registration
cluster Lukasiewicz_norm -> commutative associative monotonic
with-1-identity;
end;
definition
func drastic_norm -> BinOp of [.0,1.] means
:: FUZNORM1:def 11
for a,b being Element of [.0,1.] holds
(max (a,b) = 1 implies it.(a,b) = min (a,b)) &
(max (a,b) <> 1 implies it.(a,b) = 0);
end;
theorem :: FUZNORM1:20
for a,b being Element of [.0,1.] holds
(a = 1 implies drastic_norm.(a,b) = b) &
(b = 1 implies drastic_norm.(a,b) = a) &
(a <> 1 & b <> 1 implies drastic_norm.(a,b) = 0);
registration
cluster drastic_norm -> commutative associative with-1-identity
monotonic;
end;
definition
func nilmin_norm -> BinOp of [.0,1.] means
:: FUZNORM1:def 12
for a,b being Element of [.0,1.] holds
(a + b > 1 implies it.(a,b) = min (a,b)) &
(a + b <= 1 implies it.(a,b) = 0);
end;
registration
cluster nilmin_norm -> commutative associative with-1-identity
monotonic;
end;
definition
func Hamacher_norm -> BinOp of [.0,1.] means
:: FUZNORM1:def 13
for a,b being Element of [.0,1.] holds
it.(a,b) = (a * b) / (a + b - a * b);
end;
registration
cluster Hamacher_norm -> commutative associative with-1-identity
monotonic;
end;
begin :: Basic Triangular Conorms
definition
func drastic_conorm -> BinOp of [.0,1.] means
:: FUZNORM1:def 14
for a,b being Element of [.0,1.] holds
(min (a,b) = 0 implies it.(a,b) = max (a,b)) &
(min (a,b) <> 0 implies it.(a,b) = 1);
end;
begin :: Translating between Triangular Norms and Conorms
definition
let t be BinOp of [.0,1.];
func conorm t -> BinOp of [.0,1.] means
:: FUZNORM1:def 15
for a,b being Element of [.0,1.] holds
it.(a,b) = 1 - t.(1 - a,1 - b);
end;
registration let t be t-norm;
cluster conorm t -> monotonic commutative associative with-0-identity;
end;
theorem :: FUZNORM1:21
maxnorm = conorm minnorm;
theorem :: FUZNORM1:22
for t being BinOp of [.0,1.] holds
conorm conorm t = t;
:::theorem ::: obvious
::: for t being t-norm holds conorm t is t-conorm;
begin :: The Ordering of Triangular Norms (and Conorms)
definition let f1, f2 be BinOp of [.0,1.];
pred f1 <= f2 means
:: FUZNORM1:def 16
for a,b being Element of [.0,1.] holds
f1.(a,b) <= f2.(a,b);
end;
theorem :: FUZNORM1:23
for t being t-norm holds
drastic_norm <= t;
theorem :: FUZNORM1:24
for t being t-norm holds
t <= minnorm;
theorem :: FUZNORM1:25
for t1, t2 being t-norm st t1 <= t2 holds
conorm t2 <= conorm t1;
begin :: The Rest of Triangular Conorms
definition
func Hamacher_conorm -> BinOp of [.0,1.] means
:: FUZNORM1:def 17
for a,b being Element of [.0,1.] holds
(a = b = 1 implies it.(a,b) = 1) &
(a <> 1 or b <> 1 implies it.(a,b) = (a + b - 2 * a * b) / (1 - a * b));
end;
theorem :: FUZNORM1:26
conorm Hamacher_norm = Hamacher_conorm;
registration
cluster Hamacher_conorm -> commutative associative with-0-identity
monotonic;
end;
theorem :: FUZNORM1:27
conorm drastic_norm = drastic_conorm;
theorem :: FUZNORM1:28
conorm prodnorm = probsum_conorm;
registration
cluster probsum_conorm -> commutative associative with-0-identity monotonic;
end;
definition
func nilmax_conorm -> BinOp of [.0,1.] means
:: FUZNORM1:def 18
for a,b being Element of [.0,1.] holds
(a + b < 1 implies it.(a,b) = max (a,b)) &
(a + b >= 1 implies it.(a,b) = 1);
end;
theorem :: FUZNORM1:29
conorm nilmin_norm = nilmax_conorm;
registration
cluster nilmax_conorm -> commutative associative with-0-identity monotonic;
end;
definition
func BoundedSum_conorm -> BinOp of [.0,1.] means
:: FUZNORM1:def 19
for a,b being Element of [.0,1.] holds
it.(a,b) = min (a + b,1);
end;
theorem :: FUZNORM1:30
conorm Lukasiewicz_norm = BoundedSum_conorm;
registration
cluster BoundedSum_conorm -> commutative associative with-0-identity
monotonic;
end;
theorem :: FUZNORM1:31
for t being t-conorm holds maxnorm <= t;
theorem :: FUZNORM1:32
for t being t-conorm holds t <= drastic_conorm;