The Mizar abstract of CQC

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: A First-Order Predicate Calculus
by
Agata Darmochwal
Received May 25, 1990
MML identifier: CQC_THE1
[ Mizar article, MML identifier index ]
environ

 vocabulary ORDINAL2, ARYTM, BOOLE, FINSET_1, FUNCT_1, RELAT_1, MCART_1,
      FINSEQ_1, CQC_LANG, QC_LANG1, ZF_LANG, ARYTM_1, QMAX_1, CQC_THE1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0,
      RELAT_1, FUNCT_1, ORDINAL2, NAT_1, FINSET_1, FINSEQ_1, MCART_1, QC_LANG1,
      CQC_LANG;
 constructors NAT_1, CQC_LANG, XREAL_0, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, FINSET_1, RELSET_1, XREAL_0, CQC_LANG, FINSEQ_1, ARYTM_3,
      MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

:: --------- Auxiliary theorems

reserve n for natural number;

canceled;

theorem :: CQC_THE1:2
n <= 1 implies n = 0 or n = 1;

theorem :: CQC_THE1:3
n <= 2 implies n = 0 or n = 1 or n = 2;

theorem :: CQC_THE1:4
n <= 3 implies n = 0 or n = 1 or n = 2 or n = 3;

theorem :: CQC_THE1:5
n <= 4 implies n = 0 or n = 1 or n = 2 or n = 3
  or n = 4;

theorem :: CQC_THE1:6
n <= 5 implies n = 0 or n = 1 or n = 2 or n = 3
  or n = 4 or n = 5;

theorem :: CQC_THE1:7
n <= 6 implies n = 0 or n = 1 or n = 2 or n = 3
  or n = 4 or n = 5 or n = 6;

theorem :: CQC_THE1:8
n <= 7 implies n = 0 or n = 1 or n = 2 or n = 3
  or n = 4 or n = 5 or n = 6 or n = 7;

theorem :: CQC_THE1:9
n <= 8 implies n = 0 or n = 1 or n = 2 or n = 3
  or n = 4 or n = 5 or n = 6 or n = 7 or n = 8;

theorem :: CQC_THE1:10
n <= 9 implies n = 0 or n = 1 or n = 2 or n = 3
  or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9;

reserve i,j,n,k,l for Nat;
reserve a for set;

theorem :: CQC_THE1:11
{k: k <= n + 1} = {i: i <= n} \/ {n + 1};

theorem :: CQC_THE1:12
for n holds {k: k <= n} is finite;

reserve X,Y,Z for set;

theorem :: CQC_THE1:13
X is finite & X c= [:Y,Z:] implies
 ex A,B being set st A is finite & A c= Y & B is finite & B c= Z &
  X c= [:A,B:];

theorem :: CQC_THE1:14
X is finite & Z is finite & X c= [:Y,Z:] implies
 ex A being set st A is finite & A c= Y & X c= [:A,Z:];

:: --------- The axiomatic of a first-order calculus

 reserve T,S,X,Y for Subset of CQC-WFF;
 reserve p,q,r,t,F,H,G for Element of CQC-WFF;
 reserve s for QC-formula;
 reserve x,y for bound_QC-variable;

definition let T;
 attr T is being_a_theory means
:: CQC_THE1:def 1
   VERUM in T & for p,q,r,s,x,y holds
    ('not' p => p) => p in T &
    p => ('not' p => q) in T &
    (p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in T &
    (p '&' q => q '&' p in T) &
    (p in T & p => q in T implies q in T) &
    (All(x,p) => p in T) &
    (p => q in T & not x in still_not-bound_in p implies p => All(x,q) in T) &
    (s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s & s.x in T
     implies s.y in T);
  synonym T is_a_theory;
end;

canceled 10;

theorem :: CQC_THE1:25
T is_a_theory & S is_a_theory implies T /\ S is_a_theory;

:: --------- The consequence operation

definition let X;
 func Cn(X) -> Subset of CQC-WFF means
:: CQC_THE1:def 2
    t in it iff for T st T is_a_theory & X c= T holds t in T;
end;

canceled;

theorem :: CQC_THE1:27
VERUM in Cn(X);

theorem :: CQC_THE1:28
('not' p => p) => p in Cn(X);

theorem :: CQC_THE1:29
p => ('not' p => q) in Cn(X);

theorem :: CQC_THE1:30
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in Cn(X);


theorem :: CQC_THE1:31
p '&' q => q '&' p in Cn(X);

theorem :: CQC_THE1:32
p in Cn(X) & p => q in Cn(X) implies q in Cn(X);

theorem :: CQC_THE1:33
All(x,p) => p in Cn(X);

theorem :: CQC_THE1:34
  p => q in Cn(X) & not x in still_not-bound_in p implies
  p => All(x,q) in Cn(X);

theorem :: CQC_THE1:35
  s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
  s.x in Cn(X) implies s.y in Cn(X);

theorem :: CQC_THE1:36
Cn(X) is_a_theory;

theorem :: CQC_THE1:37
T is_a_theory & X c= T implies Cn(X) c= T;

theorem :: CQC_THE1:38
X c= Cn(X);

theorem :: CQC_THE1:39
X c= Y implies Cn(X) c= Cn(Y);

theorem :: CQC_THE1:40
Cn(Cn(X)) = Cn(X);

theorem :: CQC_THE1:41
T is_a_theory iff Cn(T) = T;

:: ---------- The notion of proof

definition
 func Proof_Step_Kinds -> set equals
:: CQC_THE1:def 3
    {k: k <= 9};
end;

definition
 cluster Proof_Step_Kinds -> non empty;
end;

canceled;

theorem :: CQC_THE1:43
 0 in Proof_Step_Kinds & 1 in Proof_Step_Kinds & 2 in Proof_Step_Kinds &
 3 in Proof_Step_Kinds & 4 in Proof_Step_Kinds & 5 in Proof_Step_Kinds &
 6 in Proof_Step_Kinds & 7 in Proof_Step_Kinds & 8 in Proof_Step_Kinds &
 9 in Proof_Step_Kinds;

theorem :: CQC_THE1:44
Proof_Step_Kinds is finite;

reserve f,g for FinSequence of [:CQC-WFF,Proof_Step_Kinds:];

theorem :: CQC_THE1:45
  1 <= n & n <= len f implies
 (f.n)`2 = 0 or (f.n)`2 = 1 or (f.n)`2 = 2 or (f.n)`2 = 3 or (f.n)`2 = 4
  or (f.n)`2 = 5 or (f.n)`2 = 6 or (f.n)`2 = 7 or (f.n)`2 = 8 or
   (f.n)`2 = 9;

definition let PR be (FinSequence of [:CQC-WFF,Proof_Step_Kinds:]),n,X;
 pred PR,n is_a_correct_step_wrt X means
:: CQC_THE1:def 4

 (PR.n)`1 in X if (PR.n)`2 = 0,
 (PR.n)`1 = VERUM if (PR.n)`2 = 1,
  ex p st (PR.n)`1 = ('not' p => p) => p if (PR.n)`2 = 2,
  ex p,q st (PR.n)`1 = p => ('not' p => q) if (PR.n)`2 = 3,
  ex p,q,r st (PR.n)`1 = (p => q) => ('not'(q '&' r) => 'not'(p '&' r))
                                        if (PR.n)`2 = 4,
  ex p,q st (PR.n)`1 = p '&' q => q '&' p
                                        if (PR.n)`2 = 5,
  ex p,x st (PR.n)`1 = All(x,p) => p if (PR.n)`2 = 6,
  ex i,j,p,q st 1 <= i & i < n & 1 <= j & j < i & p = (PR.j)`1 & q = (PR.n)`1 &
   (PR.i)`1 = p => q if (PR.n)`2 = 7,
  ex i,p,q,x st 1 <= i & i < n & (PR.i)`1 = p => q &
  not x in still_not-bound_in p & (PR.n)`1 = p => All(x,q)
                                        if (PR.n)`2 = 8,
  ex i,x,y,s st 1 <= i & i < n & s.x in CQC-WFF & s.y in CQC-WFF &
   not x in still_not-bound_in s & s.x = (PR.i)`1 & s.y = (PR.n)`1
                                        if (PR.n)`2 = 9;
end;

definition let X,f;
 pred f is_a_proof_wrt X means
:: CQC_THE1:def 5
   f <> {} &
  for n st 1 <= n & n <= len f holds f,n is_a_correct_step_wrt X;
end;

canceled 11;

theorem :: CQC_THE1:57
f is_a_proof_wrt X implies rng f <> {};

theorem :: CQC_THE1:58
f is_a_proof_wrt X implies 1 <= len f;

theorem :: CQC_THE1:59
f is_a_proof_wrt X implies (f.1)`2 = 0 or (f.1)`2 = 1 or
  (f.1)`2 = 2 or (f.1)`2 = 3 or (f.1)`2 = 4 or (f.1)`2 = 5 or (f.1)`2 = 6;

theorem :: CQC_THE1:60
 1 <= n & n <= len f implies
  (f,n is_a_correct_step_wrt X iff f^g,n is_a_correct_step_wrt X);

theorem :: CQC_THE1:61
 1 <= n & n <= len g & g,n is_a_correct_step_wrt X implies
  (f^g),(n+len f) is_a_correct_step_wrt X;

theorem :: CQC_THE1:62
 f is_a_proof_wrt X & g is_a_proof_wrt X implies f^g is_a_proof_wrt X;

theorem :: CQC_THE1:63
   f is_a_proof_wrt X & X c= Y implies f is_a_proof_wrt Y;

theorem :: CQC_THE1:64
f is_a_proof_wrt X & 1 <= l & l <= len f implies (f.l)`1 in Cn(X);

definition let f;
assume  f <> {};
 func Effect(f) -> Element of CQC-WFF
  equals
:: CQC_THE1:def 6
(f.(len f))`1;
end;

canceled;

theorem :: CQC_THE1:66
f is_a_proof_wrt X implies Effect(f) in Cn(X);

theorem :: CQC_THE1:67
X c= {F: ex f st f is_a_proof_wrt X & Effect(f) = F};

theorem :: CQC_THE1:68
for X holds Y = {p: ex f st f is_a_proof_wrt X & Effect(f) = p}
 implies Y is_a_theory;

theorem :: CQC_THE1:69
 for X holds {p: ex f st f is_a_proof_wrt X & Effect(f) = p} = Cn(X);

theorem :: CQC_THE1:70
p in Cn(X) iff ex f st f is_a_proof_wrt X & Effect(f) = p;

theorem :: CQC_THE1:71
p in Cn(X) implies ex Y st Y c= X & Y is finite & p in Cn(Y);

:: --------- TAUT - the set of all tautologies

definition
 canceled;

 func TAUT -> Subset of CQC-WFF equals
:: CQC_THE1:def 8
    Cn({}(CQC-WFF));
end;

canceled 2;

theorem :: CQC_THE1:74
T is_a_theory implies TAUT c= T;

theorem :: CQC_THE1:75
TAUT c= Cn(X);

theorem :: CQC_THE1:76
TAUT is_a_theory;

theorem :: CQC_THE1:77
VERUM in TAUT;

theorem :: CQC_THE1:78
('not' p => p) =>p in TAUT;

theorem :: CQC_THE1:79
p => ('not' p => q) in TAUT;

theorem :: CQC_THE1:80
(p => q) => ('not'(q '&' r) => 'not'
(p '&' r)) in TAUT;

theorem :: CQC_THE1:81
p '&' q => q '&' p in TAUT;

theorem :: CQC_THE1:82
p in TAUT & p => q in TAUT implies q in TAUT;

theorem :: CQC_THE1:83
All(x,p) => p in TAUT;

theorem :: CQC_THE1:84
p => q in TAUT & not x in still_not-bound_in p implies
  p => All(x,q) in TAUT;

theorem :: CQC_THE1:85
s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
  s.x in TAUT implies s.y in TAUT;

:: --------- Relation of consequence of a set of formulas

definition let X,s;
 pred X|-s means
:: CQC_THE1:def 9
  s in Cn(X);
end;

canceled;

theorem :: CQC_THE1:87
X |- VERUM;

theorem :: CQC_THE1:88
X |- ('not' p => p) => p;

theorem :: CQC_THE1:89
X |- p => ('not' p => q);

theorem :: CQC_THE1:90
X |- (p => q) => ('not'(q '&' r) => 'not'(p '&' r));

theorem :: CQC_THE1:91
X |- p '&' q => q '&' p;

theorem :: CQC_THE1:92
X |- p & X |- p => q implies X |- q;

theorem :: CQC_THE1:93
X |- All(x,p) => p;

theorem :: CQC_THE1:94
X |- p => q & not x in still_not-bound_in p implies
         X |- p => All(x,q);

theorem :: CQC_THE1:95
s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
 X |- s.x implies X |- s.y;

definition let s;
 attr s is valid means
:: CQC_THE1:def 10
  {}(CQC-WFF)|-s;
  synonym |-s;
end;

definition let s;
 redefine attr s is valid means
:: CQC_THE1:def 11
s in TAUT;
end;

canceled 2;

theorem :: CQC_THE1:98
|- p implies X|- p;

theorem :: CQC_THE1:99
|- VERUM;

theorem :: CQC_THE1:100
|- ('not' p => p) =>p;

theorem :: CQC_THE1:101
|- p => ('not' p => q);

theorem :: CQC_THE1:102
|- (p => q) => ('not'(q '&' r) => 'not'(p '&' r));

theorem :: CQC_THE1:103
|- p '&' q => q '&' p;

theorem :: CQC_THE1:104
|- p & |- p => q implies |- q;

theorem :: CQC_THE1:105
|- All(x,p) => p;

theorem :: CQC_THE1:106
|- p => q & not x in still_not-bound_in p implies |- p => All(x,q);

theorem :: CQC_THE1:107
s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
 |- s.x implies |- s.y;
The abstract of the Mizar article:

A First-Order Predicate Calculus
