grzlog_1.miz
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;
definition
::
GRZLOG_1:def1
func
VAR ->
FinSequence-membered
set equals the set of all
<*
0 , k*> where k be
Element of
NAT ;
coherence
proof
set X = the set of all
<*
0 , k*> where k be
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 18;
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 be
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,
FINSEQ_1: 44;
end;
definition
::
GRZLOG_1:def2
func
'not' ->
FinSequence equals
<*1*>;
coherence ;
::
GRZLOG_1:def3
func
'&' ->
FinSequence equals
<*2*>;
coherence ;
::
GRZLOG_1:def4
func
'=' ->
FinSequence equals
<*3*>;
coherence ;
end
definition
::
GRZLOG_1:def5
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 be
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
:: original:
GRZ-ops
redefine
func
GRZ-ops ->
Polish-language ;
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
::
GRZLOG_1:def6
func
GRZ-symbols -> non
empty
FinSequence-membered
set equals (
VAR
\/
GRZ-ops );
coherence
proof
set Y = (
VAR
\/
GRZ-ops );
for a st a
in Y holds a is
FinSequence
proof
let a;
assume
A1: a
in Y;
A2: a
in
VAR implies thesis;
a
in
GRZ-ops implies thesis;
hence thesis by
A1,
A2,
XBOOLE_0:def 3;
end;
hence thesis by
FINSEQ_1:def 18;
end;
end
definition
:: original:
'not'
redefine
func
'not' ->
Element of
GRZ-symbols ;
coherence
proof
'not'
in
GRZ-ops by
ENUMSET1:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
:: original:
'&'
redefine
func
'&' ->
Element of
GRZ-symbols ;
coherence
proof
'&'
in
GRZ-ops by
ENUMSET1:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
:: original:
'='
redefine
func
'=' ->
Element of
GRZ-symbols ;
coherence
proof
'='
in
GRZ-ops by
ENUMSET1:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
end
Lm3: for p be
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 ::
GRZLOG_1:1
Th1:
'not'
<>
'&' &
'not'
<>
'=' &
'&'
<>
'='
proof
A1: (
'not'
. 1)
= 1 by
FINSEQ_1:def 8;
(
'&'
. 1)
= 2 by
FINSEQ_1:def 8;
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
::
GRZLOG_1:def7
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 holds 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 be
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
::
GRZLOG_1:def8
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 holds 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 be
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 ::
GRZLOG_1:2
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 ::
GRZLOG_1:3
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
::
GRZLOG_1:def9
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;
::
GRZLOG_1:def10
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;
::
GRZLOG_1:def11
func
'not' t ->
GRZ-formula equals ((
Polish-unOp (
GRZ-symbols ,
GRZ-arity ,
'not' ))
. t);
coherence ;
let u;
::
GRZLOG_1:def12
func t
'&' u ->
GRZ-formula equals ((
Polish-binOp (
GRZ-symbols ,
GRZ-arity ,
'&' ))
. (t,u));
coherence ;
::
GRZLOG_1:def13
func t
'=' u ->
GRZ-formula equals ((
Polish-binOp (
GRZ-symbols ,
GRZ-arity ,
'=' ))
. (t,u));
coherence ;
end
definition
let t, u;
::
GRZLOG_1:def14
func t
'or' u ->
GRZ-formula equals (
'not' ((
'not' t)
'&' (
'not' u)));
coherence ;
::
GRZLOG_1:def15
func t
=> u ->
GRZ-formula equals (t
'=' (t
'&' u));
coherence ;
end
definition
let t, u;
::
GRZLOG_1:def16
func t
<=> u ->
GRZ-formula equals ((t
=> u)
'&' (u
=> t));
coherence ;
end
definition
let t;
::
GRZLOG_1:def17
attr t is
atomic means t
in (
Polish-atoms (
GRZ-symbols ,
GRZ-arity ));
::
GRZLOG_1:def18
attr t is
negative means (
Polish-WFF-head t)
=
'not' ;
::
GRZLOG_1:def19
attr t is
conjunctive means (
Polish-WFF-head t)
=
'&' ;
::
GRZLOG_1:def20
attr t is
being_equality means (
Polish-WFF-head t)
=
'=' ;
end
theorem ::
GRZLOG_1:4
for t holds t is
atomic iff t
in
VAR by
Th5;
theorem ::
GRZLOG_1:5
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 ::
GRZLOG_1:6
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 ::
GRZLOG_1:7
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 ::
GRZLOG_1:8
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
::
GRZLOG_1:def21
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 be
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;
::
GRZLOG_1:def22
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 be
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
::
GRZLOG_1:def23
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;
:: original:
\/
redefine
func R1
\/ R2 ->
GRZ-rule ;
coherence by
XBOOLE_1: 8;
end
definition
::
GRZLOG_1:def24
func
GRZ-MP ->
GRZ-rule equals the set of all
[
{t, (t
'=' u)}, u] where t be
GRZ-formula, u be
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 be
GRZ-formula, u be
GRZ-formula;
for a st a
in Z holds a
in Y
proof
let a;
assume a
in Z;
then
consider t,u be
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;
::
GRZLOG_1:def25
func
GRZ-ConjIntro ->
GRZ-rule equals the set of all
[
{t, u}, (t
'&' u)] where t be
GRZ-formula, u be
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 be
GRZ-formula, u be
GRZ-formula;
Z
c= Y
proof
let a;
assume a
in Z;
then
consider t,u be
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;
::
GRZLOG_1:def26
func
GRZ-ConjElimL ->
GRZ-rule equals the set of all
[
{(t
'&' u)}, t] where t be
GRZ-formula, u be
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 be
GRZ-formula, u be
GRZ-formula;
Z
c= Y
proof
let a;
assume a
in Z;
then
consider t,u be
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;
::
GRZLOG_1:def27
func
GRZ-ConjElimR ->
GRZ-rule equals the set of all
[
{(t
'&' u)}, u] where t be
GRZ-formula, u be
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 be
GRZ-formula, u be
GRZ-formula;
Z
c= Y
proof
let a;
assume a
in Z;
then
consider t,u be
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
::
GRZLOG_1:def28
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 be
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;
:: original:
\/
redefine
func S1
\/ S2 ->
GRZ-formula-finset ;
coherence
proof
set S = (S1
\/ S2);
thus S is
finite
Subset of
GRZ-formula-set ;
end;
end
definition
let A, R, P, n;
::
GRZLOG_1:def29
pred P,n
is_a_correct_step_wrt A,R means ((P
. n)
in A or ex Q be
GRZ-formula-finset st (
[Q, (P
. n)]
in R & for q st q
in Q holds ex k st k
in (
dom P) & k
< n & (P
. k)
= q));
end
definition
let A, R, P;
::
GRZLOG_1:def30
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;
:: original:
<*
redefine
func
<*a*> ->
GRZ-formula-sequence ;
coherence
proof
reconsider b = a as
Element of
GRZ-formula-set ;
<*a*>
=
<*b*>;
hence
<*a*> is
FinSequence of
GRZ-formula-set ;
end;
end
theorem ::
GRZLOG_1:9
Th40: for A, R holds for a be
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
emptyA, 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;
::
GRZLOG_1:def31
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 be
GRZ-formula-finset st (
[Q, (P
. n)]
in R & for q st q
in Q holds ex m st m
in (
dom (P
^ P1)) & m
< n & ((P
^ P1)
. m)
= q);
then
consider Q be
GRZ-formula-finset such that
A10:
[Q, (P
. n)]
in R and
A11: for q st q
in Q holds ex m st m
in (
dom (P
^ P1)) & m
< n & ((P
^ P1)
. m)
= q;
A13: for q st q
in Q holds 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 ::
GRZLOG_1:10
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 ::
GRZLOG_1:11
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 be
GRZ-formula-finset such that
A20:
[Q, (P2
. m)]
in R and
A21: for q st q
in Q holds ex i be
Element of
NAT st i
in (
dom P2) & i
< m & (P2
. i)
= q by
A11,
A15;
for q st q
in Q holds ex u be
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 be
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 ::
GRZLOG_1:12
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 ::
GRZLOG_1:13
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;
::
GRZLOG_1:def32
pred A,R
|- t means ex P st t
in (
rng P) & P is A, R
-correct;
end
definition
let A, R, B;
::
GRZLOG_1:def33
pred A,R
|- B means for t st t
in B holds (A,R)
|- t;
end
theorem ::
GRZLOG_1:14
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 ::
GRZLOG_1:15
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 ::
GRZLOG_1:16
Th47: for A, R, S st (A,R)
|- S holds 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 be
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 ::
GRZLOG_1:17
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);
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 holds 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 ::
GRZLOG_1:18
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 be
GRZ-formula-finset such that
A10:
[Q, (P
. n)]
in R and
A11: for q st q
in Q holds 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 ::
GRZLOG_1:19
for A, A1, R, R1, t st A
c= A1 & R
c= R1 & (A,R)
|- t holds (A1,R1)
|- t by
Th44;
theorem ::
GRZLOG_1:20
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 ::
GRZLOG_1:21
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 ::
GRZLOG_1:22
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 ::
GRZLOG_1:23
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;
::
GRZLOG_1:def34
attr t is
GRZ-axiomatic means t
in
GRZ-axioms ;
::
GRZLOG_1:def35
attr t is
GRZ-provable means (
GRZ-axioms ,
GRZ-rules )
|- t;
::
GRZLOG_1:def36
attr t is
LD-axiomatic means t
in
LD-axioms ;
::
GRZLOG_1:def37
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 ::
GRZLOG_1:24
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
theorem ::
GRZLOG_1:25
for t, u st (t
'=' u) is
GRZ-provable holds (u
'=' t) is
GRZ-provable by
Th70;
theorem ::
GRZLOG_1:26
for t, u st (t
'=' u) is
LD-provable holds (u
'=' t) is
LD-provable by
Th70,
XBOOLE_1: 7;
theorem ::
GRZLOG_1:27
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 ::
GRZLOG_1:28
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;
::
GRZLOG_1:def38
pred t
LD-= u means
:
Def76: (t
'=' u) is
LD-provable;
reflexivity by
Th75;
symmetry by
Th70,
XBOOLE_1: 7;
end
theorem ::
GRZLOG_1:29
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 ::
GRZLOG_1:sch1
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 be
Element of X() st R[a, b] & R[c, d] holds R[F(a,c), F(b,d)]
provided
A2: for a,b,c be
Element of X() st R[a, b] & R[b, c] holds R[a, c]
and
A3: for a,b be
Element of X() holds R[F(a,b), F(b,a)]
and
A4: for a,b,c be
Element of X() st R[a, b] holds R[F(a,c), F(b,c)];
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 ::
GRZLOG_1:30
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 ::
GRZLOG_1:31
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
::
GRZLOG_1:def39
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 be
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
::
GRZLOG_1:def40
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;
::
GRZLOG_1:def41
func
LD-EqClassOf t ->
LD-EqClass equals (
Class (
LD-EqR ,t));
coherence by
EQREL_1:def 3;
end
theorem ::
GRZLOG_1:32
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 ::
GRZLOG_1:sch2
UnOpCongr { X() -> non
empty
set , F(
Element of X()) ->
Element of X() , E() ->
Equivalence_Relation of X() } :
ex f be
UnOp of (
Class E()) st for x be
Element of X() holds (f
. (
Class (E(),x)))
= (
Class (E(),F(x)))
provided
A1: for x,y be
Element of X() st
[x, y]
in E() holds
[F(x), F(y)]
in E();
defpred
P[
object,
object] means ex y be
Element of X() st $1
= (
Class (E(),y)) & $2
= (
Class (E(),F(y)));
A2: for a st a
in (
Class E()) holds 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 be
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 be
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 ::
GRZLOG_1:sch3
BinOpCongr { X() -> non
empty
set , F(
Element of X(),
Element of X()) ->
Element of X() , E() ->
Equivalence_Relation of X() } :
ex f be
BinOp of (
Class E()) st for x,y be
Element of X() holds (f
. ((
Class (E(),x)),(
Class (E(),y))))
= (
Class (E(),F(x,y)))
provided
A1: for x1,x2,y1,y2 be
Element of X() st
[x1, x2]
in E() &
[y1, y2]
in E() holds
[F(x1,y1), F(x2,y2)]
in E();
defpred
P[
object,
object,
object] means ex x,y be
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()) holds 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 be
object such that
A5: a1
in X() and
A6: a
= (
Class (E(),a1)) by
A3,
EQREL_1:def 3;
consider b1 be
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 be
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 be
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 ::
GRZLOG_1:33
Th88: for x holds 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;
::
GRZLOG_1:def42
attr x is
LD-provable means ex t st x
= (
LD-EqClassOf t) & t is
LD-provable;
::
GRZLOG_1:def43
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 be
GRZ-formula such that
A1: x
= (
LD-EqClassOf t1) and
A2: y1
= (
LD-EqClassOf (
'not' t1));
given t2 be
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 be
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;
::
GRZLOG_1:def44
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 be
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 be
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;
::
GRZLOG_1:def45
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 be
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 be
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;
::
GRZLOG_1:def46
func x
'or' y ->
LD-EqClass equals (
'not' ((
'not' x)
'&' (
'not' y)));
coherence ;
commutativity ;
idempotence ;
::
GRZLOG_1:def47
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 ::
GRZLOG_1:34
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 ::
GRZLOG_1:35
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 ::
GRZLOG_1:36
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 ::
GRZLOG_1:37
for t holds (
LD-EqClassOf (
'not' t))
= (
'not' (
LD-EqClassOf t)) by
Def91;
theorem ::
GRZLOG_1:38
for t, u holds (
LD-EqClassOf (t
'&' u))
= ((
LD-EqClassOf t)
'&' (
LD-EqClassOf u)) by
Def92;
theorem ::
GRZLOG_1:39
for t, u holds (
LD-EqClassOf (t
'=' u))
= ((
LD-EqClassOf t)
'=' (
LD-EqClassOf u)) by
Def93;
theorem ::
GRZLOG_1:40
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 ::
GRZLOG_1:41
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 ::
GRZLOG_1:42
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 ::
GRZLOG_1:43
for x, y holds (x
=> y) is
LD-provable iff x
= (x
'&' y) by
Th92;
theorem ::
GRZLOG_1:44
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 ::
GRZLOG_1:45
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 ::
GRZLOG_1:46
for x, y, z holds (x
'or' (y
'or' z))
= ((x
'or' y)
'or' z) by
Th98;
theorem ::
GRZLOG_1:47
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 ::
GRZLOG_1:48
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 ::
GRZLOG_1:49
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 ::
GRZLOG_1:50
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;