:: Propositional Calculus
::  by Grzegorz Bancerek, Agata Darmochwa\l and Andrzej Trybulec
::
:: Received September 26, 1990
:: Copyright (c) 1990-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 SUBSET_1, CQC_LANG, XBOOLEAN, CQC_THE1, QC_LANG1;
 notations SUBSET_1, QC_LANG1, CQC_LANG, CQC_THE1;
 constructors CQC_THE1;
 registrations CQC_LANG;


begin

reserve A for QC-alphabet;
reserve p, q, r, s, t for Element of CQC-WFF(A);
reserve X for Subset of CQC-WFF(A);

theorem :: LUKASI_1:1
  (p => q) => ((q => r) => (p => r)) in TAUT(A);

theorem :: LUKASI_1:2
  p => q in TAUT(A) implies (q => r) => (p => r) in TAUT(A);

theorem :: LUKASI_1:3
  p => q in TAUT(A) & q => r in TAUT(A) implies p => r in TAUT(A);

theorem :: LUKASI_1:4  :: Identity law
  p => p in TAUT(A);

theorem :: LUKASI_1:5
  q => (p => q) in TAUT(A);

theorem :: LUKASI_1:6
  ((p => q) => r) => (q => r) in TAUT(A);

theorem :: LUKASI_1:7
  q => ((q => p) => p) in TAUT(A);

theorem :: LUKASI_1:8
  (s => (q => p)) => (q => (s => p)) in TAUT(A);

theorem :: LUKASI_1:9
  (q => r) => ((p => q) => (p => r)) in TAUT(A);

theorem :: LUKASI_1:10
  (q => (q => r)) => (q => r) in TAUT(A);

theorem :: LUKASI_1:11
  (p => (q => r)) => ((p => q) => (p => r)) in TAUT(A);

theorem :: LUKASI_1:12
  'not' VERUM(A) => p in TAUT(A);

theorem :: LUKASI_1:13
  q in TAUT(A) implies p => q in TAUT(A);

theorem :: LUKASI_1:14
  p in TAUT(A) implies (p => q) => q in TAUT(A);

theorem :: LUKASI_1:15
  s => (q => p) in TAUT(A) implies q => (s => p) in TAUT(A);

theorem :: LUKASI_1:16
  s => (q => p) in TAUT(A) & q in TAUT(A) implies s => p in TAUT(A);

theorem :: LUKASI_1:17
  s => (q => p) in TAUT(A) & q in TAUT(A) & s in TAUT(A) implies p in TAUT(A);

theorem :: LUKASI_1:18
  q => (q => r) in TAUT(A) implies q => r in TAUT(A);

theorem :: LUKASI_1:19
  (p => (q => r)) in TAUT(A) implies (p => q) => (p => r) in TAUT(A);

theorem :: LUKASI_1:20
  (p => (q => r)) in TAUT(A) & p => q in TAUT(A) implies p => r in TAUT(A);

theorem :: LUKASI_1:21
  (p => (q => r)) in TAUT(A) & p => q in TAUT(A) & p in TAUT(A) implies
  r in TAUT(A);

theorem :: LUKASI_1:22
  p => (q => r) in TAUT(A) & p => (r => s ) in TAUT(A) implies
   p => (q => s) in TAUT(A);

theorem :: LUKASI_1:23
  p => VERUM(A) in TAUT(A);

theorem :: LUKASI_1:24
  ('not' p => 'not' q) => (q => p) in TAUT(A);

theorem :: LUKASI_1:25
  'not' 'not' p => p in TAUT(A);

theorem :: LUKASI_1:26
  (p => q) => ('not' q => 'not' p) in TAUT(A);

theorem :: LUKASI_1:27
  p => 'not' 'not' p in TAUT(A);

theorem :: LUKASI_1:28
  ('not' 'not' p => q) => (p => q) in TAUT(A) & (p => q) => ('not'
  'not' p => q) in TAUT(A);

theorem :: LUKASI_1:29
  (p => 'not' 'not' q) => (p => q) in TAUT(A) & (p => q) => (p =>
  'not' 'not' q) in TAUT(A);

theorem :: LUKASI_1:30
  (p => 'not' q) => (q => 'not' p) in TAUT(A);

theorem :: LUKASI_1:31
  ('not' p => q) => ('not' q => p) in TAUT(A);

theorem :: LUKASI_1:32
  (p => 'not' p) => 'not' p in TAUT(A);

theorem :: LUKASI_1:33
  'not' p => (p => q) in TAUT(A);

theorem :: LUKASI_1:34
  p => q in TAUT(A) iff 'not' q => 'not' p in TAUT(A);

theorem :: LUKASI_1:35
  'not' p => 'not' q in TAUT(A) implies q => p in TAUT(A);

theorem :: LUKASI_1:36
  p in TAUT(A) iff 'not' 'not' p in TAUT(A);

theorem :: LUKASI_1:37
  (p => q) in TAUT(A) iff (p => 'not' 'not' q) in TAUT(A);

theorem :: LUKASI_1:38
  (p => q) in TAUT(A) iff ('not' 'not' p => q) in TAUT(A);

theorem :: LUKASI_1:39
  p => 'not' q in TAUT(A) implies q => 'not' p in TAUT(A);

theorem :: LUKASI_1:40
  'not' p => q in TAUT(A) implies 'not' q => p in TAUT(A);

:: predykat |- i schematy konsekwencji

registration
  let A,p,q,r;
  cluster (p => q) => ((q => r) => (p => r)) -> valid;
end;

theorem :: LUKASI_1:41
  p => q is valid implies (q => r) => (p => r) is valid;

theorem :: LUKASI_1:42
  p => q is valid & q => r is valid implies p => r is valid;

registration
  let A,p;
  cluster p => p -> valid;
end;

registration
  let A,p,q;
  cluster p => (q => p) -> valid;
end;

theorem :: LUKASI_1:43
  p is valid implies q => p is valid;

registration
  let A,p,q,s;
  cluster (s => (q => p)) => (q => (s => p)) -> valid;
end;

theorem :: LUKASI_1:44
  p => (q => r) is valid implies q => (p => r) is valid;

theorem :: LUKASI_1:45
  p => (q => r) is valid & q is valid implies p => r is valid;

theorem :: LUKASI_1:46
  p => VERUM(A) is valid & 'not' VERUM(A) => p is valid;

registration
  let A,p,q;
  cluster p => ((p => q) => q) -> valid;
end;

registration
  let A,q,r;
  cluster (q => (q => r)) => (q => r) -> valid;
end;

theorem :: LUKASI_1:47
  q => (q => r) is valid implies q => r is valid;

registration
  let A,p,q,r;
  cluster (p => (q => r)) => ((p => q) => (p => r)) -> valid;
end;

theorem :: LUKASI_1:48
  p => (q => r) is valid implies (p => q) => (p => r) is valid;

theorem :: LUKASI_1:49
  p => (q => r) is valid & p => q is valid implies p => r is valid;

registration
  let A,p,q,r;
  cluster ((p => q) => r) => (q => r) -> valid;
end;

theorem :: LUKASI_1:50
  (p => q) => r is valid implies q => r is valid;

registration
  let A,p,q,r;
  cluster (p => q) => ((r => p) => (r => q)) -> valid;
end;

theorem :: LUKASI_1:51
  p => q is valid implies (r => p) => (r => q) is valid;

registration
  let A,p,q;
  cluster (p => q) => ('not' q => 'not' p) -> valid;
end;

registration
  let A,p,q;
  cluster ('not' p => 'not' q) => (q => p) ->  valid;
end;

theorem :: LUKASI_1:52
  'not' p => 'not' q is valid iff q => p is valid;

registration
  let A,p;
  cluster p => 'not' 'not' p -> valid;
end;

registration
  let A,p;
  cluster 'not' 'not' p => p -> valid;
end;

theorem :: LUKASI_1:53
  'not' 'not' p is valid iff p is valid;

registration
  let A,p,q;
  cluster ('not' 'not' p => q) => (p => q) -> valid;
end;

theorem :: LUKASI_1:54
  'not' 'not' p => q is valid iff p => q is valid;

registration
  let A,p,q;
  cluster (p => 'not' 'not' q) => (p => q) -> valid;
end;

theorem :: LUKASI_1:55
  p => 'not' 'not' q is valid iff p => q is valid;

registration
  let A,p,q;
  cluster (p => 'not' q) => (q => 'not' p) -> valid;
end;

theorem :: LUKASI_1:56
  p => 'not' q is valid implies q => 'not' p is valid;

registration
  let A,p,q;
  cluster ('not' p => q) => ('not' q => p) -> valid;
end;

theorem :: LUKASI_1:57
  'not' p => q is valid implies 'not' q => p is valid;

theorem :: LUKASI_1:58
  X|- p => q implies X|- (q => r) => (p => r);

theorem :: LUKASI_1:59
  X|- p => q & X|- q => r implies X|- p => r;

theorem :: LUKASI_1:60
  X|- p => p;

theorem :: LUKASI_1:61
  X|- p implies X|- q => p;

theorem :: LUKASI_1:62
  X |- p implies X |- (p => q) => q;

theorem :: LUKASI_1:63
  X |- p => (q => r) implies X |- q => (p => r);

theorem :: LUKASI_1:64
  X |- p => (q => r) & X |- q implies X |- p => r;

theorem :: LUKASI_1:65
  X |- p => (p => q) implies X |- p => q;

theorem :: LUKASI_1:66
  X |- (p => q) => r implies X |- q => r;

theorem :: LUKASI_1:67
  X |- p => (q => r) implies X |- (p => q) => (p =>r);

theorem :: LUKASI_1:68
  X |- p => (q => r) & X|- p => q implies X |- p => r;

theorem :: LUKASI_1:69
  X|- 'not' p => 'not' q iff X|- q => p;

theorem :: LUKASI_1:70
  X|- 'not' 'not' p iff X|- p;

theorem :: LUKASI_1:71
  X|- p => 'not' 'not' q iff X|- p => q;

theorem :: LUKASI_1:72
  X|- 'not' 'not' p => q iff X|- p => q;

theorem :: LUKASI_1:73
  X|- p => 'not' q implies X|- q => 'not' p;

theorem :: LUKASI_1:74
  X|- 'not' p => q implies X|- 'not' q => p;

theorem :: LUKASI_1:75
  X|- p => 'not' q & X |- q implies X|- 'not' p;

theorem :: LUKASI_1:76
  X|- 'not' p => q & X |- 'not' q implies X|- p;