:: On Fuzzy Negations Generated by Fuzzy Implications
::  by Adam Grabowski
:: 
:: Received February 26, 2020
:: Copyright (c) 2020-2021 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, FUZIMPL1, SUBSET_1, CARD_1,
      TARSKI, ARYTM_1, ARYTM_3, POWER, FUNCT_1, XBOOLE_0, RELAT_1, BINOP_1,
      FUZIMPL2, ORDINAL2, WAYBEL29, VALUED_0, FUNCT_2, FUZIMPL3, MEMBERED,
      PARTFUN1, ZFMISC_1, BORSUK_1, OPOSET_1, NAT_6;
 notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XXREAL_0, NUMBERS, BINOP_1,
      ZFMISC_1, VALUED_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3,
      STRUCT_0, RCOMP_1, PARTFUN1, MEMBERED, POWER, BORSUK_1, FUZIMPL1,
      FUZIMPL2;
 constructors SEQ_4, TOPMETR, PREPOWER, POWER, FUZIMPL1, FUZIMPL2, FUNCT_3;
 registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, ORDINAL1,
      FUZNORM1, VALUED_0, NUMBERS, FUNCT_2, FOMODEL0, FUNCT_1, EULRPART,
      RELAT_1, FUZIMPL2, BORSUK_1, FUZIMPL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

theorem :: FUZIMPL3:1
  for x, r being Real st 0 <= x <= 1 & r > -1 holds
    x * r + 1 > 0;

theorem :: FUZIMPL3:2
  for z being Real st z in [.0,1.] & z <> 0 holds
    ex w being Element of [.0,1.] st w < z;

theorem :: FUZIMPL3:3
  for z being Real st z in [.0,1.] & z <> 1 holds
    ex w being Element of [.0,1.] st w > z;

registration
  cluster bijective increasing for UnOp of [.0,1.];
end;

registration
  cluster bijective non-decreasing -> increasing for UnOp of [.0,1.];
  cluster bijective increasing -> non-decreasing for UnOp of [.0,1.];
end;

registration let f be bijective increasing UnOp of [.0,1.];
  cluster f" -> real-valued Function-like;
end;

registration let f be bijective increasing UnOp of [.0,1.];
  cluster (f|[.0,1.])" -> real-valued;
end;

theorem :: FUZIMPL3:4
  for f being one-to-one UnOp of [.0,1.],
      d being Element of [.0,1.] st
    d in rng f holds (f").d in dom f;

theorem :: FUZIMPL3:5
  for f being bijective increasing UnOp of [.0,1.] holds
    f" is increasing;

registration let f be bijective increasing UnOp of [.0,1.];
  cluster f" -> increasing;
end;

theorem :: FUZIMPL3:6
  for f being UnOp of [.0,1.] holds
    f is non-decreasing iff
      for a,b being Element of [.0,1.] st a <= b holds f.a <= f.b;

theorem :: FUZIMPL3:7
  for f being UnOp of [.0,1.] holds
    f is non-increasing iff
      for a,b being Element of [.0,1.] st a <= b holds f.a >= f.b;

theorem :: FUZIMPL3:8
  for f being UnOp of [.0,1.] holds
    f is decreasing iff
      for a,b being Element of [.0,1.] st a < b holds f.a > f.b;

theorem :: FUZIMPL3:9
  for f being UnOp of [.0,1.] holds
    f is increasing iff
      for a,b being Element of [.0,1.] st a < b holds f.a < f.b;

theorem :: FUZIMPL3:10
  for f being increasing bijective UnOp of [.0,1.] holds
    f.0 = 0 & f.1 = 1;

registration let f be bijective increasing UnOp of [.0,1.];
  cluster f" -> bijective increasing for UnOp of [.0,1.];
end;

begin :: Conjugate Fuzzy Implications

definition
  func Theta -> set equals
:: FUZIMPL3:def 1
    the set of all f where f is bijective increasing UnOp of [.0,1.];
end;

definition let f be BinOp of [.0,1.];
           let h be bijective increasing UnOp of [.0,1.];
  func ConjImpl (f,h) -> BinOp of [.0,1.] means
:: FUZIMPL3:def 2
    for x1,x2 being Element of [.0,1.] holds
      it.(x1,x2) = h".(f.(h.x1, h.x2));
end;

definition let f,g be BinOp of [.0,1.];
  pred f,g are_conjugate means
:: FUZIMPL3:def 3
    ex h being bijective increasing UnOp of [.0,1.] st
      g = ConjImpl (f,h);
end;

registration
  let I be Fuzzy_Implication,
      f be bijective non-decreasing UnOp of [.0,1.];
  cluster ConjImpl (I,f) -> decreasing_on_1st increasing_on_2nd
    00-dominant 11-dominant 10-weak;
end;

theorem :: FUZIMPL3:11 ::: Proposition 1.1.8 p. 6
  for I being Fuzzy_Implication,
      f being bijective increasing UnOp of [.0,1.] holds
    ConjImpl (I,f) is Fuzzy_Implication;

registration
  cluster satisfying_(NP) satisfying_(OP) satisfying_(EP) satisfying_(IP)
    for Fuzzy_Implication;
end;

theorem :: FUZIMPL3:12  :: Proposition 1.3.6 a) p. 13
  for I being Fuzzy_Implication,
      f being bijective increasing UnOp of [.0,1.] st
   I is satisfying_(NP) holds
   ConjImpl (I,f) is satisfying_(NP);

theorem :: FUZIMPL3:13  :: Proposition 1.3.6 b) p. 13
  for I being Fuzzy_Implication,
      f being bijective increasing UnOp of [.0,1.] st
   I is satisfying_(EP) holds
     ConjImpl (I,f) is satisfying_(EP);

theorem :: FUZIMPL3:14  :: Proposition 1.3.6 c) p. 13
  for I being Fuzzy_Implication,
      f being bijective increasing UnOp of [.0,1.] st
   I is satisfying_(IP) holds
   ConjImpl (I,f) is satisfying_(IP);

theorem :: FUZIMPL3:15  :: Proposition 1.3.6 d) p. 13
  for I being Fuzzy_Implication,
      f being bijective increasing UnOp of [.0,1.] st
   I is satisfying_(OP) holds
   ConjImpl (I,f) is satisfying_(OP);

registration
  let I be satisfying_(NP) Fuzzy_Implication,
      f be bijective increasing UnOp of [.0,1.];
  cluster ConjImpl (I,f) -> satisfying_(NP);
end;

registration
  let I be satisfying_(EP) Fuzzy_Implication,
      f be bijective increasing UnOp of [.0,1.];
  cluster ConjImpl (I,f) -> satisfying_(EP);
end;

registration
  let I be satisfying_(IP) Fuzzy_Implication,
      f be bijective increasing UnOp of [.0,1.];
  cluster ConjImpl (I,f) -> satisfying_(IP);
end;

registration
  let I be satisfying_(OP) Fuzzy_Implication,
      f be bijective increasing UnOp of [.0,1.];
  cluster ConjImpl (I,f) -> satisfying_(OP);
end;

theorem :: FUZIMPL3:16
  for I being Fuzzy_Implication,
      f being bijective increasing UnOp of [.0,1.] holds
    ConjImpl (I,f) = f" * I * [:f,f:];

begin :: Fuzzy Negations

definition let N be UnOp of [.0,1.];
  attr N is satisfying_(N1) means
:: FUZIMPL3:def 4
    N.0 = 1 & N.1 = 0;
  attr N is satisfying_(N2) means
:: FUZIMPL3:def 5
    N is non-increasing;
end;

definition
  func N_CC -> UnOp of [.0,1.] means
:: FUZIMPL3:def 6
    for x being Element of [.0,1.] holds
      it.x = 1 - x;
end;

registration
  cluster N_CC -> satisfying_(N1) satisfying_(N2);
end;

registration
  cluster N_CC -> bijective decreasing;
end;

registration
  cluster bijective decreasing for UnOp of [.0,1.];
end;

registration
  cluster satisfying_(N1) satisfying_(N2) for UnOp of [.0,1.];
end;

definition
  mode Fuzzy_Negation is satisfying_(N1) satisfying_(N2) UnOp of [.0,1.];
end;

definition let f be UnOp of [.0,1.];
  attr f is continuous means
:: FUZIMPL3:def 7
    ex g being Function of I[01], I[01] st f = g &
      g is continuous;
end;

definition let N be UnOp of [.0,1.];
  attr N is involutive means
:: FUZIMPL3:def 8
    for x being Element of [.0,1.] holds
      N.(N.x) = x;
end;

definition let N be UnOp of [.0,1.];
  attr N is satisfying_(N3) means
:: FUZIMPL3:def 9
    N is decreasing;
  attr N is satisfying_(N4) means
:: FUZIMPL3:def 10
    N is continuous;
  attr N is satisfying_(N5) means
:: FUZIMPL3:def 11
    N is involutive;
end;

definition let N be UnOp of [.0,1.];
  attr N is negation-strict means
:: FUZIMPL3:def 12
    N is satisfying_(N3) satisfying_(N4);
end;

definition let N be UnOp of [.0,1.];
  attr N is negation-strong means
:: FUZIMPL3:def 13
    N is satisfying_(N5);
  attr N is non-vanishing means
:: FUZIMPL3:def 14
    for x being Element of [.0,1.] holds
    N.x = 0 iff x = 1;
  attr N is non-filling means
:: FUZIMPL3:def 15
    for x being Element of [.0,1.] holds
    N.x = 1 iff x = 0;
end;

begin :: Generating Fuzzy Negations from Fuzzy Implications

theorem :: FUZIMPL3:17
  for f being decreasing bijective UnOp of [.0,1.] holds
    f.0 = 1 & f.1 = 0;

definition let I be BinOp of [.0,1.];
  func FNegation I -> UnOp of [.0,1.] means
:: FUZIMPL3:def 16
    for x being Element of [.0,1.] holds
      it.x = I.(x,0);
end;

:: Lemma 1.4.14

registration let I be satisfying_(I1) satisfying_(I3) satisfying_(I5)
                 BinOp of [.0,1.];
  cluster FNegation I -> satisfying_(N1) satisfying_(N2);
end;

:: Definition 1.4.15
theorem :: FUZIMPL3:18 ::: natural negation generated by I
  for I being Fuzzy_Implication holds
    FNegation I is Fuzzy_Negation;

begin :: Boundary Fuzzy Negations

definition
  func NegationD1 -> UnOp of [.0,1.] means
:: FUZIMPL3:def 17
    for x being Element of [.0,1.] holds
      (x = 0 implies it.x = 1) &
      (x <> 0 implies it.x = 0);
  func NegationD2 -> UnOp of [.0,1.] means
:: FUZIMPL3:def 18
    for x being Element of [.0,1.] holds
      (x = 1 implies it.x = 0) &
      (x <> 1 implies it.x = 1);
end;

:: The Ordering of Fuzzy Negations

definition let f1, f2 be UnOp of [.0,1.];
  pred f1 <= f2 means
:: FUZIMPL3:def 19
    for a being Element of [.0,1.] holds
      f1.a <= f2.a;
end;

registration
  cluster NegationD1 -> satisfying_(N1) satisfying_(N2);
  cluster NegationD2 -> satisfying_(N1) satisfying_(N2);
end;

theorem :: FUZIMPL3:19
  for N being Fuzzy_Negation holds
    NegationD1 <= N <= NegationD2;

begin :: Table 1.7:
:: On Fuzzy Negations Generated by Fuzzy Implications

theorem :: FUZIMPL3:20
  FNegation I_LK = N_CC;

theorem :: FUZIMPL3:21
  FNegation I_GD = NegationD1;

theorem :: FUZIMPL3:22
  FNegation I_RC = N_CC;

theorem :: FUZIMPL3:23
  FNegation I_KD = N_CC;

theorem :: FUZIMPL3:24
  FNegation I_GG = NegationD1;

theorem :: FUZIMPL3:25
  FNegation I_RS = NegationD1;

theorem :: FUZIMPL3:26
  FNegation I_YG = NegationD1;

theorem :: FUZIMPL3:27
  FNegation I_WB = NegationD2;

theorem :: FUZIMPL3:28
  FNegation I_FD = N_CC;

theorem :: FUZIMPL3:29 :: Proposition 1.4.17 i)
  for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds
    FNegation I is Fuzzy_Negation;

theorem :: FUZIMPL3:30  :: Proposition 1.4.17 ii)
  for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.]
  for x being Element of [.0,1.] holds
      x <= (FNegation I).((FNegation I).x);

theorem :: FUZIMPL3:31 :: Proposition 1.4.17 iii)
  for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds
    (FNegation I) * (FNegation I) * (FNegation I) = FNegation I;

begin :: Sugeno Negation

definition let x,l be Real; ::: see NAT_6
  attr l is x_greater means
:: FUZIMPL3:def 20
    l > x;
end;

registration
  cluster -1_greater for Real;
end;

definition let l be Real;
  assume
  l > -1;
  func SugenoNegation l -> UnOp of [.0,1.] means
:: FUZIMPL3:def 21
    for x being Element of [.0,1.] holds
      it.x = (1 - x) / (1 + l * x);
end;

theorem :: FUZIMPL3:32
  N_CC = SugenoNegation 0;

registration let r be -1_greater Real;
  cluster SugenoNegation r -> satisfying_(N1) satisfying_(N2);
end;

begin :: Conjugate Fuzzy Negations

definition let f be UnOp of [.0,1.];
           let h be bijective increasing UnOp of [.0,1.];
  func ConjNeg (f,h) -> UnOp of [.0,1.] means
:: FUZIMPL3:def 22
    for x being Element of [.0,1.] holds
      it.x = h".(f.(h.x));
end;

theorem :: FUZIMPL3:33
  for I being Fuzzy_Negation,
      f being bijective increasing UnOp of [.0,1.] holds
    ConjNeg (I,f) = f" * I * f;

definition let f,g be UnOp of [.0,1.];
  pred f,g are_conjugate means
:: FUZIMPL3:def 23
    ex h being bijective increasing UnOp of [.0,1.] st
      g = ConjNeg (f,h);
end;

:: Proposition 1.4.8

registration
  let N be Fuzzy_Negation,
      h be bijective increasing UnOp of [.0,1.];
  cluster ConjNeg (N,h) -> satisfying_(N1) satisfying_(N2);
end;

theorem :: FUZIMPL3:34 :: Theorem 1.4.21
  for I being Fuzzy_Implication,
      h being bijective increasing UnOp of [.0,1.] holds
    ConjNeg (FNegation I,h) = FNegation ConjImpl (I,h);