:: Introduction to Modal Propositional Logic
::  by Alicia de la Cruz
::
:: Received September 30, 1991
:: Copyright (c) 1991-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, SUBSET_1, TREES_2, ZFMISC_1, FINSEQ_1, XBOOLE_0,
      TREES_1, FUNCT_1, RELAT_1, ORDINAL4, NAT_1, CARD_1, XXREAL_0, PARTFUN1,
      TARSKI, ORDINAL1, ARYTM_3, FINSET_1, FUNCOP_1, MARGREL1, MCART_1,
      QC_LANG1, XBOOLEAN, VALUED_1, ZF_LANG, MODAL_1, TREES_3;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1,
      ORDINAL1, NUMBERS, WELLORD2, XCMPLX_0, NAT_1, DOMAIN_1, MCART_1, RELAT_1,
      FUNCT_1, RELSET_1, FINSEQ_1, FUNCOP_1, FINSEQ_2, FUNCT_2, FINSET_1,
      PARTFUN1, TREES_1, TREES_2, XXREAL_0, TREES_3;
 constructors PARTFUN1, WELLORD2, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2,
      TREES_2, RELSET_1, FUNCOP_1, TREES_3, XTUPLE_0, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
      XXREAL_0, XREAL_0, FINSEQ_1, TREES_1, TREES_2, CARD_1, RELSET_1, TREES_3,
      XTUPLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

reserve x,y,x1,x2,z for set,
  n,m,k for Nat,
  t1 for (DecoratedTree of [: NAT,NAT :]),
  w,s,t,u for FinSequence of NAT,
  D for non empty set;

definition
  let Z be Tree;
  func Root Z -> Element of Z equals
:: MODAL_1:def 1
  {};
end;

definition
  let D;
  let T be DecoratedTree of D;
  func Root T -> Element of D equals
:: MODAL_1:def 2
  T.(Root dom T);
end;

theorem :: MODAL_1:1
  n <> m implies not <*n*>,<*m*>^s are_c=-comparable;

::$CT

theorem :: MODAL_1:3
  n <> m implies not <*n*> is_a_proper_prefix_of <*m*>^s;

::$CT 4

theorem :: MODAL_1:8
  for Z being Tree,n,m st n <= m & <*m*> in Z holds <*n*> in Z;

theorem :: MODAL_1:9
  w^t is_a_proper_prefix_of w^s implies t is_a_proper_prefix_of s
;

theorem :: MODAL_1:10
  t1 in PFuncs(NAT*,[: NAT,NAT :]);

theorem :: MODAL_1:11
  for Z,Z1,Z2 being Tree,z being Element of Z st Z
  with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2;

theorem :: MODAL_1:12
  for Z,Z1,Z2 being (DecoratedTree of D),z being Element of dom Z st
  Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2;

theorem :: MODAL_1:13
  for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2), w being Element of Z1 st v =
  w & w is_a_proper_prefix_of p holds succ v = succ w;

theorem :: MODAL_1:14
  for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2),w being Element of Z1 st v =
  w & not p,w are_c=-comparable holds succ v = succ w;

theorem :: MODAL_1:15
  for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds for v
  being Element of Z1 with-replacement (p,Z2),w being Element of Z2 st v = p^w
  holds succ v,succ w are_equipotent;

theorem :: MODAL_1:16
  for Z1 being Tree,p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1,w being Element of Z1|p st v = p^w holds succ v,succ
  w are_equipotent;

theorem :: MODAL_1:17
  for Z being finite Tree st branchdeg (Root Z) = 0 holds card Z = 1 & Z = {{}}
;

theorem :: MODAL_1:18
  for Z being finite Tree st branchdeg (Root Z) = 1 holds succ (
  Root Z) = { <*0*> };

theorem :: MODAL_1:19
  for Z being finite Tree st branchdeg (Root Z) = 2 holds succ (
  Root Z) = { <*0*>,<*1*> };

reserve s9,w9,v9 for Element of NAT*;

theorem :: MODAL_1:20
  for Z being Tree,o being Element of Z st o <> Root Z holds Z|o,{
  o^s9: o^s9 in Z } are_equipotent & not Root Z in { o^w9 : o^w9 in Z };

theorem :: MODAL_1:21
  for Z being finite Tree,o being Element of Z st o <> Root Z
  holds card (Z|o) < card Z;

theorem :: MODAL_1:22
  for Z being finite Tree,z being Element of Z st succ (Root Z) =
  {z} holds Z = elementary_tree 1 with-replacement (<*0*>,Z|z);

theorem :: MODAL_1:23
  for Z being finite (DecoratedTree of D),z be Element of dom Z st
  succ (Root dom Z) = {z} holds Z = ((elementary_tree 1) --> Root Z)
  with-replacement (<*0*>,Z|z);

theorem :: MODAL_1:24
  for Z being Tree,x1,x2 be Element of Z st x1 = <*0*> & x2 = <*1
*> & succ (Root Z) = {x1,x2} holds Z = (elementary_tree 2 with-replacement (<*0
  *>,Z|x1)) with-replacement (<*1*>,Z|x2);

theorem :: MODAL_1:25
  for Z being (DecoratedTree of D),x1,x2 being Element of dom Z st
  x1 = <*0*> & x2 = <*1*> & succ (Root dom Z) = {x1,x2} holds Z = (((
elementary_tree 2) --> Root Z) with-replacement (<*0*>, Z|x1)) with-replacement
  (<*1*>,Z|x2);

definition
  func MP-variables -> set equals
:: MODAL_1:def 3
  [: {3},NAT :];
end;

registration
  cluster MP-variables -> non empty;
end;

definition
  mode MP-variable is Element of MP-variables;
end;

definition
  func MP-conectives -> set equals
:: MODAL_1:def 4
  [: {0,1,2},NAT :];
end;

registration
  cluster MP-conectives -> non empty;
end;

definition
  mode MP-conective is Element of MP-conectives;
end;

theorem :: MODAL_1:26
  MP-conectives misses MP-variables;

reserve p,q for MP-variable;

definition
  let T be finite Tree,v be Element of T;
  redefine func branchdeg v -> Nat;
end;

definition

  func MP-WFF -> DTree-set of [: NAT,NAT :] means
:: MODAL_1:def 5

  (for x being DecoratedTree of [: NAT,NAT :] st x in it holds x is finite) &
  for x being finite DecoratedTree of [: NAT,NAT :] holds x in it iff
  for v being Element of dom x holds branchdeg v <= 2 &
  (branchdeg v = 0 implies x .v = [0,0] or ex k st x .v = [3,k]) &
  (branchdeg v = 1 implies x .v = [1,0] or x .v = [1,1]) &
  (branchdeg v = 2 implies x .v = [2,0]);
end;

:: [0,0] = VERUM
:: [1,0] = negation
:: [1,1] = modal operator of necessity
:: [2,0] = &

definition
  mode MP-wff is Element of MP-WFF;
end;

registration
  cluster -> finite for MP-wff;
end;

reserve A,A1,B,B1,C,C1 for MP-wff;

definition
  let A;
  let a be Element of dom A;
  redefine func A|a -> MP-wff;
end;

definition
  let a be Element of MP-conectives;
  func the_arity_of a -> Nat equals
:: MODAL_1:def 6
  a`1;
end;

definition
  let D be non empty set, T,T1 be (DecoratedTree of D),
  p be FinSequence of NAT;
  assume
 p in dom T;
  func @(T,p,T1) -> DecoratedTree of D equals
:: MODAL_1:def 7

  T with-replacement (p,T1);
end;

theorem :: MODAL_1:27
  ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff;

theorem :: MODAL_1:28
  ((elementary_tree 1)-->[1,1]) with-replacement (<*0*>,A) is MP-wff;

theorem :: MODAL_1:29
  (((elementary_tree 2)-->[2,0]) with-replacement (<*0*>,A))
  with-replacement (<*1*>,B) is MP-wff;

definition
  let A;
  func 'not' A -> MP-wff equals
:: MODAL_1:def 8
  ((elementary_tree 1)-->[1,0]) with-replacement
  (<*0*>,A);
  func (#) A -> MP-wff equals
:: MODAL_1:def 9
  ((elementary_tree 1)-->[1,1]) with-replacement (
  <*0*>,A);
  let B;
  func A '&' B -> MP-wff equals
:: MODAL_1:def 10
  ((((elementary_tree 2)-->[2,0])
  with-replacement (<*0*>,A))) with-replacement (<*1*>,B);
end;

definition
  let A;
  func ? A -> MP-wff equals
:: MODAL_1:def 11
  'not' (#) 'not' A;
  let B;
  func A 'or' B -> MP-wff equals
:: MODAL_1:def 12
  'not'('not' A '&' 'not' B);
  func A => B -> MP-wff equals
:: MODAL_1:def 13
  'not'(A '&' 'not' B);
end;

theorem :: MODAL_1:30
  (elementary_tree 0) --> [3,n] is MP-wff;

theorem :: MODAL_1:31
  (elementary_tree 0) --> [0,0] is MP-wff;

definition
  let p;
  func @p -> MP-wff equals
:: MODAL_1:def 14
  (elementary_tree 0) --> p;
end;

theorem :: MODAL_1:32
  @p = @q implies p = q;

theorem :: MODAL_1:33
  'not' A = 'not' B implies A = B;

theorem :: MODAL_1:34
  (#)A = (#)B implies A = B;

theorem :: MODAL_1:35
  (A '&' B) = (A1 '&' B1) implies A = A1 & B = B1;

definition
  func VERUM -> MP-wff equals
:: MODAL_1:def 15
  (elementary_tree 0) --> [0,0];
end;

theorem :: MODAL_1:36
  card dom A = 1 implies A = VERUM or ex p st A = @p;

theorem :: MODAL_1:37
  card dom A >= 2 implies (ex B st A = 'not' B or A = (#)B) or ex
  B,C st A = B '&' C;

theorem :: MODAL_1:38
  card dom A < card dom 'not' A;

theorem :: MODAL_1:39
  card dom A < card dom (#)A;

theorem :: MODAL_1:40
  card dom A < card dom(A '&' B) & card dom B < card dom (A '&' B);

definition
  let IT be MP-wff;
  attr IT is atomic means
:: MODAL_1:def 16

  ex p st IT = @p;
  attr IT is negative means
:: MODAL_1:def 17

  ex A st IT = 'not' A;
  attr IT is necessitive means
:: MODAL_1:def 18

  ex A st IT = (#) A;
  attr IT is conjunctive means
:: MODAL_1:def 19

  ex A,B st IT = A '&' B;
end;

registration
  cluster atomic for MP-wff;
  cluster negative for MP-wff;
  cluster necessitive for MP-wff;
  cluster conjunctive for MP-wff;
end;

scheme :: MODAL_1:sch 1
  MPInd { Prop[Element of MP-WFF] }: for A being Element of MP-WFF holds Prop[
  A]
provided
 Prop[VERUM] and
 for p being MP-variable holds Prop[@p] and
 for A being Element of MP-WFF st Prop[A] holds Prop['not' A] and
 for A being Element of MP-WFF st Prop[A] holds Prop[(#) A] and
 for A, B being Element of MP-WFF st Prop[A] & Prop[B] holds Prop[A '&' B];

theorem :: MODAL_1:41
  for A being Element of MP-WFF holds A = VERUM or A is atomic MP-wff or
  A is negative MP-wff or A is necessitive MP-wff or A is conjunctive MP-wff;

theorem :: MODAL_1:42
  A = VERUM or (ex p st A = @p) or (ex B st A = 'not' B) or (ex B
  st A = (#) B) or ex B,C st A = B '&' C;

theorem :: MODAL_1:43
  @p <> 'not' A & @p <> (#)A & @p <> A '&' B;

theorem :: MODAL_1:44
  'not' A <> (#)B & 'not' A <> B '&' C;

theorem :: MODAL_1:45
  (#)A <> B '&' C;

theorem :: MODAL_1:46
  VERUM <> @p & VERUM <> 'not' A & VERUM <> (#)A & VERUM <> A '&' B;

scheme :: MODAL_1:sch 2
  MPFuncEx{ D() -> non empty set, d() -> Element of D(), F(Element of
  MP-variables) -> Element of D(), N,H(Element of D()) -> Element of D(), C((
  Element of D()),Element of D()) -> Element of D() }: ex f being Function of
MP-WFF, D() st f.VERUM = d() & (for p being MP-variable holds f.@p = F(p)) & (
  for A being Element of MP-WFF holds f.('not' A) = N(f.A)) & (for A being
  Element of MP-WFF holds f.((#)A) = H(f.A)) & for A,B being Element of MP-WFF
  holds f.(A '&' B) = C(f.A,f.B);