:: Two Axiomatizations of {N}elson Algebras
::  by Adam Grabowski
:: 
:: Received April 19, 2015
:: Copyright (c) 2015-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 LATTICES, BINOP_1, XBOOLE_0, EQREL_1, XBOOLEAN, XXREAL_0,
      REALSET1, SUBSET_1, STRUCT_0, XXREAL_2, FUNCT_1, ARYTM_3, ARYTM_1,
      ROBBINS1, NELSON_1, PBOOLE, ZFMISC_1, OPOSET_1;
 notations TARSKI, XBOOLE_0, LATTICES, SUBSET_1, BINOP_1, FUNCT_2, STRUCT_0,
      ROBBINS1, ROBBINS3;
 constructors BINOP_1, ROBBINS3;
 registrations STRUCT_0, LATTICES, LATTICE2, ROBBINS1, ROBBINS3, XBOOLE_0,
      ZFMISC_1, LATTAD_1;
 requirements SUBSET, BOOLE;


begin :: De Morgan Algebras

definition let L be non empty OrthoLattStr;
  attr L is DeMorgan means
:: NELSON_1:def 1
    for x, y being Element of L holds
      (x "/\" y)` = x` "\/" y`;
end;

registration
  cluster de_Morgan involutive -> DeMorgan for non empty OrthoLattStr;
  cluster DeMorgan involutive -> de_Morgan for non empty OrthoLattStr;
end;

registration
  cluster trivial -> DeMorgan for non empty OrthoLattStr;
end;

registration
  cluster DeMorgan involutive bounded distributive Lattice-like for
    non empty OrthoLattStr;
end;

definition
  mode DeMorgan_Algebra is DeMorgan involutive
    distributive Lattice-like non empty OrthoLattStr;
end;

definition
  mode Quasi-Boolean_Algebra is bounded DeMorgan_Algebra;
end;

 reserve L for Quasi-Boolean_Algebra,
         x, y, z for Element of L;

theorem :: NELSON_1:1
  (x "\/" y)` = x` "/\" y`;

theorem :: NELSON_1:2
  (Top L)` = Bottom L;

theorem :: NELSON_1:3
  (Bottom L)` = Top L;

theorem :: NELSON_1:4
  x "/\" (x "/\" y) = x "/\" y;

theorem :: NELSON_1:5
  x "\/" (x "\/" y) = x "\/" y;

begin :: The Structure and Operators in Nelson Algebras

definition
  struct (OrthoLattStr) NelsonStr
                 (# carrier -> set,
                      unity -> Element of the carrier,
            Compl, Nnegation -> UnOp of the carrier,
       Iimpl, impl, L_join, L_meet -> BinOp of the carrier #);
end;

registration
  cluster strict non empty for NelsonStr;
end;

registration
  cluster trivial DeMorgan involutive bounded distributive Lattice-like for
    non empty NelsonStr;
end;

definition let L be non empty NelsonStr,
               a, b be Element of L;
  func a => b -> Element of L equals
:: NELSON_1:def 2
    (the Iimpl of L).(a,b);
end;

definition let L be non empty NelsonStr,
               a, b be Element of L;
  pred a < b means
:: NELSON_1:def 3
    a => b = Top L;
end;

:: Lattice-like ordering

definition let L be non empty NelsonStr,
               a, b be Element of L;
  pred a <= b means
:: NELSON_1:def 4
    a = a "/\" b;
end;

:: Strong negation operator

definition let L be non empty NelsonStr,
               a be Element of L;
  func ! a -> Element of L equals
:: NELSON_1:def 5
    (the Nnegation of L).a;
end;

:: Strong implication

definition let L be non empty NelsonStr,
               a, b be Element of L;
  func a =-> b -> Element of L equals
:: NELSON_1:def 6
    (the impl of L).(a,b);
end;

begin :: The Non-Equational Axiomatization of Nelson Algebras

::NdR _A1, _A2 : quasi_ordering on A
definition let L be non empty NelsonStr;
  attr L is satisfying_A1 means
:: NELSON_1:def 7
    for a being Element of L holds
      a < a;

  attr L is satisfying_A1b means
:: NELSON_1:def 8
    for a, b, c being Element of L holds
      a < b & b < c implies a < c;
end;

definition let L be bounded Lattice-like non empty NelsonStr;
  attr L is satisfying_A2 means
:: NELSON_1:def 9
    L is DeMorgan involutive distributive;
end;

registration
  cluster satisfying_A2 -> DeMorgan involutive distributive
    for bounded Lattice-like non empty NelsonStr;
  cluster DeMorgan involutive distributive -> satisfying_A2
    for bounded Lattice-like non empty NelsonStr;
end;

:: Axioms of N-algebras (according to Rasiowa)
:: These lattices are called Nelson algebras now, but Rasiowa used the name
:: either N-lattices or quasi-pseudo-boolean algebras.

definition let L be non empty NelsonStr;
  attr L is satisfying_N3 means
:: NELSON_1:def 10
    for x, a, b being Element of L holds
      a "/\" x < b iff x < (a => b);

  attr L is satisfying_N4 means
:: NELSON_1:def 11
    for a, b being Element of L holds
      a =-> b = (a => b) "/\" ((-b) => -a);

  attr L is satisfying_N5 means
:: NELSON_1:def 12
    for a, b being Element of L holds
      a =-> b = Top L iff a "/\" b = a;

  attr L is satisfying_N6 means
:: NELSON_1:def 13
    for a, b, c being Element of L holds
      a < c & b < c implies a "\/" b < c;

  attr L is satisfying_N7 means
:: NELSON_1:def 14
    for a, b, c being Element of L holds
      a < b & a < c implies a < b "/\" c;

  attr L is satisfying_N8 means
:: NELSON_1:def 15
    for a, b being Element of L holds
      (a "/\" -b) < -(a => b);

  attr L is satisfying_N9 means
:: NELSON_1:def 16
    for a, b being Element of L holds
      -(a => b) < (a "/\" -b);

  attr L is satisfying_N10 means
:: NELSON_1:def 17
    for a being Element of L holds
      a < -!a;

  attr L is satisfying_N11 means
:: NELSON_1:def 18
    for a being Element of L holds
      -!a < a;

  attr L is satisfying_N12 means
:: NELSON_1:def 19
    for a, b being Element of L holds
      a "/\" -a < b;

  attr L is satisfying_N13 means
:: NELSON_1:def 20
    for a being Element of L holds
      ! a = a => - Top L;
end;

registration
  cluster satisfying_A1 satisfying_A1b satisfying_A2 satisfying_N3
  satisfying_N4 satisfying_N5 satisfying_N6 satisfying_N7
  satisfying_N8 satisfying_N9 satisfying_N10 satisfying_N11 satisfying_N12
   satisfying_N13 for bounded Lattice-like non empty NelsonStr;
end;

definition
  mode Nelson_Algebra is satisfying_A1 satisfying_A1b
  satisfying_A2 satisfying_N3
  satisfying_N4 satisfying_N5 satisfying_N6 satisfying_N7
  satisfying_N8 satisfying_N9 satisfying_N10 satisfying_N11 satisfying_N12
  satisfying_N13 bounded Lattice-like non empty NelsonStr;
end;

definition let L be satisfying_N4 bounded non empty NelsonStr,
               a, b be Element of L;
  redefine func a =-> b equals
:: NELSON_1:def 21
    (a => b) "/\" ((-b) => -a);
end;

 reserve L for Nelson_Algebra,
         a, b, c, d, x, y, z for Element of L;

theorem :: NELSON_1:6
  a [= b iff a <= b;

theorem :: NELSON_1:7
  a <= b & b <= a iff a = b;

theorem :: NELSON_1:8
  a "/\" b = Top L iff a = Top L & b = Top L;

::NdR RasiowaNonClassical: p 69 1.1 (2) <=> (4)
theorem :: NELSON_1:9  :: (2.1) (2.3 <=> 2.5)
  a <= b iff a < b & -b < -a;

theorem :: NELSON_1:10
  a "/\" b < a;

theorem :: NELSON_1:11
  a < a "\/" b;

::NdR RasiowaNonClassical: p 69 1.1 (2) <=> (3)
theorem :: NELSON_1:12  :: (2.1) (2.3 <=> 2.4)
  a <= b iff a =-> b = Top L;

::NdR RasiowaNonClassical: p 70 (38)
theorem :: NELSON_1:13
  -(a "/\" b) = (-a) "\/" (-b);

theorem :: NELSON_1:14
  (a "/\" -a) "/\" (b "\/" -b) = a "/\" -a;

theorem :: NELSON_1:15
  a <= b & b <= c implies a <= c;

theorem :: NELSON_1:16
  b <= c implies a "\/" b <= a "\/" c & a "/\" b <= a "/\" c;

theorem :: NELSON_1:17
  (-a) "\/" b <= a => b;

theorem :: NELSON_1:18
  (a => b) "/\" ((-a) "\/" b) = (-a) "\/" b;

theorem :: NELSON_1:19
  (-a) "\/" b < a => b;

theorem :: NELSON_1:20
  a "/\" (a => b) = a "/\" ((-a) "\/" b);

theorem :: NELSON_1:21
  -x < -y implies -(z => x) < -(z => y);

theorem :: NELSON_1:22
  x < y implies a "/\" (a => x) < y;

theorem :: NELSON_1:23
  x < y implies a => x < a => y;

theorem :: NELSON_1:24
  a => (b "/\" c) = (a => b) "/\" (a => c);

begin :: Properties of Nelson Algebras
:: Proven properties from Rasiowa's "Algebraic Models of Logic"
:: Items 2.3, 2.4, p. 92
:: The same set of properties, but with different numbers is also
:: in Rasiowa's "An Algebraic Appproach to Non-Classical Logic"

::NdR RasiowaNonClassical: p 69 1.2 (5)
theorem :: NELSON_1:25  :: (2.7)
  a =-> a = Top L;

::NdR RasiowaNonClassical: p 69 1.2 (6)
theorem :: NELSON_1:26  :: (2.8)
  a =-> b = Top L & b =-> c = Top L implies a =-> c = Top L;

::NdR RasiowaNonClassical: p 69 1.2 (7)
theorem :: NELSON_1:27  :: (2.9)
  a =-> b = Top L & b =-> a = Top L implies a = b;

::NdR RasiowaNonClassical: p 69 1.2 (8)
theorem :: NELSON_1:28  :: (2.10)
  a =-> Top L = Top L;

::NdR RasiowaNonClassical: p 69 1.3 (9)
theorem :: NELSON_1:29  :: (2.11)
  a => a = Top L;

::NdR RasiowaNonClassical: p 69 1.3 (10)
theorem :: NELSON_1:30  :: (2.12)
  (a => b) = (Top L) & (b => c) = (Top L) implies (a => c) = (Top L);

::NdR RasiowaNonClassical: p 69 1.3 (11)
theorem :: NELSON_1:31 :: (2.13)
  b < c implies a "\/" b < a "\/" c & a "/\" b < a "/\" c;

::NdR p 69 1.3 (12)
theorem :: NELSON_1:32 :: (2.14)
  a < b & c < d implies a "\/" c < b "\/" d & a "/\" c < b "/\" d;

::NdR RasiowaNonClassical: p 69 1.3 (13)
theorem :: NELSON_1:33  :: (2.15)
  a "/\" (a => b) < b;

::NdR RasiowaNonClassical: p 69 1.3 (14)
theorem :: NELSON_1:34  :: (2.16)
  a => (b => c) = (a "/\" b) => c;

::NdR RasiowaNonClassical: p 69 1.3 (15)
theorem :: NELSON_1:35  :: (2.17)
  a => (b => c) = b => (a => c);

::NdR RasiowaNonClassical: p 69 1.3 (16)
theorem :: NELSON_1:36  :: (2.18)
  a < ((a => b) => b);

::NdR RasiowaNonClassical: p 71 PROOF (50)
theorem :: NELSON_1:37  :: (2.19)
  a < b => (a "/\" b);

::NdR RasiowaNonClassical: p 69 (18)
theorem :: NELSON_1:38 :: RasiowaNonClassical: p 69 (17)
  a "/\" -a <= b "\/" -b;

theorem :: NELSON_1:39 :: RasiowaNonClassical: p 69 (18)
  a <= b =-> (a "/\" b);

::NdR RasiowaNonClassical: p 70 1.3 (19)
theorem :: NELSON_1:40  :: (2.20)
  a => !b = b => !a;

::NdR RasiowaNonClassical: p 70 1.3 (20)
theorem :: NELSON_1:41  :: (2.21)
  (a => Top L) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (21)
theorem :: NELSON_1:42  :: (2.22)
  ((Bottom L) => a) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (22)
theorem :: NELSON_1:43  :: (2.23)
  ((Top L) => b) = b;

::NdR RasiowaNonClassical: p 70 1.3 (23)
theorem :: NELSON_1:44  :: (2.24)
  a = Top L & a => b = Top L implies b = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (24)
theorem :: NELSON_1:45  :: (2.25)
  a => (b => a) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (25)
theorem :: NELSON_1:46  :: (2.26)
  ((a => (b => c)) => ((a => b) => (a => c))) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (26)
theorem :: NELSON_1:47  :: (2.27)
  (a => (a "\/" b)) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (27)
theorem :: NELSON_1:48  :: (2.28)
  b => (a "\/" b) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (28)
theorem :: NELSON_1:49  :: (2.29)
  (a => c) => ((b => c) => ((a "\/" b) => c)) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (29)
theorem :: NELSON_1:50  :: (2.30)
  (a "/\" b) => a = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (30)
theorem :: NELSON_1:51  :: (2.31)
  (a "/\" b) => b = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (31)
theorem :: NELSON_1:52  :: (2.32)
  (a => b) => ((a => c) => (a => (b "/\" c))) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (32)
theorem :: NELSON_1:53  :: (2.33)
  (a => !b) => (b => !a) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (33)
theorem :: NELSON_1:54  :: (2.34)
  (!(a => a)) => b = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (34)
theorem :: NELSON_1:55  :: (2.35)
  (-a) => (a => b) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (35)
theorem :: NELSON_1:56  :: (2.36)
  ((-(a => b)) => (a "/\" -b)) "/\" ((a "/\" -b) => -(a => b)) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (36)
theorem :: NELSON_1:57  :: (2.37)
  ((-!a) => a) "/\" (a => (-!a)) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (37)
theorem :: NELSON_1:58  :: (2.38)
  --a = a;

::NdR RasiowaNonClassical: p 70 1.3 (39)
theorem :: NELSON_1:59  :: (2.39)
  -(a "\/" b) = ((-a) "/\" (-b));

::NdR RasiowaNonClassical: p 70 1.3 (38)
theorem :: NELSON_1:60  :: (2.40)
  -(a "/\" b) = ((-a) "\/" (-b));

::NdR RasiowaNonClassical: p 70 1.3 (40)
theorem :: NELSON_1:61  :: (2.41)
  a < b implies b => c < a => c & c => a < c => b;

::NdR RasiowaNonClassical: p 70 1.3 (41)
theorem :: NELSON_1:62  :: (2.42)
  (a => b) => ((c => d) => ((a "/\" c) => (b "/\" d))) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (42)
theorem :: NELSON_1:63  :: (2.43)
  (a => b) => ((c => d) => ((a "\/" c) => (b "\/" d))) = Top L;

::NdR RasiowaNonClassical: p 70 1.3 (43)
theorem :: NELSON_1:64  :: (2.44)
  (b => a) => ((c => d) => ((a => c) => (b => d))) = Top L;

begin :: Alternative Equational Axiomatics by Rasiowa

definition let L be non empty NelsonStr;
  attr L is satisfying_N0* means
:: NELSON_1:def 22
    for a, b being Element of L holds
      a <= b iff a =-> b = Top L;

::NdR RasiowaNonClassical: p 75 qpB1*
  attr L is satisfying_N1* means
:: NELSON_1:def 23
    for a, b being Element of L holds
      a => (b => a) = Top L;
::NdR RasiowaNonClassical: p 75 qpB2*
  attr L is satisfying_N2* means
:: NELSON_1:def 24
    for a, b, c being Element of L holds
      (a => (b => c)) => ((a => b) => (a => c)) = Top L;
::NdR RasiowaNonClassical: p 76 qpB3*
  attr L is satisfying_N3* means
:: NELSON_1:def 25
    for a being Element of L holds
      ((Top L) => a) = a;
::NdR RasiowaNonClassical: p 76 qpB5*
  attr L is satisfying_N5* means
:: NELSON_1:def 26
    for a, b being Element of L holds
      ((a =-> b) => ((b =-> a) => b)) = ((b =-> a) => ((a =-> b) => a));
::NdR RasiowaNonClassical: p 76 qpB6*
  attr L is satisfying_N6* means
:: NELSON_1:def 27
    for a, b being Element of L holds
      a => (a "\/" b) = Top L;
::NdR RasiowaNonClassical: p 76 qpB7*
  attr L is satisfying_N7* means
:: NELSON_1:def 28
    for a, b being Element of L holds
      b => (a "\/" b) = Top L;
::NdR RasiowaNonClassical: p 77 qpB8*
  attr L is satisfying_N8* means
:: NELSON_1:def 29
    for a, b, c being Element of L holds
      (a => c) => ((b => c) => ((a "\/" b) => c)) = Top L;
::NdR RasiowaNonClassical: p 77 qpB9*
  attr L is satisfying_N9* means
:: NELSON_1:def 30
    for a, b being Element of L holds
      (a "/\" b) => a = Top L;
::NdR RasiowaNonClassical: p 77 qpB10*
  attr L is satisfying_N10* means
:: NELSON_1:def 31
    for a, b being Element of L holds
      (a "/\" b) => b = Top L;
::NdR RasiowaNonClassical: p 77 qpB11*
  attr L is satisfying_N11* means
:: NELSON_1:def 32
    for a, b, c being Element of L holds
      (a => b) => ((a => c) => (a => (b "/\" c))) = Top L;
::NdR RasiowaNonClassical: p 77 qpB12*
  attr L is satisfying_N12* means
:: NELSON_1:def 33
    for a, b being Element of L holds
      (a => !b) => (b => !a) = Top L;
::NdR RasiowaNonClassical: p 77 qpB13*
  attr L is satisfying_N13* means
:: NELSON_1:def 34
    for a, b being Element of L holds
      (!(a => a)) => b = Top L;
::NdR RasiowaNonClassical: p 77 qpB14*
  attr L is satisfying_N14* means
:: NELSON_1:def 35
    for a, b being Element of L holds
      (-a) => (a => b) = Top L;
::NdR RasiowaNonClassical: p 77 qpB15*
  attr L is satisfying_N15* means
:: NELSON_1:def 36
    for a, b being Element of L holds
      ((-(a => b)) => (a "/\" -b)) "/\" ((a "/\" -b) => -(a => b)) = Top L;
::NdR RasiowaNonClassical: p 77 qpB17*
  attr L is satisfying_N17* means
:: NELSON_1:def 37
    for a, b being Element of L holds
      -(a "\/" b) = ((-a) "/\" (-b));
::NdR RasiowaNonClassical: p 77 qpB19*
  attr L is satisfying_N19* means
:: NELSON_1:def 38
    for a being Element of L holds
      ((-!a) => a) "/\" (a => (-!a)) = Top L;
end;

notation
  let L be non empty NelsonStr;
::NdR RasiowaNonClassical: p 77 qpB4*
  synonym L is satisfying_N4* for L is satisfying_N4;
::NdR RasiowaNonClassical: p 77 qpB16*
  synonym L is satisfying_N16* for L is DeMorgan;
::NdR RasiowaNonClassical: p 77 qpB18*
  synonym L is satisfying_N18* for L is involutive;
end;

registration
  cluster -> satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4*
    satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8*
    satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12*
    satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16*
    satisfying_N17* satisfying_N18* satisfying_N19* for Nelson_Algebra;
end;

theorem :: NELSON_1:65
  for L be non empty NelsonStr st
    L is satisfying_N0* holds
  L is Nelson_Algebra iff
    L is satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4*
    satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8*
    satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12*
    satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16*
    satisfying_N17* satisfying_N18* satisfying_N19*;