:: Grzegorczyk's Logics, Part 1
:: by Taneli Huuskonen
::
:: Received April 30, 2015
:: Copyright (c) 2015-2026 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, XBOOLE_0, FINSEQ_1, XXREAL_0, TARSKI, ARYTM_3,
CARD_1, ORDINAL4, FUNCT_1, XBOOLEAN, RELAT_1, NAT_1, ZF_LANG, GRZLOG_1,
POLNOT_1, ZFMISC_1, FOMODEL2, FINSET_1, CQC_THE1, EQREL_1, SETFAM_1,
BINOP_1;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1,
NAT_1, NUMBERS, FINSEQ_1,
ENUMSET1, ZFMISC_1, POLNOT_1, FUNCT_2, BINOP_1, RELSET_1, XXREAL_0,
XCMPLX_0, FINSET_1, EQREL_1, SETFAM_1;
constructors NAT_1, NUMBERS, ENUMSET1, FINSEQ_1, POLNOT_1, RELSET_1, XREAL_0,
EQREL_1;
registrations ORDINAL1, RELSET_1, FINSEQ_1, XBOOLE_0, FUNCT_1, NAT_1, XREAL_0,
FINSET_1, EQREL_1;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, POLNOT_1;
expansions TARSKI, FINSEQ_1, SUBSET_1;
theorems TARSKI, FUNCT_1, NAT_1, FINSEQ_1, XBOOLE_0, XREAL_1, XXREAL_0,
ORDINAL1, XBOOLE_1, POLNOT_1, ENUMSET1, ZFMISC_1, FUNCT_2, EQREL_1,
RELSET_1;
schemes FUNCT_2, FINSET_1, XBOOLE_0, EQREL_1, BINOP_1;
begin
reserve k,m,n for Element of NAT,
i, j for Nat,
a, b, c for object,
X, Y, Z for set,
D, D1, D2 for non empty set;
reserve p, q, r, s for FinSequence;
::
:: The Construction of Grzegorczyk's LD Language
::
definition
func VAR -> FinSequence-membered set equals
the set of all <*0,k*> where k is Element of NAT;
coherence
proof
set X = the set of all <*0,k*> where k is Element of NAT;
for a st a in X holds a is FinSequence
proof
let a;
assume a in X;
then consider k such that A1: a = <*0, k*>;
thus thesis by A1;
end;
hence thesis by FINSEQ_1:def 19;
end;
end;
registration
cluster VAR -> non empty antichain-like;
coherence
proof
<*0, the Element of NAT*> in VAR;
hence VAR is non empty;
for p st p in VAR holds dom p = { 1, 2 }
proof
let p;
assume p in VAR;
then consider k such that A2: p = <*0, k*>;
thus thesis by A2, FINSEQ_1:92;
end;
hence thesis by POLNOT_1:45;
end;
end;
definition
mode Variable is Element of VAR;
end;
Lm1:
for a being Variable holds a.1 = 0
proof
let a be Variable;
a in VAR;
then consider k such that A1: a = <* 0, k *>;
thus thesis by A1;
end;
definition
func 'not' -> FinSequence equals <*1*>;
coherence;
func '&' -> FinSequence equals <*2*>;
coherence;
func '=' -> FinSequence equals <*3*>;
coherence;
end;
definition
func GRZ-ops -> non empty FinSequence-membered set equals
{ 'not', '&', '=' };
coherence
proof
set X = { 'not', '&', '=' };
X is FinSequence-membered by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
end;
Lm2:
for p being Element of GRZ-ops holds dom p = Seg 1 & p.1 <> 0
proof
let p be Element of GRZ-ops;
A1: p = 'not' implies thesis by FINSEQ_1:def 8;
A2: p = '&' implies thesis by FINSEQ_1:def 8;
p = '=' implies thesis by FINSEQ_1:def 8;
hence thesis by A1, A2, ENUMSET1:def 1;
end;
definition
redefine func GRZ-ops -> Polish-language; :: redefines GRZ-ops (GRZLOG_1, definition)
coherence
proof
for p st p in GRZ-ops holds dom p = Seg 1 by Lm2;
hence thesis by POLNOT_1:45;
end;
end;
definition
func GRZ-symbols -> non empty FinSequence-membered set equals
VAR \/ GRZ-ops;
coherence;
end;
definition
redefine func 'not' -> Element of GRZ-symbols; :: redefines 'not' (GRZLOG_1, definition)
coherence
proof
'not' in GRZ-ops by ENUMSET1:def 1;
hence thesis by XBOOLE_0:def 3;
end;
redefine func '&' -> Element of GRZ-symbols; :: redefines '&' (GRZLOG_1, definition)
coherence
proof
'&' in GRZ-ops by ENUMSET1:def 1;
hence thesis by XBOOLE_0:def 3;
end;
redefine func '=' -> Element of GRZ-symbols; :: redefines '=' (GRZLOG_1, definition)
coherence
proof
'=' in GRZ-ops by ENUMSET1:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
Lm3:
for p being Element of GRZ-symbols holds p.1 = 0 iff p in VAR
proof
let p be Element of GRZ-symbols;
thus p.1 = 0 implies p in VAR
proof
assume p.1 = 0;
then not p in GRZ-ops by Lm2;
hence thesis by XBOOLE_0:def 3;
end;
thus p in VAR implies p.1 = 0 by Lm1;
end;
Lm4:
not ex a st a in VAR & a in GRZ-ops
proof
given a such that A1: a in VAR and A2: a in GRZ-ops;
reconsider p = a as Element of GRZ-symbols by A1, XBOOLE_0:def 3;
p.1 = 0 by A1, Lm1;
hence contradiction by A2, Lm2;
end;
theorem Th1:
'not' <> '&' & 'not' <> '=' & '&' <> '='
proof
A1: 'not'.1 = 1;
'&'.1 = 2;
hence thesis by A1, FINSEQ_1:def 8;
end;
Th3:
GRZ-symbols is non trivial antichain-like
proof
thus GRZ-symbols is non trivial by Th1;
let p, q;
set r = p^q;
assume that A1: p in GRZ-symbols and A2: r in GRZ-symbols;
reconsider p as Element of GRZ-symbols by A1;
reconsider r as Element of GRZ-symbols by A2;
per cases;
suppose p.1 = 0;
then A4: p in VAR by Lm3;
then consider k such that A5: p = <* 0, k *>;
r = (<*0*>^<*k*>)^q by A5, FINSEQ_1:def 9
.= <*0*>^(<*k*>^q) by FINSEQ_1:32;
then r.1 = 0 by FINSEQ_1:41;
then r in VAR by Lm3;
hence thesis by A4, POLNOT_1:def 16;
end;
suppose A10: p.1 <> 0;
then not p in VAR by Lm3;
then A11: p in GRZ-ops by XBOOLE_0:def 3;
then dom p = Seg 1 by Lm2;
then 1 in dom p by FINSEQ_1:1;
then r.1 = p.1 by FINSEQ_1:def 7;
then not r in VAR by A10, Lm3;
then r in GRZ-ops by XBOOLE_0:def 3;
hence thesis by A11, POLNOT_1:def 16;
end;
end;
registration
cluster GRZ-symbols -> non trivial antichain-like;
coherence by Th3;
end;
definition
func GRZ-op-arity -> Function of GRZ-ops, NAT means
:Def3:
it.'not' = 1 & it.'&' = 2 & it.'=' = 2;
existence
proof
defpred X[ object, object ] means
($1 = 'not' & $2 = 1) or (($1 = '&' or $1 = '=') & $2 = 2);
A10: for a st a in GRZ-ops ex b st b in NAT & X[a, b]
proof
let a;
assume a in GRZ-ops;
then a = 'not' or a = '&' or a = '=' by ENUMSET1:def 1;
hence thesis;
end;
consider f being Function of GRZ-ops, NAT such that
A21: for a st a in GRZ-ops holds X[a, f.a]
from FUNCT_2:sch 1(A10);
take f;
'not' in GRZ-ops & '&' in GRZ-ops & '=' in GRZ-ops by ENUMSET1:def 1;
hence thesis by A21, Th1;
end;
uniqueness
proof
let f, g be Function of GRZ-ops, NAT such that
A1: f.'not' = 1 & f.'&' = 2 & f.'=' = 2 and
A2: g.'not' = 1 & g.'&' = 2 & g.'=' = 2;
dom f = GRZ-ops by FUNCT_2:def 1;
then A11: dom f = dom g by FUNCT_2:def 1;
for a st a in dom f holds f.a = g.a
proof
let a;
assume a in dom f;
then a = 'not' or a = '&' or a = '=' by ENUMSET1:def 1;
hence thesis by A1, A2;
end;
hence thesis by A11, FUNCT_1:2;
end;
end;
definition
func GRZ-arity -> Polish-arity-function of GRZ-symbols means
:Def4:
for a st a in GRZ-symbols holds
((a in GRZ-ops implies it.a = GRZ-op-arity.a)
& (not a in GRZ-ops implies it.a = 0));
existence
proof
defpred X[ object, object ] means
($1 in GRZ-ops implies $2 = GRZ-op-arity.$1)
& (not $1 in GRZ-ops implies $2 = 0);
A1: for a st a in GRZ-symbols ex b st b in NAT & X[a, b]
proof
let a;
assume a in GRZ-symbols;
per cases;
suppose not a in GRZ-ops;
hence thesis;
end;
suppose A5: a in GRZ-ops;
take GRZ-op-arity.a;
thus thesis by A5, FUNCT_2:5;
end;
end;
consider f being Function of GRZ-symbols, NAT such that
A10: for a st a in GRZ-symbols holds X[a, f.a] from FUNCT_2:sch 1(A1);
set p = the Element of VAR;
A11: p in GRZ-symbols by XBOOLE_0:def 3;
not p in GRZ-ops by Lm4;
then f.p = 0 by A10, A11;
then reconsider f as Polish-arity-function of GRZ-symbols
by A11, POLNOT_1:def 18;
take f;
let a;
assume a in GRZ-symbols;
hence thesis by A10;
end;
uniqueness
proof
let f1, f2 be Polish-arity-function of GRZ-symbols;
assume that
A1: for a st a in GRZ-symbols holds
((a in GRZ-ops implies f1.a = GRZ-op-arity.a)
& (not a in GRZ-ops implies f1.a = 0)) and
A2: for a st a in GRZ-symbols holds
((a in GRZ-ops implies f2.a = GRZ-op-arity.a)
& (not a in GRZ-ops implies f2.a = 0));
dom f1 = GRZ-symbols by FUNCT_2:def 1;
then A3: dom f1 = dom f2 by FUNCT_2:def 1;
for a st a in dom f1 holds f1.a = f2.a
proof
let a;
assume A4: a in dom f1;
per cases;
suppose A5: a in GRZ-ops;
hence f1.a = GRZ-op-arity.a by A1, A4 .= f2.a by A2, A4, A5;
end;
suppose A6: not a in GRZ-ops;
hence f1.a = 0 by A1, A4 .= f2.a by A2, A4, A6;
end;
end;
hence thesis by A3, FUNCT_1:2;
end;
end;
Lm10:
for a st a in GRZ-ops holds GRZ-arity.a = GRZ-op-arity.a
proof
let a;
assume A1: a in GRZ-ops;
then a in GRZ-symbols by XBOOLE_0:def 3;
hence thesis by A1, Def4;
end;
theorem Th4:
GRZ-arity.'not' = 1 & GRZ-arity.'&' = 2 & GRZ-arity.'=' = 2
proof
'not' in GRZ-ops by ENUMSET1:def 1;
hence GRZ-arity.'not' = GRZ-op-arity.'not' by Lm10 .= 1 by Def3;
'&' in GRZ-ops by ENUMSET1:def 1;
hence GRZ-arity.'&' = GRZ-op-arity.'&' by Lm10 .= 2 by Def3;
'=' in GRZ-ops by ENUMSET1:def 1;
hence GRZ-arity.'=' = GRZ-op-arity.'=' by Lm10 .= 2 by Def3;
end;
theorem Th5:
Polish-atoms(GRZ-symbols, GRZ-arity) = VAR
proof
set X = Polish-atoms(GRZ-symbols, GRZ-arity);
thus X c= VAR
proof
let a;
assume A11: a in X;
then GRZ-arity.a = 0 by POLNOT_1:def 7;
then A13: not a in GRZ-ops by Th4, ENUMSET1:def 1;
a in GRZ-symbols by A11, POLNOT_1:def 7;
hence thesis by A13, XBOOLE_0:def 3;
end;
let a;
assume A2: a in VAR;
then A3: a in GRZ-symbols by XBOOLE_0:def 3;
not a in GRZ-ops by A2, Lm4;
then GRZ-arity.a = 0 by A3, Def4;
hence a in X by A3, POLNOT_1:def 7;
end;
definition
func GRZ-formula-set -> Polish-language of GRZ-symbols equals
Polish-WFF-set(GRZ-symbols, GRZ-arity);
coherence;
mode GRZ-formula is Polish-WFF of GRZ-symbols, GRZ-arity;
end;
registration
cluster non empty for Subset of GRZ-formula-set;
existence
proof
set X = GRZ-formula-set;
X c= X;
then reconsider X as Subset of GRZ-formula-set;
take X;
thus thesis;
end;
end;
definition
let n;
func x.n -> GRZ-formula equals
<*0, n*>;
coherence
proof
A1: <*0, n*> in Polish-atoms(GRZ-symbols, GRZ-arity) by Th5;
Polish-atoms(GRZ-symbols, GRZ-arity)
c= Polish-expression-set(GRZ-symbols, GRZ-arity) by POLNOT_1:36;
hence thesis by A1, POLNOT_1:def 25;
end;
end;
reserve t, u, v, w for GRZ-formula;
definition
let t;
func 'not' t -> GRZ-formula equals
Polish-unOp(GRZ-symbols, GRZ-arity, 'not').t;
coherence;
let u;
func t '&' u -> GRZ-formula equals
Polish-binOp(GRZ-symbols, GRZ-arity, '&').(t, u);
coherence;
func t '=' u -> GRZ-formula equals
Polish-binOp(GRZ-symbols, GRZ-arity, '=').(t, u);
coherence;
end;
definition
let t, u;
func t 'or' u -> GRZ-formula equals
'not' (('not' t) '&' ('not' u));
coherence;
func t => u -> GRZ-formula equals
t '=' (t '&' u);
coherence;
end;
definition
let t, u;
func t <=> u -> GRZ-formula equals
(t => u) '&' (u => t);
coherence;
end;
definition
let t;
attr t is atomic means
t in Polish-atoms(GRZ-symbols, GRZ-arity);
attr t is negative means
Polish-WFF-head t = 'not';
attr t is conjunctive means
Polish-WFF-head t = '&';
attr t is being_equality means
Polish-WFF-head t = '=';
end;
theorem
for t holds t is atomic iff t in VAR by Th5;
theorem
for t holds t is negative iff ex u st t = 'not' u
proof
let t;
thus t is negative implies ex u st t = 'not' u
proof
assume t is negative;
then consider u such that
A3: t = Polish-unOp(GRZ-symbols, GRZ-arity, 'not').u
by Th4, POLNOT_1:80;
take u;
thus thesis by A3;
end;
thus thesis by Th4, POLNOT_1:81;
end;
theorem
for t holds t is conjunctive iff ex u, v st t = u '&' v
proof
let t;
thus t is conjunctive implies ex u, v st t = u '&' v
proof
assume t is conjunctive;
then consider u, v such that
A3: t = Polish-binOp(GRZ-symbols, GRZ-arity, '&').(u, v)
by Th4, POLNOT_1:82;
take u, v;
thus thesis by A3;
end;
thus thesis by Th4, POLNOT_1:83;
end;
theorem
for t holds t is being_equality iff ex u, v st t = u '=' v
proof
let t;
thus t is being_equality implies ex u, v st t = u '=' v
proof
assume t is being_equality;
then consider u, v such that
A3: t = Polish-binOp(GRZ-symbols, GRZ-arity, '=').(u, v)
by Th4, POLNOT_1:82;
take u, v;
thus thesis by A3;
end;
thus thesis by Th4, POLNOT_1:83;
end;
theorem
for t holds
t is atomic or t is negative or t is conjunctive or t is being_equality
proof
let t;
set s = Polish-WFF-head t;
assume A1: not thesis;
then not s in GRZ-ops by ENUMSET1:def 1;
then A2: s in VAR by XBOOLE_0:def 3;
s = GRZ-symbols-head t by POLNOT_1:def 33;
hence contradiction by A1, A2, Th5, POLNOT_1:69;
end;
registration
cluster atomic -> non negative for GRZ-formula;
coherence
proof
let t;
assume A1: t is atomic;
assume t is negative; then
Polish-arity t = 1 by Th4, POLNOT_1:def 35;
hence contradiction by A1, POLNOT_1:84;
end;
cluster atomic -> non conjunctive for GRZ-formula;
coherence
proof
let t;
assume A1: t is atomic;
assume t is conjunctive; then
Polish-arity t = 2 by Th4, POLNOT_1:def 35;
hence contradiction by A1, POLNOT_1:84;
end;
cluster atomic -> non being_equality for GRZ-formula;
coherence
proof
let t;
assume A1: t is atomic;
assume t is being_equality; then
Polish-arity t = 2 by Th4, POLNOT_1:def 35;
hence contradiction by A1, POLNOT_1:84;
end;
cluster negative -> non conjunctive for GRZ-formula;
coherence by Th1;
cluster negative -> non being_equality for GRZ-formula;
coherence by Th1;
cluster conjunctive -> non being_equality for GRZ-formula;
coherence by Th1;
end;
begin
definition
func GRZ-axioms -> non empty Subset of GRZ-formula-set means
:Def10:
for a holds a in it iff ex t, u, v st
a = 'not'(t '&' 'not' t) or
a = ('not' 'not' t) '=' t or
a = t '=' (t '&' t) or
a = (t '&' u) '=' (u '&' t) or
a = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or
a = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or
a = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or
a = (t '=' u) '=' (u '=' t) or
a = (t '=' u) '=' (('not' t) '=' ('not' u));
existence
proof
defpred P[ object ] means ex t, u, v st
$1 = 'not'(t '&' 'not' t) or
$1 = ('not' 'not' t) '=' t or
$1 = t '=' (t '&' t) or
$1 = (t '&' u) '=' (u '&' t) or
$1 = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or
$1 = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or
$1 = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or
$1 = (t '=' u) '=' (u '=' t) or
$1 = (t '=' u) '=' (('not' t) '=' ('not' u));
consider X being set such that
A1: for a holds a in X iff a in GRZ-formula-set & P[ a ]
from XBOOLE_0:sch 1;
A2: ('not' 'not' x.1) '=' x.1 in X by A1;
X c= GRZ-formula-set by A1;
then reconsider X as non empty Subset of GRZ-formula-set by A2;
take X;
thus thesis by A1;
end;
uniqueness
proof
defpred P[ object ] means ex t, u, v st
$1 = 'not'(t '&' 'not' t) or
$1 = ('not' 'not' t) '=' t or
$1 = t '=' (t '&' t) or
$1 = (t '&' u) '=' (u '&' t) or
$1 = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or
$1 = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or
$1 = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or
$1 = (t '=' u) '=' (u '=' t) or
$1 = (t '=' u) '=' (('not' t) '=' ('not' u));
let X1, X2 be non empty Subset of GRZ-formula-set;
assume that
A1: for a holds a in X1 iff P[ a ] and
A2: for a holds a in X2 iff P[ a ];
thus X1 = X2 from XBOOLE_0:sch 2(A1, A2);
end;
func LD-specific-axioms -> non empty Subset of GRZ-formula-set means
:Def11:
for a holds a in it iff ex t, u, v st
a = (t '=' u) => ((t '&' v) '=' (u '&' v)) or
a = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or
a = (t '=' u) => ((t '=' v) '=' (u '=' v));
existence
proof
defpred P[ object ] means ex t, u, v st
$1 = (t '=' u) => ((t '&' v) '=' (u '&' v)) or
$1 = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or
$1 = (t '=' u) => ((t '=' v) '=' (u '=' v));
consider X being set such that
A1: for a holds a in X iff a in GRZ-formula-set & P[ a ]
from XBOOLE_0:sch 1;
A2: (x.1 '=' x.1) => ((x.1 '&' x.1) '=' (x.1 '&' x.1)) in X by A1;
X c= GRZ-formula-set by A1;
then reconsider X as non empty Subset of GRZ-formula-set by A2;
take X;
thus thesis by A1;
end;
uniqueness
proof
defpred P[ object ] means ex t, u, v st
$1 = (t '=' u) => ((t '&' v) '=' (u '&' v)) or
$1 = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or
$1 = (t '=' u) => ((t '=' v) '=' (u '=' v));
let X1, X2 be non empty Subset of GRZ-formula-set;
assume that
A1: for a holds a in X1 iff P[ a ] and
A2: for a holds a in X2 iff P[ a ];
thus X1 = X2 from XBOOLE_0:sch 2(A1, A2);
end;
end;
definition
func LD-axioms -> non empty Subset of GRZ-formula-set equals
GRZ-axioms \/ LD-specific-axioms;
coherence;
end;
definition
mode GRZ-rule is Relation of (bool GRZ-formula-set), GRZ-formula-set;
end;
reserve R, R1, R2 for GRZ-rule;
definition
let R1, R2;
redefine func R1 \/ R2 -> GRZ-rule; :: redefines \/ (XBOOLE_0, definition)
coherence by XBOOLE_1:8;
end;
definition
func GRZ-MP -> GRZ-rule equals
the set of all [{t,t '=' u}, u] where t is GRZ-formula, u is GRZ-formula;
coherence
proof
set X = GRZ-formula-set;
set Y = [: bool X, X :];
set Z = the set of all [{t, t '=' u}, u] where
t is GRZ-formula, u is GRZ-formula;
for a st a in Z holds a in Y
proof
let a;
assume a in Z;
then consider t, u being GRZ-formula such that
A2: a = [{t, t '=' u}, u];
set w = {t, t '=' u};
t in X & t '=' u in X;
then w c= X by TARSKI:def 2;
then w in bool X by ZFMISC_1:def 1;
hence thesis by A2, ZFMISC_1:def 2;
end;
then Z c= Y;
hence thesis;
end;
func GRZ-ConjIntro -> GRZ-rule equals
the set of all [{t,u}, t '&' u] where t is GRZ-formula, u is GRZ-formula;
coherence
proof
set X = GRZ-formula-set;
set Y = [: bool X, X :];
set Z = the set of all [{t, u}, t '&' u] where t is GRZ-formula,
u is GRZ-formula;
Z c= Y
proof
let a;
assume a in Z;
then consider t, u being GRZ-formula such that
A2: a = [{t, u}, t '&' u];
set w = {t, u};
t in X & u in X;
then w c= X by TARSKI:def 2;
then w in bool X by ZFMISC_1:def 1;
hence thesis by A2, ZFMISC_1:def 2;
end;
hence thesis;
end;
func GRZ-ConjElimL -> GRZ-rule equals
the set of all [{t '&' u}, t] where t is GRZ-formula, u is GRZ-formula;
coherence
proof
set X = GRZ-formula-set;
set Y = [: bool X, X :];
set Z = the set of all [{t '&' u}, t] where t is GRZ-formula,
u is GRZ-formula;
Z c= Y
proof
let a;
assume a in Z;
then consider t, u being GRZ-formula such that
A2: a = [{t '&' u}, t];
set w = {t '&' u};
t '&' u in X;
then w c= X by TARSKI:def 1;
then w in bool X by ZFMISC_1:def 1;
hence thesis by A2, ZFMISC_1:def 2;
end;
hence thesis;
end;
func GRZ-ConjElimR -> GRZ-rule equals
the set of all [{t '&' u}, u] where t is GRZ-formula, u is GRZ-formula;
coherence
proof
set X = GRZ-formula-set;
set Y = [: bool X, X :];
set Z = the set of all
[{t '&' u}, u] where t is GRZ-formula, u is GRZ-formula;
Z c= Y
proof
let a;
assume a in Z;
then consider t, u being GRZ-formula such that
A2: a = [{t '&' u}, u];
set w = {t '&' u};
t '&' u in X;
then w c= X by TARSKI:def 1;
then w in bool X by ZFMISC_1:def 1;
hence thesis by A2, ZFMISC_1:def 2;
end;
hence thesis;
end;
end;
definition
func GRZ-rules -> GRZ-rule means
:Def35:
for a holds a in it iff a in GRZ-MP or a in GRZ-ConjIntro
or a in GRZ-ConjElimL or a in GRZ-ConjElimR;
existence
proof
set W = GRZ-formula-set;
set U = [: bool W, W :];
defpred P[ object ] means $1 in GRZ-MP or $1 in GRZ-ConjIntro
or $1 in GRZ-ConjElimL or $1 in GRZ-ConjElimR;
consider X being set such that
A1: for a holds a in X iff a in U & P[ a ]
from XBOOLE_0:sch 1;
X c= U by A1;
then reconsider X as GRZ-rule;
take X;
thus thesis by A1;
end;
uniqueness
proof
defpred P[ object ] means $1 in GRZ-MP or $1 in GRZ-ConjIntro
or $1 in GRZ-ConjElimL or $1 in GRZ-ConjElimR;
let X1, X2 be GRZ-rule;
assume that
A1: for a holds a in X1 iff P[ a ] and
A2: for a holds a in X2 iff P[ a ];
thus X1 = X2 from XBOOLE_0:sch 2(A1, A2);
end;
end;
definition
mode GRZ-formula-sequence is FinSequence of GRZ-formula-set;
mode GRZ-formula-finset is finite Subset of GRZ-formula-set;
end;
reserve A, A1, A2 for non empty Subset of GRZ-formula-set;
reserve B, B1, B2 for Subset of GRZ-formula-set;
reserve P, P1, P2 for GRZ-formula-sequence;
reserve S, S1, S2 for GRZ-formula-finset;
definition
let S1, S2;
redefine func S1 \/ S2 -> GRZ-formula-finset; :: redefines \/ (XBOOLE_0, definition)
coherence
proof
set S = S1 \/ S2;
thus S is finite Subset of GRZ-formula-set;
end;
end;
definition
let A, R, P, n;
pred P, n is_a_correct_step_wrt A, R means
(P.n in A or ex Q being GRZ-formula-finset st
([Q, P.n] in R & for q st q in Q ex k st k in dom P & k < n & P.k = q));
end;
definition
let A, R, P;
attr P is (A, R)-correct means
for k st k in dom P holds P, k is_a_correct_step_wrt A, R;
end;
definition
let A;
let a be Element of A;
redefine func <*a*> -> GRZ-formula-sequence; :: redefines <* (FINSEQ_1, definition)
coherence
proof
reconsider b = a as Element of GRZ-formula-set;
<*a*>=<*b*>;
hence <*a*> is FinSequence of GRZ-formula-set;
end;
end;
theorem Th40:
for A, R for a being Element of A holds <*a*> is (A, R)-correct
proof
let A, R;
let a be Element of A;
set P = <*a*>;
let k;
assume k in dom P;
then P.k in rng P by FUNCT_1:3;
then P.k in {a} by FINSEQ_1:38;
then P.k = a by TARSKI:def 1;
hence <*a*>, k is_a_correct_step_wrt A, R;
end;
registration
let A, R;
cluster non empty (A, R)-correct for GRZ-formula-sequence;
existence
proof
set P = <*the Element of A*>;
take P;
thus P is non empty;
thus P is (A, R)-correct by Th40;
end;
end;
definition
let A, R, S;
attr S is (A, R)-correct means
ex P st S = rng P & P is (A, R)-correct;
end;
Lm40:
for p, q, k, m st k in dom p & m in dom q & m < k holds m in dom p
proof
let p, q, k, m;
assume that
A1: k in dom p and
A2: m in dom q and
A3: m < k;
A4: dom p = Seg len p by FINSEQ_1:def 3;
A5: dom q = Seg len q by FINSEQ_1:def 3;
A6: 1 <= m by A2, A5, FINSEQ_1:1;
k <= len p by A1, A4, FINSEQ_1:1;
then m <= len p by A3, XXREAL_0:2;
hence thesis by A4, A6, FINSEQ_1:1;
end;
Lm41:
for A, R, P, P1, P2, n st n in dom P & P^P1, n is_a_correct_step_wrt A, R
holds P^P2, n is_a_correct_step_wrt A, R
proof
let A, R, P, P1, P2, n;
assume that
A1: n in dom P and
A2: P^P1, n is_a_correct_step_wrt A, R;
A3: P.n = (P^P1).n by A1, FINSEQ_1:def 7;
A4: P.n = (P^P2).n by A1, FINSEQ_1:def 7;
per cases by A2, A3;
suppose P.n in A;
hence thesis by A4;
end;
suppose ex Q being GRZ-formula-finset st
([Q, P.n] in R
& for q st q in Q ex m st m in dom (P^P1) & m < n & (P^P1).m = q);
then consider Q being GRZ-formula-finset such that
A10: [Q, P.n] in R and
A11: for q st q in Q ex m st m in dom (P^P1) & m < n & (P^P1).m = q;
A13: for q st q in Q ex m st m in dom (P^P2) & m < n & (P^P2).m = q
proof
let q;
assume q in Q;
then consider m such that
A14: m in dom (P^P1) and
A15: m < n and
A16: (P^P1).m = q
by A11;
take m;
A20: m in dom P by A1, A14, A15, Lm40;
dom P c= dom (P^P2) by FINSEQ_1:26;
hence m in dom (P^P2) by A20;
thus m < n by A15;
thus (P^P2).m = P.m by A20, FINSEQ_1:def 7
.= q by A16, A20, FINSEQ_1:def 7;
end;
thus thesis by A4, A10, A13;
end;
end;
theorem
for A, R, P, P1, P2 st P is (A, R)-correct & P = P1^P2 holds
P1 is (A, R)-correct
proof
let A, R, P, P1, P2;
assume that
A1: P is (A, R)-correct and
A2: P = P1^P2;
set P0 = <*>GRZ-formula-set;
let k;
assume A3: k in dom P1;
dom P1 c= dom P by A2, FINSEQ_1:26;
then P1^P0, k is_a_correct_step_wrt A, R by A1, A2, A3, Lm41;
hence P1, k is_a_correct_step_wrt A, R by FINSEQ_1:34;
end;
theorem Th42:
for A, R, P1, P2 st P1 is (A, R)-correct & P2 is (A, R)-correct holds
P1^P2 is (A, R)-correct
proof
let A, R, P1, P2;
set P0 = <*>GRZ-formula-set;
assume that
A1: P1 is (A, R)-correct and
A2: P2 is (A, R)-correct;
let k;
assume A3: k in dom (P1^P2);
per cases;
suppose A5: k in dom P1;
then P1, k is_a_correct_step_wrt A, R by A1;
then P1^P0, k is_a_correct_step_wrt A, R by FINSEQ_1:34;
hence P1^P2, k is_a_correct_step_wrt A, R by A5, Lm41;
end;
suppose (P1^P2).k in A;
hence thesis;
end;
suppose that A10: not k in dom P1 and A11: not (P1^P2).k in A;
consider j such that A12: j in dom P2 and A13: k = (len P1) + j
by A3, A10, FINSEQ_1:25;
reconsider m = j as Element of NAT by ORDINAL1:def 12;
A15: P2, m is_a_correct_step_wrt A, R by A2, A12;
A16: (P1^P2).k = P2.m by A12, A13, FINSEQ_1:def 7;
then consider Q being GRZ-formula-finset such that
A20: [Q, P2.m] in R and
A21: for q st q in Q ex i being Element of NAT
st i in dom P2 & i < m & P2.i = q by A11, A15;
for q st q in Q ex u being Element of NAT
st u in dom (P1^P2) & u < k & (P1^P2).u = q
proof
let q;
assume q in Q;
then consider i being Element of NAT such that
A25: i in dom P2 and
A26: i < m and
A27: P2.i = q by A21;
reconsider j = i as Nat;
reconsider u = len P1 + i as Element of NAT by ORDINAL1:def 12;
take u;
j in Seg len P2 by A25, FINSEQ_1:def 3;
then A30: 1 <= j & j <= len P2 by FINSEQ_1:1;
thus u in dom (P1^P2) by A25, FINSEQ_1:28;
thus u < k by A13, A26, XREAL_1:6;
thus (P1^P2).u = q by A27, A30, FINSEQ_1:65;
end;
hence thesis by A16, A20;
end;
end;
theorem Th43:
for A, R, S1, S2 st S1 is (A, R)-correct & S2 is (A, R)-correct holds
S1 \/ S2 is (A, R)-correct
proof
let A, R, S1, S2;
assume
A1: S1 is (A, R)-correct & S2 is (A, R)-correct;
consider P1, P2 such that
A3: P1 is (A, R)-correct and
A4: S1 = rng P1 and
A5: P2 is (A, R)-correct and
A6: S2 = rng P2 by A1;
reconsider S = rng(P1^P2) as GRZ-formula-finset;
S = S1 \/ S2 by A4, A6, FINSEQ_1:31;
hence thesis by A3, A5, Th42;
end;
Lm44:
for A, A1, R, R1, P, k st A c= A1 & R c= R1
& P, k is_a_correct_step_wrt A, R holds
P, k is_a_correct_step_wrt A1, R1;
theorem Th44:
for A, A1, R, R1, P st A c= A1 & R c= R1 & P is (A, R)-correct holds
P is (A1, R1)-correct by Lm44;
definition
let A, R, t;
pred A, R |- t means
ex P st t in rng P & P is (A, R)-correct;
end;
definition
let A, R, B;
pred A, R |- B means
for t st t in B holds A, R |- t;
end;
theorem Th45:
for A, R, t holds A, R |- t iff ex S st t in S & S is (A, R)-correct
proof
let A, R, t;
thus A, R |- t implies ex S st t in S & S is (A, R)-correct
proof
assume A, R |- t;
then consider P such that A1: t in rng P and A2: P is (A, R)-correct;
take S = rng P;
thus thesis by A1, A2;
end;
given S such that A10: t in S and A11: S is (A, R)-correct;
consider P such that A12: S = rng P and A13: P is (A, R)-correct by A11;
thus thesis by A10, A12, A13;
end;
theorem Th46:
for A, R, t st t in A holds A, R |- t
proof
let A, R, t;
assume t in A;
then reconsider a = t as Element of A;
set P = <*a*>;
take P;
rng P = {a} by FINSEQ_1:38;
hence thesis by TARSKI:def 1, Th40;
end;
theorem Th47:
for A, R, S st A, R |- S ex S1 st S c= S1 & S1 is (A, R)-correct
proof
let A, R, S;
assume A1: A, R |- S;
defpred X[ set ] means ex S1 st $1 c= S1 & S1 is (A, R)-correct;
A2: S is finite;
A10: X[ {} ]
proof
reconsider t = the Element of A as GRZ-formula;
consider S1 such that t in S1 and A11: S1 is (A, R)-correct by Th45, Th46;
take S1;
thus thesis by A11;
end;
A20: for x, B being set st x in S & B c= S & X[ B ] holds X[ B \/ {x} ]
proof
let x, B be set;
assume that
A21: x in S and
B c= S and
A23: X[ B ];
reconsider t = x as GRZ-formula by A21;
consider S1 such that
A24: t in S1 and
A25: S1 is (A, R)-correct by A1, A21, Th45;
consider S2 such that
A26: B c= S2 and
A27: S2 is (A, R)-correct by A23;
take S1 \/ S2;
{x} c= S1 by A24, TARSKI:def 1;
hence B \/ {x} c= S1 \/ S2 by A26, XBOOLE_1:13;
thus S1 \/ S2 is (A, R)-correct by A25, A27, Th43;
end;
thus X[ S ] from FINSET_1:sch 2(A2, A10, A20);
end;
theorem Th48:
for A, R, t, S st A, R |- S & [S, t] in R holds A, R |- t
proof
let A, R, t, S;
assume that
A1: A, R |- S and
A2: [S, t] in R;
consider S1 such that
A3: S c= S1 and
A4: S1 is (A, R)-correct by A1, Th47;
consider P1 such that
A5: S1 = rng P1 and
A6: P1 is (A, R)-correct by A4;
set P2 = P1^<*t*>;
rng P1 \/ rng <*t*> c= GRZ-formula-set by XBOOLE_1:8;
then rng P2 c= GRZ-formula-set by FINSEQ_1:31;
then reconsider P2 as GRZ-formula-sequence by FINSEQ_1:def 4;
take P2;
rng <*t*> = {t} by FINSEQ_1:38;
then t in rng <*t*> by TARSKI:def 1;
then t in rng P1 \/ rng <*t*> by XBOOLE_0:def 3;
hence t in rng P2 by FINSEQ_1:31;
let k;
reconsider j = k as Nat;
assume k in dom P2;
then per cases by FINSEQ_1:25;
suppose A11: j in dom P1;
then P1, k is_a_correct_step_wrt A, R by A6;
then P1^<*>GRZ-formula-set, k is_a_correct_step_wrt A, R
by FINSEQ_1:34;
hence thesis by A11, Lm41;
end;
suppose ex i st i in dom <*t*> & j = len P1+i;
then consider i such that
A20: i in dom <*t*> and
A21: j = len P1+i;
P2.j = <*t*>.i by A20, A21, FINSEQ_1:def 7;
then P2.j in rng <*t*> by A20, FUNCT_1:3;
then P2.j in {t} by FINSEQ_1:38;
then A22: P2.j = t by TARSKI:def 1;
i in {1} by A20, FINSEQ_1:2, FINSEQ_1:def 8;
then A23: j = len P1+1 by A21, TARSKI:def 1;
for q st q in S ex m st m in dom P2 & m < k & P2.m = q
proof
let q;
assume q in S;
then consider a such that
A25: a in dom P1 and
A26: P1.a = q by A3, A5, FUNCT_1:def 3;
reconsider m = a as Element of NAT by A25;
take m;
dom P1 c= dom P2 by FINSEQ_1:26;
hence m in dom P2 by A25;
m in Seg len P1 by A25, FINSEQ_1:def 3;
then m <= len P1 by FINSEQ_1:1;
hence m < k by A23, NAT_1:13;
thus thesis by A25, A26, FINSEQ_1:def 7;
end;
hence thesis by A2, A22;
end;
end;
theorem
for A, R, t st A, R |- t holds t in A or ex S st [S, t] in R & A, R |- S
proof
let A, R, t;
assume that
A1: A, R |- t and
A2: not t in A;
consider P such that
A3: t in rng P and
A4: P is (A, R)-correct by A1;
consider a such that
A5: a in dom P and
A6: P.a = t by A3, FUNCT_1:def 3;
reconsider n = a as Element of NAT by A5;
P, n is_a_correct_step_wrt A, R by A4, A5;
then consider Q being GRZ-formula-finset such that
A10: [Q, P.n] in R and
A11: for q st q in Q ex k
st k in dom P & k < n & P.k = q by A2, A6;
take Q;
thus [Q, t] in R by A6, A10;
let u;
assume u in Q;
then consider k such that
A15: k in dom P and
k < n and
A17: P.k = u by A11;
u in rng P by A15, A17, FUNCT_1:3;
hence A, R |- u by A4;
end;
theorem
for A, A1, R, R1, t st A c= A1 & R c= R1 & A, R |- t holds A1, R1 |- t
by Th44;
theorem Th60:
for A, t, u holds
A, GRZ-rules |- t '&' u iff A, GRZ-rules |- t & A, GRZ-rules |- u
proof
let A, t, u;
thus A, GRZ-rules |- t '&' u implies A, GRZ-rules |- t & A, GRZ-rules |- u
proof
assume A1: A, GRZ-rules |- t '&' u;
set S = {t '&' u};
for a st a in S holds a in GRZ-formula-set
proof
let a;
assume a in S;
then a = t '&' u by TARSKI:def 1;
hence thesis;
end;
then S c= GRZ-formula-set;
then reconsider S as GRZ-formula-finset;
A2: A, GRZ-rules |- S by A1, TARSKI:def 1;
[S, t] in GRZ-ConjElimL;
then [S, t] in GRZ-rules by Def35;
hence A, GRZ-rules |- t by A2, Th48;
[S, u] in GRZ-ConjElimR;
then [S, u] in GRZ-rules by Def35;
hence A, GRZ-rules |- u by A2, Th48;
end;
assume that A10: A, GRZ-rules |- t and A11: A, GRZ-rules |- u;
set S1 = {t, u};
for a st a in S1 holds a in GRZ-formula-set
proof
let a;
assume a in S1;
then a = t or a = u by TARSKI:def 2;
hence thesis;
end;
then S1 c= GRZ-formula-set;
then reconsider S1 as GRZ-formula-finset;
A12: A, GRZ-rules |- S1 by A10, A11, TARSKI:def 2;
[S1, t '&' u] in GRZ-ConjIntro;
then [S1, t '&' u] in GRZ-rules by Def35;
hence A, GRZ-rules |- t '&' u by A12, Th48;
end;
theorem Th61:
for A, t, u st A, GRZ-rules |- t & A, GRZ-rules |- t '=' u holds
A, GRZ-rules |- u
proof
let A, t, u;
assume A1: A, GRZ-rules |- t & A, GRZ-rules |- t '=' u;
set S = {t, t '=' u};
for a st a in S holds a in GRZ-formula-set
proof
let a;
assume a in S;
then a = t or a = t '=' u by TARSKI:def 2;
hence thesis;
end;
then S c= GRZ-formula-set;
then reconsider S as GRZ-formula-finset;
A3: A, GRZ-rules |- S by A1, TARSKI:def 2;
[S, u] in GRZ-MP;
then [S, u] in GRZ-rules by Def35;
hence A, GRZ-rules |- u by A3, Th48;
end;
theorem Th62:
for A, t, u st A, GRZ-rules |- t & A, GRZ-rules |- t => u holds
A, GRZ-rules |- u
proof
let A, t, u;
assume that
A1: A, GRZ-rules |- t and
A2: A, GRZ-rules |- t => u;
A, GRZ-rules |- t '&' u by A1, A2, Th61;
hence thesis by Th60;
end;
theorem
for A, t, u st A, GRZ-rules |- t '&' u holds A, GRZ-rules |- u '&' t
proof
let A, t, u;
assume A, GRZ-rules |- t '&' u;
then A, GRZ-rules |- t & A, GRZ-rules |- u by Th60;
hence thesis by Th60;
end;
definition
let t;
attr t is GRZ-axiomatic means
t in GRZ-axioms;
attr t is GRZ-provable means
GRZ-axioms, GRZ-rules |- t;
attr t is LD-axiomatic means
t in LD-axioms;
attr t is LD-provable means
LD-axioms, GRZ-rules |- t;
end;
registration
let t;
cluster 'not' (t '&' 'not' t) -> GRZ-axiomatic;
coherence by Def10;
cluster ('not' 'not' t) '=' t -> GRZ-axiomatic;
coherence by Def10;
cluster t '=' (t '&' t) -> GRZ-axiomatic;
coherence by Def10;
let u;
cluster (t '&' u) '=' (u '&' t) -> GRZ-axiomatic;
coherence by Def10;
cluster ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) -> GRZ-axiomatic;
coherence by Def10;
cluster (t '=' u) '=' (u '=' t) -> GRZ-axiomatic;
coherence by Def10;
cluster (t '=' u) '=' (('not' t) '=' ('not' u)) -> GRZ-axiomatic;
coherence by Def10;
let v;
cluster (t '&' (u '&' v)) '=' ((t '&' u) '&' v) -> GRZ-axiomatic;
coherence by Def10;
cluster (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) -> GRZ-axiomatic;
coherence by Def10;
cluster (t '=' u) => ((t '&' v) '=' (u '&' v)) -> LD-axiomatic;
coherence
proof
(t '=' u) => ((t '&' v) '=' (u '&' v)) in LD-specific-axioms by Def11;
hence thesis by XBOOLE_0:def 3;
end;
cluster (t '=' u) => ((t 'or' v) '=' (u 'or' v)) -> LD-axiomatic;
coherence
proof
(t '=' u) => ((t 'or' v) '=' (u 'or' v)) in LD-specific-axioms by Def11;
hence thesis by XBOOLE_0:def 3;
end;
cluster (t '=' u) => ((t '=' v) '=' (u '=' v)) -> LD-axiomatic;
coherence
proof
(t '=' u) => ((t '=' v) '=' (u '=' v)) in LD-specific-axioms by Def11;
hence thesis by XBOOLE_0:def 3;
end;
end;
registration
cluster GRZ-axiomatic -> LD-axiomatic for GRZ-formula;
coherence by XBOOLE_0:def 3;
cluster GRZ-axiomatic -> GRZ-provable for GRZ-formula;
coherence by Th46;
cluster LD-axiomatic -> LD-provable for GRZ-formula;
coherence by Th46;
cluster GRZ-provable -> LD-provable for GRZ-formula;
coherence
proof
let t;
assume t is GRZ-provable;
then
A1: GRZ-axioms, GRZ-rules |- t;
GRZ-axioms c= LD-axioms by XBOOLE_1:7;
then LD-axioms, GRZ-rules |- t by A1,Th44;
hence thesis;
end;
end;
registration
cluster GRZ-axiomatic GRZ-provable LD-axiomatic LD-provable for GRZ-formula;
existence
proof
take x.1 '=' (x.1 '&' x.1);
thus thesis;
end;
end;
theorem Th70:
for A, t, u st GRZ-axioms c= A & A, GRZ-rules |- t '=' u holds
A, GRZ-rules |- u '=' t
proof
let A, t, u;
assume that
A1: GRZ-axioms c= A and
A2: A, GRZ-rules |- t '=' u;
set v = (t '=' u) '=' (u '=' t);
v in GRZ-axioms by Def10;
then A, GRZ-rules |- v by A1, Th46;
hence thesis by A2, Th61;
end;
begin :: Provability
theorem
for t, u st t '=' u is GRZ-provable holds u '=' t is GRZ-provable by Th70;
theorem
for t, u st t '=' u is LD-provable holds u '=' t is LD-provable
by Th70, XBOOLE_1:7;
theorem Th74:
for t, u, v st t '=' u is LD-provable & u '=' v is LD-provable holds
t '=' v is LD-provable
proof
let t, u, v;
assume that
A1: t '=' u is LD-provable and
A2: u '=' v is LD-provable;
A3: u '=' t is LD-provable by A1, Th70, XBOOLE_1:7;
set w = (u '=' v) '=' (t '=' v);
(u '=' t) => w is LD-provable;
then w is LD-provable by A3, Th62;
hence thesis by A2, Th61;
end;
theorem Th75:
for t holds t '=' t is LD-provable
proof
let t;
set u = t '&' t;
A2: t '=' u is LD-provable;
then u '=' t is LD-provable by Th70, XBOOLE_1:7;
hence thesis by A2, Th74;
end;
definition
let t, u;
pred t LD-= u means
:Def76:
t '=' u is LD-provable;
reflexivity by Th75;
symmetry by Th70, XBOOLE_1:7;
end;
theorem Th76:
for t, u st t LD-= u holds 'not' t LD-= 'not' u
proof
let t, u;
set v = (t '=' u) '=' (('not' t) '=' ('not' u));
assume t LD-= u;
then A1: t '=' u is LD-provable;
v is LD-provable;
then ('not' t) '=' ('not' u) is LD-provable by A1, Th61;
hence thesis;
end;
scheme
BinReplace { X() -> non empty set,
F(Element of X(), Element of X()) -> Element of X(),
R[ Element of X(), Element of X() ] }:
for a, b, c, d being Element of X() st R[a, b] & R[c, d] holds
R[F(a, c), F(b, d)]
provided
A2: for a, b, c being Element of X() st R[a, b] & R[b, c] holds R[a, c] and
A3: for a, b being Element of X() holds R[F(a,b), F(b,a)] and
A4: for a, b, c being Element of X() st R[a, b] holds R[F(a,c), F(b,c)]
proof
let a, b, c, d be Element of X();
assume that
A10: R[a, b] and
A11: R[c, d];
A12: R[F(a,c), F(b,c)] by A4, A10;
R[F(b,c), F(c,b)] by A3;
then A13: R[F(a,c), F(c,b)] by A2, A12;
R[F(c,b),F(d,b)] by A4, A11;
then A14: R[F(a,c),F(d,b)] by A2, A13;
R[F(d,b),F(b,d)] by A3;
hence thesis by A2, A14;
end;
Lm77a:
for t, u, v st t '=' u is LD-provable holds
(t '&' v) '=' (u '&' v) is LD-provable
proof
let t, u, v;
assume A1: t '=' u is LD-provable;
(t '=' u) => ((t '&' v) '=' (u '&' v)) is LD-provable;
hence thesis by A1, Th62;
end;
theorem Th77:
for t, u, v, w st t LD-= u & v LD-= w holds t '&' v LD-= u '&' w
proof
deffunc F( GRZ-formula, GRZ-formula ) = $1 '&' $2;
defpred P[ GRZ-formula, GRZ-formula ] means $1 '=' $2 is LD-provable;
A2: for t, u, v st P[t, u] & P[u, v] holds P[t, v] by Th74;
A3: for t, u holds P[F(t,u), F(u,t)];
A4: for t, u, v st P[t, u] holds P[F(t,v), F(u,v)] by Lm77a;
for t, u, v, w st P[t, u] & P[v, w] holds P[F(t, v), F(u, w)]
from BinReplace(A2, A3, A4);
hence thesis;
end;
Lm78a:
for t, u, v st t '=' u is LD-provable holds
(t '=' v) '=' (u '=' v) is LD-provable
proof
let t, u, v;
assume A1: t '=' u is LD-provable;
(t '=' u) => ((t '=' v) '=' (u '=' v)) is LD-provable;
hence thesis by A1, Th62;
end;
theorem Th78:
for t, u, v, w st t LD-= u & v LD-= w holds t '=' v LD-= u '=' w
proof
deffunc F( GRZ-formula, GRZ-formula ) = $1 '=' $2;
defpred P[ GRZ-formula, GRZ-formula ] means $1 '=' $2 is LD-provable;
A2: for t, u, v st P[t, u] & P[u, v] holds P[t, v] by Th74;
A3: for t, u holds P[F(t,u), F(u,t)];
A4: for t, u, v st P[t, u] holds P[F(t,v), F(u,v)] by Lm78a;
for t, u, v, w st P[t, u] & P[v, w] holds P[F(t, v), F(u, w)]
from BinReplace(A2, A3, A4);
hence thesis;
end;
definition
func LD-EqR -> Equivalence_Relation of GRZ-formula-set means
:Def80:
for t, u holds [t,u] in it iff t LD-= u;
existence
proof
set W = GRZ-formula-set;
defpred X[object, object] means ex t, u st t = $1 & u = $2 & t LD-= u;
A1: for a st a in W holds X[a, a];
A10: for a, b st X[a, b] holds X[b, a];
A20: for a, b, c st X[a, b] & X[b, c] holds X[a, c]
proof
let a, b, c;
assume that A21: X[a, b] and A22: X[b, c];
consider t, u such that A23: t = a & u = b & t LD-= u by A21;
consider v, w such that A26: v = b & w = c & v LD-= w by A22;
take t, w;
thus thesis by A23, A26, Th74;
end;
consider E being Equivalence_Relation of W such that
A30: for a, b holds [a,b] in E iff a in W & b in W & X[a, b]
from EQREL_1:sch 1(A1, A10, A20);
take E;
let t, u;
thus [t, u] in E implies t LD-= u
proof
assume [t, u] in E;
then consider v, w such that A31: v = t & w = u & v LD-= w by A30;
thus thesis by A31;
end;
thus thesis by A30;
end;
uniqueness
proof
let E1, E2 be Equivalence_Relation of GRZ-formula-set;
assume that
A1: for t, u holds [t,u] in E1 iff t LD-= u and
A2: for t, u holds [t,u] in E2 iff t LD-= u;
for t, u holds [t, u] in E1 iff [t, u] in E2 by A1, A2;
hence thesis by RELSET_1:def 2;
end;
end;
registration
cluster non empty for Subset-Family of GRZ-formula-set;
existence
proof
reconsider t = bool GRZ-formula-set as Subset-Family of GRZ-formula-set;
take t;
thus thesis by ZFMISC_1:def 1;
end;
end;
definition
func LD-EqClasses -> non empty Subset-Family of GRZ-formula-set equals
Class LD-EqR;
coherence;
end;
definition
mode LD-EqClass is Element of LD-EqClasses;
end;
definition
let t;
func LD-EqClassOf t -> LD-EqClass equals
Class(LD-EqR, t);
coherence by EQREL_1:def 3;
end;
theorem Th80:
for t, u holds t LD-= u iff LD-EqClassOf t = LD-EqClassOf u
proof
let t, u;
thus t LD-= u implies LD-EqClassOf t = LD-EqClassOf u
proof
assume t LD-= u;
then [t, u] in LD-EqR by Def80;
then u in LD-EqClassOf t by EQREL_1:18;
hence thesis by EQREL_1:23;
end;
assume LD-EqClassOf t = LD-EqClassOf u;
then u in LD-EqClassOf t by EQREL_1:23;
then [t, u] in LD-EqR by EQREL_1:18;
hence thesis by Def80;
end;
scheme
UnOpCongr { X() -> non empty set, F(Element of X()) -> Element of X(),
E() -> Equivalence_Relation of X()}:
ex f being UnOp of Class E() st for x being Element of X() holds
f.(Class(E(), x)) = Class(E(), F(x))
provided
A1: for x, y being Element of X() st [x,y] in E() holds [F(x),F(y)] in E()
proof
defpred P[ object, object ] means ex y being Element of X() st
$1 = Class(E(), y) & $2 = Class(E(), F(y));
A2: for a st a in Class E() ex b st b in Class E() & P[a, b]
proof
let a;
assume a in Class E();
then consider c such that A5: c in X() and A6: a = Class(E(), c)
by EQREL_1:def 3;
reconsider y = c as Element of X() by A5;
take b = Class(E(), F(y));
thus b in Class E() by EQREL_1:def 3;
thus thesis by A6;
end;
consider f being Function of Class E(), Class E() such that
A10: for a st a in Class E() holds P[a, f.a]
from FUNCT_2:sch 1(A2);
take f;
let x be Element of X();
set u = Class(E(), x);
u in Class E() by EQREL_1:def 3;
then P[u, f.u] by A10;
then consider y being Element of X() such that
A11: Class(E(), x) = Class(E(), y) and
A12: f.(Class(E(), y)) = Class(E(), F(y));
y in Class(E(), x) by A11, EQREL_1:23;
then [x, y] in E() by EQREL_1:18;
then [F(x), F(y)] in E() by A1;
then F(y) in Class(E(), F(x)) by EQREL_1:18;
hence thesis by A11, A12, EQREL_1:23;
end;
scheme
BinOpCongr { X() -> non empty set,
F(Element of X(), Element of X()) -> Element of X(),
E() -> Equivalence_Relation of X()}:
ex f being BinOp of Class E() st for x, y being Element of X() holds
f.(Class(E(), x), Class(E(), y)) = Class(E(), F(x, y))
provided
A1: for x1, x2, y1, y2 being Element of X()
st [x1,x2] in E() & [y1,y2] in E() holds [F(x1, y1),F(x2, y2)] in E()
proof
defpred P[ object, object, object ] means ex x, y being Element of X() st
$1 = Class(E(), x) & $2 = Class(E(), y) & $3 = Class(E(), F(x,y));
A2: for a,b st a in Class E() & b in Class E()
ex c st c in Class E() & P[a, b, c]
proof
let a, b;
assume that A3: a in Class E() and A4: b in Class E();
consider a1 being object such that A5: a1 in X() and A6: a = Class(E(), a1)
by A3, EQREL_1:def 3;
consider b1 being object such that A7: b1 in X() and A8: b = Class(E(), b1)
by A4, EQREL_1:def 3;
reconsider a1, b1 as Element of X() by A5, A7;
take c = Class(E(), F(a1, b1));
thus c in Class E() by EQREL_1:def 3;
thus thesis by A6, A8;
end;
consider f being Function of [: Class E(), Class E() :], Class E() such that
A10: for a, b st a in Class E() & b in Class E() holds P[a, b, f.(a, b)]
from BINOP_1:sch 1(A2);
take f;
let x, y be Element of X();
set u = Class(E(), x);
set v = Class(E(), y);
u in Class E() & v in Class E() by EQREL_1:def 3;
then P[u, v, f.(u,v)] by A10;
then consider x1, y1 being Element of X() such that
A11: Class(E(), x) = Class(E(), x1) and
A12: Class(E(), y) = Class(E(), y1) and
A13: f.(Class(E(), x1), Class(E(), y1)) = Class(E(), F(x1, y1));
x1 in Class(E(), x) & y1 in Class(E(), y) by A11, A12, EQREL_1:23;
then [x, x1] in E() & [y, y1] in E() by EQREL_1:18;
then [F(x,y), F(x1,y1)] in E() by A1;
then F(x1,y1) in Class(E(), F(x,y)) by EQREL_1:18;
hence thesis by A11, A12, A13, EQREL_1:23;
end;
reserve x, y, z for LD-EqClass;
theorem Th88:
for x ex t st x = LD-EqClassOf t
proof
let x;
x in Class LD-EqR;
then consider a such that
A1: a in GRZ-formula-set and
A2: x = Class(LD-EqR, a) by EQREL_1:def 3;
reconsider t = a as GRZ-formula by A1;
take t;
thus thesis by A2;
end;
definition
let x;
attr x is LD-provable means
ex t st x = LD-EqClassOf t & t is LD-provable;
func 'not' x -> LD-EqClass means
:Def91:
ex t st x = LD-EqClassOf t & it = LD-EqClassOf 'not' t;
existence
proof
consider t such that A2: x = LD-EqClassOf t by Th88;
take LD-EqClassOf 'not' t;
thus thesis by A2;
end;
uniqueness
proof
let y1, y2 be LD-EqClass;
given t1 being GRZ-formula such that
A1: x = LD-EqClassOf t1 and
A2: y1 = LD-EqClassOf 'not' t1;
given t2 being GRZ-formula such that
A3: x = LD-EqClassOf t2 and
A4: y2 = LD-EqClassOf 'not' t2;
t1 LD-= t2 by A1, A3, Th80;
hence y1 = y2 by A2, A4, Th76, Th80;
end;
involutiveness
proof
let y, x be LD-EqClass;
given t being GRZ-formula such that
A1: x = LD-EqClassOf t and
A2: y = LD-EqClassOf 'not' t;
set u = 'not' t;
('not' u) '=' t is LD-provable;
then x = LD-EqClassOf 'not' u by A1, Def76, Th80;
hence thesis by A2;
end;
let y;
func x '&' y -> LD-EqClass means
:Def92:
ex t, u st x = LD-EqClassOf t & y = LD-EqClassOf u
& it = LD-EqClassOf t '&' u;
existence
proof
consider t such that A1: x = LD-EqClassOf t by Th88;
consider u such that A2: y = LD-EqClassOf u by Th88;
take LD-EqClassOf t '&' u;
thus thesis by A1, A2;
end;
uniqueness
proof
let z1, z2 be LD-EqClass;
given t1, u1 being GRZ-formula such that
A1: x = LD-EqClassOf t1 and
A2: y = LD-EqClassOf u1 and
A3: z1 = LD-EqClassOf t1 '&' u1;
given t2, u2 being GRZ-formula such that
A4: x = LD-EqClassOf t2 and
A5: y = LD-EqClassOf u2 and
A6: z2 = LD-EqClassOf t2 '&' u2;
A7: t1 LD-= t2 by A1, A4, Th80;
u1 LD-= u2 by A2, A5, Th80;
hence z1 = z2 by A3, A6, A7, Th77, Th80;
end;
commutativity
proof
let z;
let x, y;
given t, u such that
A1: x = LD-EqClassOf t & y = LD-EqClassOf u & z = LD-EqClassOf t '&' u;
take u, t;
u '&' t LD-= t '&' u;
hence thesis by A1, Th80;
end;
idempotence
proof
let x;
consider t such that A1: x = LD-EqClassOf t by Th88;
take t, t;
t '=' (t '&' t) is LD-provable;
hence thesis by A1, Th80, Def76;
end;
func x '=' y -> LD-EqClass means
:Def93:
ex t, u st x = LD-EqClassOf t & y = LD-EqClassOf u
& it = LD-EqClassOf t '=' u;
existence
proof
consider t such that A1: x = LD-EqClassOf t by Th88;
consider u such that A2: y = LD-EqClassOf u by Th88;
take LD-EqClassOf t '=' u;
thus thesis by A1, A2;
end;
uniqueness
proof
let z1, z2 be LD-EqClass;
given t1, u1 being GRZ-formula such that
A1: x = LD-EqClassOf t1 and
A2: y = LD-EqClassOf u1 and
A3: z1 = LD-EqClassOf t1 '=' u1;
given t2, u2 being GRZ-formula such that
A4: x = LD-EqClassOf t2 and
A5: y = LD-EqClassOf u2 and
A6: z2 = LD-EqClassOf t2 '=' u2;
A7: t1 LD-= t2 by A1, A4, Th80;
u1 LD-= u2 by A2, A5, Th80;
hence z1 = z2 by A3, A6, A7, Th78, Th80;
end;
commutativity
proof
let z;
let x, y;
given t, u such that
A1: x = LD-EqClassOf t & y = LD-EqClassOf u & z = LD-EqClassOf t '=' u;
take u, t;
u '=' t LD-= t '=' u;
hence thesis by A1, Th80;
end;
end;
definition
let x, y;
func x 'or' y -> LD-EqClass equals
'not' (('not' x) '&' ('not' y));
coherence;
commutativity;
idempotence;
func x => y -> LD-EqClass equals
x '=' (x '&' y);
coherence;
end;
registration
let t be LD-provable GRZ-formula;
cluster LD-EqClassOf t -> LD-provable;
coherence;
end;
theorem Th90:
for t st LD-EqClassOf t is LD-provable holds t is LD-provable
proof
let t;
set x = LD-EqClassOf t;
assume x is LD-provable;
then consider u such that A1: LD-EqClassOf u = x and A2: u is LD-provable;
u LD-= t by A1, Th80;
then u '=' t is LD-provable;
hence thesis by A2, Th61;
end;
theorem Th91:
for x, y holds x '&' y is LD-provable iff x is LD-provable & y is LD-provable
proof
let x, y;
consider t, u such that
A2: x = LD-EqClassOf t & y = LD-EqClassOf u and
A3: x '&' y = LD-EqClassOf t '&' u by Def92;
thus x '&' y is LD-provable implies x is LD-provable & y is LD-provable
proof
assume x '&' y is LD-provable;
then t '&' u is LD-provable by A3, Th90;
then t is LD-provable & u is LD-provable by Th60;
hence thesis by A2;
end;
assume x is LD-provable & y is LD-provable;
then t is LD-provable & u is LD-provable by A2, Th90;
then t '&' u is LD-provable by Th60;
hence x '&' y is LD-provable by A3;
end;
theorem Th92:
for x, y holds x '=' y is LD-provable iff x = y
proof
let x, y;
consider t, u such that
A2: x = LD-EqClassOf t & y = LD-EqClassOf u and
A3: x '=' y = LD-EqClassOf (t '=' u) by Def93;
thus x '=' y is LD-provable implies x = y
proof
assume x '=' y is LD-provable;
then t '=' u is LD-provable by A3, Th90;
hence thesis by A2, Th80, Def76;
end;
assume x = y;
then t '=' u is LD-provable by A2, Th80, Def76;
hence thesis by A3;
end;
theorem
for t holds LD-EqClassOf 'not' t = 'not' LD-EqClassOf t by Def91;
theorem
for t, u holds LD-EqClassOf (t '&' u) = (LD-EqClassOf t) '&' (LD-EqClassOf u)
by Def92;
theorem
for t, u holds LD-EqClassOf (t '=' u) = (LD-EqClassOf t) '=' (LD-EqClassOf u)
by Def93;
theorem Th96:
for t, u holds LD-EqClassOf (t 'or' u)
= (LD-EqClassOf t) 'or' (LD-EqClassOf u)
proof
let t, u;
thus LD-EqClassOf (t 'or' u)
= 'not' LD-EqClassOf (('not' t) '&' ('not' u)) by Def91
.= 'not' ((LD-EqClassOf 'not' t) '&' (LD-EqClassOf 'not' u)) by Def92
.= 'not' (('not' LD-EqClassOf t) '&' (LD-EqClassOf 'not' u)) by Def91
.= (LD-EqClassOf t) 'or' (LD-EqClassOf u) by Def91;
end;
theorem Th97:
for t, u holds LD-EqClassOf (t => u) = (LD-EqClassOf t) => (LD-EqClassOf u)
proof
let t, u;
thus LD-EqClassOf (t => u)
= (LD-EqClassOf t) '=' (LD-EqClassOf (t '&' u)) by Def93
.= (LD-EqClassOf t) => (LD-EqClassOf u) by Def92;
end;
theorem Th98:
for x, y, z holds (x '&' y) '&' z = x '&' (y '&' z)
proof
let x, y, z;
consider t, u such that
A1: x = LD-EqClassOf t and
A2: y = LD-EqClassOf u and
A3: x '&' y = LD-EqClassOf (t '&' u) by Def92;
consider v such that
A5: z = LD-EqClassOf v by Th88;
A10: (t '&' (u '&' v)) '=' ((t '&' u) '&' v) is LD-provable;
thus (x '&' y) '&' z = LD-EqClassOf ((t '&' u) '&' v) by A3, A5, Def92
.= LD-EqClassOf (t '&' (u '&' v)) by A10, Th80, Def76
.= (LD-EqClassOf t) '&' (LD-EqClassOf (u '&' v)) by Def92
.= x '&' (y '&' z) by A1, A2, A5, Def92;
end;
theorem
for x, y holds x => y is LD-provable iff x = x '&' y by Th92;
theorem Th101:
for x, y, z st x => y is LD-provable & y => z is LD-provable holds
x => z is LD-provable
proof
let x, y, z;
assume that
A1: x => y is LD-provable and
A2: y => z is LD-provable;
x = x '&' y by A1, Th92
.= x '&' (y '&' z) by A2, Th92
.= (x '&' y) '&' z by Th98
.= x '&' z by A1, Th92;
hence thesis by Th92;
end;
theorem
for t, u, v st t => u is LD-provable & u => v is LD-provable holds
t => v is LD-provable
proof
let t, u, v;
assume A1: t => u is LD-provable & u => v is LD-provable;
set x = LD-EqClassOf t;
set y = LD-EqClassOf u;
set z = LD-EqClassOf v;
A2: LD-EqClassOf (t => u) = x => y & LD-EqClassOf (u => v) = y => z by Th97;
LD-EqClassOf (t => v) = x => z by Th97;
hence t => v is LD-provable by A1, A2, Th90, Th101;
end;
theorem
for x, y, z holds x 'or' (y 'or' z) = (x 'or' y) 'or' z by Th98;
theorem Th104:
for x, y, z holds x '&' (y 'or' z) = ((x '&' y) 'or' (x '&' z))
proof
let x, y, z;
consider t such that A1: x = LD-EqClassOf t by Th88;
consider u such that A2: y = LD-EqClassOf u by Th88;
consider v such that A3: z = LD-EqClassOf v by Th88;
(t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) is LD-provable;
then A5: LD-EqClassOf (t '&' (u 'or' v))
= LD-EqClassOf ((t '&' u) 'or' (t '&' v)) by Th80, Def76;
thus x '&' (y 'or' z)
= (LD-EqClassOf t) '&' (LD-EqClassOf (u 'or' v)) by A1, A2, A3, Th96
.= LD-EqClassOf((t '&' u) 'or' (t '&' v)) by A5, Def92
.= (LD-EqClassOf (t '&' u)) 'or' (LD-EqClassOf (t '&' v)) by Th96
.= (LD-EqClassOf (t '&' u))
'or' ((LD-EqClassOf t) '&' (LD-EqClassOf v)) by Def92
.= ((x '&' y) 'or' (x '&' z)) by A1, A2, A3, Def92;
end;
theorem Th105:
for x, y, z holds x 'or' (y '&' z) = ((x 'or' y) '&' (x 'or' z))
proof
let x, y, z;
thus x 'or' (y '&' z) = 'not' (('not' x) '&' (('not' y) 'or' ('not' z)))
.= 'not' ((('not' x) '&' ('not' y)) 'or' (('not' x) '&' ('not' z)))
by Th104
.= ((x 'or' y) '&' (x 'or' z));
end;
theorem
for x, y holds (x => y is LD-provable & y => x is LD-provable) iff x = y
proof
let x, y;
thus (x => y is LD-provable & y => x is LD-provable) implies x = y
proof
assume that A1: x => y is LD-provable and A2: y => x is LD-provable;
thus x = x '&' y by A1, Th92 .= y by A2, Th92;
end;
assume x = y;
hence x => y is LD-provable & y => x is LD-provable by Th92;
end;
theorem
for x, y st x is LD-provable holds x 'or' y is LD-provable
proof
let x, y;
assume A1: x is LD-provable;
consider u such that A2: y = LD-EqClassOf u by Th88;
LD-EqClassOf ('not' (u '&' 'not' u))
= 'not' LD-EqClassOf (u '&' 'not' u) by Def91
.= 'not' ((LD-EqClassOf u) '&' (LD-EqClassOf 'not' u)) by Def92
.= 'not' (y '&' 'not' y) by A2, Def91;
then A5: x '&' ('not' y 'or' y) is LD-provable by A1, Th91;
x '&' ('not' y 'or' y) = (x '&' 'not' y) 'or' (x '&' y) by Th104
.= ((x '&' 'not' y) 'or' x) '&' ((x '&' 'not' y) 'or' y) by Th105;
then A6: (x '&' 'not' y) 'or' y is LD-provable by A5, Th91;
(x '&' 'not' y) 'or' y = (y 'or' x) '&' (y 'or' 'not' y) by Th105;
hence thesis by A6, Th91;
end;