:: by Taneli Huuskonen

::

:: Received April 30, 2015

:: Copyright (c) 2015-2017 Association of Mizar Users

definition

{ <*0,k*> where k is Element of NAT : verum } is FinSequence-membered set
end;

func VAR -> FinSequence-membered set equals :: GRZLOG_1:def 1

{ <*0,k*> where k is Element of NAT : verum } ;

coherence { <*0,k*> where k is Element of NAT : verum } ;

{ <*0,k*> where k is Element of NAT : verum } is FinSequence-membered set

proof end;

Lm1: for a being Variable holds a . 1 = 0

proof end;

definition
end;

Lm2: for p being Element of GRZ-ops holds

( dom p = Seg 1 & p . 1 <> 0 )

proof end;

definition

:: original: GRZ-ops

redefine func GRZ-ops -> Polish-language;

coherence

GRZ-ops is Polish-language

end;
redefine func GRZ-ops -> Polish-language;

coherence

GRZ-ops is Polish-language

proof end;

definition

:: original: 'not'

redefine func 'not' -> Element of GRZ-symbols ;

coherence

'not' is Element of GRZ-symbols

redefine func '&' -> Element of GRZ-symbols ;

coherence

'&' is Element of GRZ-symbols

redefine func '=' -> Element of GRZ-symbols ;

coherence

'=' is Element of GRZ-symbols

end;
redefine func 'not' -> Element of GRZ-symbols ;

coherence

'not' is Element of GRZ-symbols

proof end;

:: original: '&'redefine func '&' -> Element of GRZ-symbols ;

coherence

'&' is Element of GRZ-symbols

proof end;

:: original: '='redefine func '=' -> Element of GRZ-symbols ;

coherence

'=' is Element of GRZ-symbols

proof end;

Lm3: for p being Element of GRZ-symbols holds

( p . 1 = 0 iff p in VAR )

proof end;

Lm4: for a being object holds

( not a in VAR or not a in GRZ-ops )

proof end;

Th3: ( not GRZ-symbols is trivial & GRZ-symbols is antichain-like )

proof end;

definition

ex b_{1} being Function of GRZ-ops,NAT st

( b_{1} . 'not' = 1 & b_{1} . '&' = 2 & b_{1} . '=' = 2 )

for b_{1}, b_{2} being Function of GRZ-ops,NAT st b_{1} . 'not' = 1 & b_{1} . '&' = 2 & b_{1} . '=' = 2 & b_{2} . 'not' = 1 & b_{2} . '&' = 2 & b_{2} . '=' = 2 holds

b_{1} = b_{2}
end;

func GRZ-op-arity -> Function of GRZ-ops,NAT means :Def3: :: GRZLOG_1:def 7

( it . 'not' = 1 & it . '&' = 2 & it . '=' = 2 );

existence ( it . 'not' = 1 & it . '&' = 2 & it . '=' = 2 );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines GRZ-op-arity GRZLOG_1:def 7 :

for b_{1} being Function of GRZ-ops,NAT holds

( b_{1} = GRZ-op-arity iff ( b_{1} . 'not' = 1 & b_{1} . '&' = 2 & b_{1} . '=' = 2 ) );

for b

( b

definition

ex b_{1} being Polish-arity-function of GRZ-symbols st

for a being object st a in GRZ-symbols holds

( ( a in GRZ-ops implies b_{1} . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies b_{1} . a = 0 ) )

for b_{1}, b_{2} being Polish-arity-function of GRZ-symbols st ( for a being object st a in GRZ-symbols holds

( ( a in GRZ-ops implies b_{1} . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies b_{1} . a = 0 ) ) ) & ( for a being object st a in GRZ-symbols holds

( ( a in GRZ-ops implies b_{2} . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies b_{2} . a = 0 ) ) ) holds

b_{1} = b_{2}
end;

func GRZ-arity -> Polish-arity-function of GRZ-symbols means :Def4: :: GRZLOG_1:def 8

for a being object 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 for a being object 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 ) );

ex b

for a being object st a in GRZ-symbols holds

( ( a in GRZ-ops implies b

proof end;

uniqueness for b

( ( a in GRZ-ops implies b

( ( a in GRZ-ops implies b

b

proof end;

:: deftheorem Def4 defines GRZ-arity GRZLOG_1:def 8 :

for b_{1} being Polish-arity-function of GRZ-symbols holds

( b_{1} = GRZ-arity iff for a being object st a in GRZ-symbols holds

( ( a in GRZ-ops implies b_{1} . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies b_{1} . a = 0 ) ) );

for b

( b

( ( a in GRZ-ops implies b

Lm10: for a being object st a in GRZ-ops holds

GRZ-arity . a = GRZ-op-arity . a

proof end;

definition

Polish-WFF-set (GRZ-symbols,GRZ-arity) is Polish-language of GRZ-symbols ;

mode GRZ-formula is Polish-WFF of GRZ-symbols,GRZ-arity;

end;

func GRZ-formula-set -> Polish-language of GRZ-symbols equals :: GRZLOG_1:def 9

Polish-WFF-set (GRZ-symbols,GRZ-arity);

coherence Polish-WFF-set (GRZ-symbols,GRZ-arity);

Polish-WFF-set (GRZ-symbols,GRZ-arity) is Polish-language of GRZ-symbols ;

mode GRZ-formula is Polish-WFF of GRZ-symbols,GRZ-arity;

:: deftheorem defines GRZ-formula-set GRZLOG_1:def 9 :

GRZ-formula-set = Polish-WFF-set (GRZ-symbols,GRZ-arity);

GRZ-formula-set = Polish-WFF-set (GRZ-symbols,GRZ-arity);

registration

not for b_{1} being Subset of GRZ-formula-set holds b_{1} is empty
end;

cluster non empty functional FinSequence-membered antichain-like for Element of bool GRZ-formula-set;

existence not for b

proof end;

definition

let t be GRZ-formula;

(Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . t is GRZ-formula ;

let u be GRZ-formula;

(Polish-binOp (GRZ-symbols,GRZ-arity,'&')) . (t,u) is GRZ-formula ;

(Polish-binOp (GRZ-symbols,GRZ-arity,'=')) . (t,u) is GRZ-formula ;

end;
func 'not' t -> GRZ-formula equals :: GRZLOG_1:def 11

(Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . t;

coherence (Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . t;

(Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . t is GRZ-formula ;

let u be GRZ-formula;

func t '&' u -> GRZ-formula equals :: GRZLOG_1:def 12

(Polish-binOp (GRZ-symbols,GRZ-arity,'&')) . (t,u);

coherence (Polish-binOp (GRZ-symbols,GRZ-arity,'&')) . (t,u);

(Polish-binOp (GRZ-symbols,GRZ-arity,'&')) . (t,u) is GRZ-formula ;

func t '=' u -> GRZ-formula equals :: GRZLOG_1:def 13

(Polish-binOp (GRZ-symbols,GRZ-arity,'=')) . (t,u);

coherence (Polish-binOp (GRZ-symbols,GRZ-arity,'=')) . (t,u);

(Polish-binOp (GRZ-symbols,GRZ-arity,'=')) . (t,u) is GRZ-formula ;

:: deftheorem defines 'not' GRZLOG_1:def 11 :

for t being GRZ-formula holds 'not' t = (Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . t;

for t being GRZ-formula holds 'not' t = (Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . t;

:: deftheorem defines '&' GRZLOG_1:def 12 :

for t, u being GRZ-formula holds t '&' u = (Polish-binOp (GRZ-symbols,GRZ-arity,'&')) . (t,u);

for t, u being GRZ-formula holds t '&' u = (Polish-binOp (GRZ-symbols,GRZ-arity,'&')) . (t,u);

:: deftheorem defines '=' GRZLOG_1:def 13 :

for t, u being GRZ-formula holds t '=' u = (Polish-binOp (GRZ-symbols,GRZ-arity,'=')) . (t,u);

for t, u being GRZ-formula holds t '=' u = (Polish-binOp (GRZ-symbols,GRZ-arity,'=')) . (t,u);

definition

let t, u be GRZ-formula;

coherence

'not' (('not' t) '&' ('not' u)) is GRZ-formula ;

coherence

t '=' (t '&' u) is GRZ-formula ;

end;
coherence

'not' (('not' t) '&' ('not' u)) is GRZ-formula ;

coherence

t '=' (t '&' u) is GRZ-formula ;

:: deftheorem defines 'or' GRZLOG_1:def 14 :

for t, u being GRZ-formula holds t 'or' u = 'not' (('not' t) '&' ('not' u));

for t, u being GRZ-formula holds t 'or' u = 'not' (('not' t) '&' ('not' u));

:: deftheorem defines => GRZLOG_1:def 15 :

for t, u being GRZ-formula holds t => u = t '=' (t '&' u);

for t, u being GRZ-formula holds t => u = t '=' (t '&' u);

:: deftheorem defines <=> GRZLOG_1:def 16 :

for t, u being GRZ-formula holds t <=> u = (t => u) '&' (u => t);

for t, u being GRZ-formula holds t <=> u = (t => u) '&' (u => t);

:: deftheorem defines atomic GRZLOG_1:def 17 :

for t being GRZ-formula holds

( t is atomic iff t in Polish-atoms (GRZ-symbols,GRZ-arity) );

for t being GRZ-formula holds

( t is atomic iff t in Polish-atoms (GRZ-symbols,GRZ-arity) );

:: deftheorem defines negative GRZLOG_1:def 18 :

for t being GRZ-formula holds

( t is negative iff Polish-WFF-head t = 'not' );

for t being GRZ-formula holds

( t is negative iff Polish-WFF-head t = 'not' );

:: deftheorem defines conjunctive GRZLOG_1:def 19 :

for t being GRZ-formula holds

( t is conjunctive iff Polish-WFF-head t = '&' );

for t being GRZ-formula holds

( t is conjunctive iff Polish-WFF-head t = '&' );

:: deftheorem defines being_equality GRZLOG_1:def 20 :

for t being GRZ-formula holds

( t is being_equality iff Polish-WFF-head t = '=' );

for t being GRZ-formula holds

( t is being_equality iff Polish-WFF-head t = '=' );

theorem :: GRZLOG_1:8

for t being GRZ-formula holds

( t is atomic or t is negative or t is conjunctive or t is being_equality )

( t is atomic or t is negative or t is conjunctive or t is being_equality )

proof end;

registration

coherence

for b_{1} being GRZ-formula st b_{1} is atomic holds

not b_{1} is negative

for b_{1} being GRZ-formula st b_{1} is atomic holds

not b_{1} is conjunctive

for b_{1} being GRZ-formula st b_{1} is atomic holds

not b_{1} is being_equality

for b_{1} being GRZ-formula st b_{1} is negative holds

not b_{1} is conjunctive
by Th1;

coherence

for b_{1} being GRZ-formula st b_{1} is negative holds

not b_{1} is being_equality
by Th1;

coherence

for b_{1} being GRZ-formula st b_{1} is conjunctive holds

not b_{1} is being_equality
by Th1;

end;
for b

not b

proof end;

coherence for b

not b

proof end;

coherence for b

not b

proof end;

coherence for b

not b

coherence

for b

not b

coherence

for b

not b

definition

ex b_{1} being non empty Subset of GRZ-formula-set st

for a being object holds

( a in b_{1} iff ex t, u, v being GRZ-formula 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)) ) )

for b_{1}, b_{2} being non empty Subset of GRZ-formula-set st ( for a being object holds

( a in b_{1} iff ex t, u, v being GRZ-formula 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)) ) ) ) & ( for a being object holds

( a in b_{2} iff ex t, u, v being GRZ-formula 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)) ) ) ) holds

b_{1} = b_{2}

ex b_{1} being non empty Subset of GRZ-formula-set st

for a being object holds

( a in b_{1} iff ex t, u, v being GRZ-formula 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)) ) )

for b_{1}, b_{2} being non empty Subset of GRZ-formula-set st ( for a being object holds

( a in b_{1} iff ex t, u, v being GRZ-formula 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)) ) ) ) & ( for a being object holds

( a in b_{2} iff ex t, u, v being GRZ-formula 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)) ) ) ) holds

b_{1} = b_{2}
end;

func GRZ-axioms -> non empty Subset of GRZ-formula-set means :Def10: :: GRZLOG_1:def 21

for a being object holds

( a in it iff ex t, u, v being GRZ-formula 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 for a being object holds

( a in it iff ex t, u, v being GRZ-formula 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)) ) );

ex b

for a being object holds

( a in b

( 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)) ) )

proof end;

uniqueness for b

( a in b

( 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)) ) ) ) & ( for a being object holds

( a in b

( 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)) ) ) ) holds

b

proof end;

func LD-specific-axioms -> non empty Subset of GRZ-formula-set means :Def11: :: GRZLOG_1:def 22

for a being object holds

( a in it iff ex t, u, v being GRZ-formula 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 for a being object holds

( a in it iff ex t, u, v being GRZ-formula 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)) ) );

ex b

for a being object holds

( a in b

( 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)) ) )

proof end;

uniqueness for b

( a in b

( 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)) ) ) ) & ( for a being object holds

( a in b

( 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)) ) ) ) holds

b

proof end;

:: deftheorem Def10 defines GRZ-axioms GRZLOG_1:def 21 :

for b_{1} being non empty Subset of GRZ-formula-set holds

( b_{1} = GRZ-axioms iff for a being object holds

( a in b_{1} iff ex t, u, v being GRZ-formula 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)) ) ) );

for b

( b

( a in b

( 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)) ) ) );

:: deftheorem Def11 defines LD-specific-axioms GRZLOG_1:def 22 :

for b_{1} being non empty Subset of GRZ-formula-set holds

( b_{1} = LD-specific-axioms iff for a being object holds

( a in b_{1} iff ex t, u, v being GRZ-formula 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)) ) ) );

for b

( b

( a in b

( 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)) ) ) );

definition

GRZ-axioms \/ LD-specific-axioms is non empty Subset of GRZ-formula-set ;

end;

func LD-axioms -> non empty Subset of GRZ-formula-set equals :: GRZLOG_1:def 23

GRZ-axioms \/ LD-specific-axioms;

coherence GRZ-axioms \/ LD-specific-axioms;

GRZ-axioms \/ LD-specific-axioms is non empty Subset of GRZ-formula-set ;

definition

let R1, R2 be GRZ-rule;

:: original: \/

redefine func R1 \/ R2 -> GRZ-rule;

coherence

R1 \/ R2 is GRZ-rule by XBOOLE_1:8;

end;
:: original: \/

redefine func R1 \/ R2 -> GRZ-rule;

coherence

R1 \/ R2 is GRZ-rule by XBOOLE_1:8;

definition

{ [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } is GRZ-rule

{ [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } is GRZ-rule

{ [{(t '&' u)},t] where t, u is GRZ-formula : verum } is GRZ-rule

{ [{(t '&' u)},u] where t, u is GRZ-formula : verum } is GRZ-rule
end;

func GRZ-MP -> GRZ-rule equals :: GRZLOG_1:def 24

{ [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } ;

coherence { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } ;

{ [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } is GRZ-rule

proof end;

func GRZ-ConjIntro -> GRZ-rule equals :: GRZLOG_1:def 25

{ [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } ;

coherence { [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } ;

{ [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } is GRZ-rule

proof end;

func GRZ-ConjElimL -> GRZ-rule equals :: GRZLOG_1:def 26

{ [{(t '&' u)},t] where t, u is GRZ-formula : verum } ;

coherence { [{(t '&' u)},t] where t, u is GRZ-formula : verum } ;

{ [{(t '&' u)},t] where t, u is GRZ-formula : verum } is GRZ-rule

proof end;

func GRZ-ConjElimR -> GRZ-rule equals :: GRZLOG_1:def 27

{ [{(t '&' u)},u] where t, u is GRZ-formula : verum } ;

coherence { [{(t '&' u)},u] where t, u is GRZ-formula : verum } ;

{ [{(t '&' u)},u] where t, u is GRZ-formula : verum } is GRZ-rule

proof end;

:: deftheorem defines GRZ-MP GRZLOG_1:def 24 :

GRZ-MP = { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } ;

GRZ-MP = { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } ;

:: deftheorem defines GRZ-ConjIntro GRZLOG_1:def 25 :

GRZ-ConjIntro = { [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } ;

GRZ-ConjIntro = { [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } ;

:: deftheorem defines GRZ-ConjElimL GRZLOG_1:def 26 :

GRZ-ConjElimL = { [{(t '&' u)},t] where t, u is GRZ-formula : verum } ;

GRZ-ConjElimL = { [{(t '&' u)},t] where t, u is GRZ-formula : verum } ;

:: deftheorem defines GRZ-ConjElimR GRZLOG_1:def 27 :

GRZ-ConjElimR = { [{(t '&' u)},u] where t, u is GRZ-formula : verum } ;

GRZ-ConjElimR = { [{(t '&' u)},u] where t, u is GRZ-formula : verum } ;

definition

ex b_{1} being GRZ-rule st

for a being object holds

( a in b_{1} iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) )

for b_{1}, b_{2} being GRZ-rule st ( for a being object holds

( a in b_{1} iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) ) ) & ( for a being object holds

( a in b_{2} iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) ) ) holds

b_{1} = b_{2}
end;

func GRZ-rules -> GRZ-rule means :Def35: :: GRZLOG_1:def 28

for a being object 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 for a being object holds

( a in it iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) );

ex b

for a being object holds

( a in b

proof end;

uniqueness for b

( a in b

( a in b

b

proof end;

:: deftheorem Def35 defines GRZ-rules GRZLOG_1:def 28 :

for b_{1} being GRZ-rule holds

( b_{1} = GRZ-rules iff for a being object holds

( a in b_{1} iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) ) );

for b

( b

( a in b

definition

mode GRZ-formula-sequence is FinSequence of GRZ-formula-set ;

mode GRZ-formula-finset is finite Subset of GRZ-formula-set;

end;
mode GRZ-formula-finset is finite Subset of GRZ-formula-set;

definition

let S1, S2 be GRZ-formula-finset;

:: original: \/

redefine func S1 \/ S2 -> GRZ-formula-finset;

coherence

S1 \/ S2 is GRZ-formula-finset

end;
:: original: \/

redefine func S1 \/ S2 -> GRZ-formula-finset;

coherence

S1 \/ S2 is GRZ-formula-finset

proof end;

definition

let A be non empty Subset of GRZ-formula-set;

let R be GRZ-rule;

let P be GRZ-formula-sequence;

let n be Element of NAT ;

end;
let R be GRZ-rule;

let P be GRZ-formula-sequence;

let n be Element of NAT ;

pred P,n is_a_correct_step_wrt A,R means :: GRZLOG_1:def 29

( P . n in A or ex Q being GRZ-formula-finset st

( [Q,(P . n)] in R & ( for q being FinSequence st q in Q holds

ex k being Element of NAT st

( k in dom P & k < n & P . k = q ) ) ) );

( P . n in A or ex Q being GRZ-formula-finset st

( [Q,(P . n)] in R & ( for q being FinSequence st q in Q holds

ex k being Element of NAT st

( k in dom P & k < n & P . k = q ) ) ) );

:: deftheorem defines is_a_correct_step_wrt GRZLOG_1:def 29 :

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for P being GRZ-formula-sequence

for n being Element of NAT holds

( P,n is_a_correct_step_wrt A,R iff ( P . n in A or ex Q being GRZ-formula-finset st

( [Q,(P . n)] in R & ( for q being FinSequence st q in Q holds

ex k being Element of NAT st

( k in dom P & k < n & P . k = q ) ) ) ) );

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for P being GRZ-formula-sequence

for n being Element of NAT holds

( P,n is_a_correct_step_wrt A,R iff ( P . n in A or ex Q being GRZ-formula-finset st

( [Q,(P . n)] in R & ( for q being FinSequence st q in Q holds

ex k being Element of NAT st

( k in dom P & k < n & P . k = q ) ) ) ) );

definition

let A be non empty Subset of GRZ-formula-set;

let R be GRZ-rule;

let P be GRZ-formula-sequence;

end;
let R be GRZ-rule;

let P be GRZ-formula-sequence;

attr P is A,R -correct means :: GRZLOG_1:def 30

for k being Element of NAT st k in dom P holds

P,k is_a_correct_step_wrt A,R;

for k being Element of NAT st k in dom P holds

P,k is_a_correct_step_wrt A,R;

:: deftheorem defines -correct GRZLOG_1:def 30 :

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for P being GRZ-formula-sequence holds

( P is A,R -correct iff for k being Element of NAT st k in dom P holds

P,k is_a_correct_step_wrt A,R );

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for P being GRZ-formula-sequence holds

( P is A,R -correct iff for k being Element of NAT st k in dom P holds

P,k is_a_correct_step_wrt A,R );

definition

let A be non empty Subset of GRZ-formula-set;

let a be Element of A;

:: original: <*

redefine func <*a*> -> GRZ-formula-sequence;

coherence

<*a*> is GRZ-formula-sequence

end;
let a be Element of A;

:: original: <*

redefine func <*a*> -> GRZ-formula-sequence;

coherence

<*a*> is GRZ-formula-sequence

proof end;

theorem Th40: :: GRZLOG_1:9

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for a being Element of A holds <*a*> is A,R -correct

for R being GRZ-rule

for a being Element of A holds <*a*> is A,R -correct

proof end;

registration

let A be non empty Subset of GRZ-formula-set;

let R be GRZ-rule;

ex b_{1} being GRZ-formula-sequence st

( not b_{1} is empty & b_{1} is A,R -correct )

end;
let R be GRZ-rule;

cluster V1() V4( NAT ) V5( GRZ-formula-set ) non empty Function-like finite FinSequence-like FinSubsequence-like A,R -correct for FinSequence of GRZ-formula-set ;

existence ex b

( not b

proof end;

definition

let A be non empty Subset of GRZ-formula-set;

let R be GRZ-rule;

let S be GRZ-formula-finset;

end;
let R be GRZ-rule;

let S be GRZ-formula-finset;

attr S is A,R -correct means :: GRZLOG_1:def 31

ex P being GRZ-formula-sequence st

( S = rng P & P is A,R -correct );

ex P being GRZ-formula-sequence st

( S = rng P & P is A,R -correct );

:: deftheorem defines -correct GRZLOG_1:def 31 :

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for S being GRZ-formula-finset holds

( S is A,R -correct iff ex P being GRZ-formula-sequence st

( S = rng P & P is A,R -correct ) );

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for S being GRZ-formula-finset holds

( S is A,R -correct iff ex P being GRZ-formula-sequence st

( S = rng P & P is A,R -correct ) );

Lm40: for p, q being FinSequence

for k, m being Element of NAT st k in dom p & m in dom q & m < k holds

m in dom p

proof end;

Lm41: for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for P, P1, P2 being GRZ-formula-sequence

for n being Element of NAT 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 end;

theorem :: GRZLOG_1:10

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for P, P1, P2 being GRZ-formula-sequence st P is A,R -correct & P = P1 ^ P2 holds

P1 is A,R -correct

for R being GRZ-rule

for P, P1, P2 being GRZ-formula-sequence st P is A,R -correct & P = P1 ^ P2 holds

P1 is A,R -correct

proof end;

theorem Th42: :: GRZLOG_1:11

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for P1, P2 being GRZ-formula-sequence st P1 is A,R -correct & P2 is A,R -correct holds

P1 ^ P2 is A,R -correct

for R being GRZ-rule

for P1, P2 being GRZ-formula-sequence st P1 is A,R -correct & P2 is A,R -correct holds

P1 ^ P2 is A,R -correct

proof end;

theorem Th43: :: GRZLOG_1:12

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for S1, S2 being GRZ-formula-finset st S1 is A,R -correct & S2 is A,R -correct holds

S1 \/ S2 is A,R -correct

for R being GRZ-rule

for S1, S2 being GRZ-formula-finset st S1 is A,R -correct & S2 is A,R -correct holds

S1 \/ S2 is A,R -correct

proof end;

Lm44: for A, A1 being non empty Subset of GRZ-formula-set

for R, R1 being GRZ-rule

for P being GRZ-formula-sequence

for k being Element of NAT 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: :: GRZLOG_1:13

for A, A1 being non empty Subset of GRZ-formula-set

for R, R1 being GRZ-rule

for P being GRZ-formula-sequence st A c= A1 & R c= R1 & P is A,R -correct holds

P is A1,R1 -correct by Lm44;

for R, R1 being GRZ-rule

for P being GRZ-formula-sequence st A c= A1 & R c= R1 & P is A,R -correct holds

P is A1,R1 -correct by Lm44;

definition

let A be non empty Subset of GRZ-formula-set;

let R be GRZ-rule;

let t be GRZ-formula;

end;
let R be GRZ-rule;

let t be GRZ-formula;

pred A,R |- t means :: GRZLOG_1:def 32

ex P being GRZ-formula-sequence st

( t in rng P & P is A,R -correct );

ex P being GRZ-formula-sequence st

( t in rng P & P is A,R -correct );

:: deftheorem defines |- GRZLOG_1:def 32 :

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for t being GRZ-formula holds

( A,R |- t iff ex P being GRZ-formula-sequence st

( t in rng P & P is A,R -correct ) );

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for t being GRZ-formula holds

( A,R |- t iff ex P being GRZ-formula-sequence st

( t in rng P & P is A,R -correct ) );

definition
end;

:: deftheorem defines |- GRZLOG_1:def 33 :

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for B being Subset of GRZ-formula-set holds

( A,R |- B iff for t being GRZ-formula st t in B holds

A,R |- t );

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for B being Subset of GRZ-formula-set holds

( A,R |- B iff for t being GRZ-formula st t in B holds

A,R |- t );

theorem Th45: :: GRZLOG_1:14

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for t being GRZ-formula holds

( A,R |- t iff ex S being GRZ-formula-finset st

( t in S & S is A,R -correct ) )

for R being GRZ-rule

for t being GRZ-formula holds

( A,R |- t iff ex S being GRZ-formula-finset st

( t in S & S is A,R -correct ) )

proof end;

theorem Th46: :: GRZLOG_1:15

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for t being GRZ-formula st t in A holds

A,R |- t

for R being GRZ-rule

for t being GRZ-formula st t in A holds

A,R |- t

proof end;

theorem Th47: :: GRZLOG_1:16

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for S being GRZ-formula-finset st A,R |- S holds

ex S1 being GRZ-formula-finset st

( S c= S1 & S1 is A,R -correct )

for R being GRZ-rule

for S being GRZ-formula-finset st A,R |- S holds

ex S1 being GRZ-formula-finset st

( S c= S1 & S1 is A,R -correct )

proof end;

theorem Th48: :: GRZLOG_1:17

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for t being GRZ-formula

for S being GRZ-formula-finset st A,R |- S & [S,t] in R holds

A,R |- t

for R being GRZ-rule

for t being GRZ-formula

for S being GRZ-formula-finset st A,R |- S & [S,t] in R holds

A,R |- t

proof end;

theorem :: GRZLOG_1:18

for A being non empty Subset of GRZ-formula-set

for R being GRZ-rule

for t being GRZ-formula holds

( not A,R |- t or t in A or ex S being GRZ-formula-finset st

( [S,t] in R & A,R |- S ) )

for R being GRZ-rule

for t being GRZ-formula holds

( not A,R |- t or t in A or ex S being GRZ-formula-finset st

( [S,t] in R & A,R |- S ) )

proof end;

theorem :: GRZLOG_1:19

for A, A1 being non empty Subset of GRZ-formula-set

for R, R1 being GRZ-rule

for t being GRZ-formula st A c= A1 & R c= R1 & A,R |- t holds

A1,R1 |- t by Th44;

for R, R1 being GRZ-rule

for t being GRZ-formula st A c= A1 & R c= R1 & A,R |- t holds

A1,R1 |- t by Th44;

theorem Th60: :: GRZLOG_1:20

for A being non empty Subset of GRZ-formula-set

for t, u being GRZ-formula holds

( A, GRZ-rules |- t '&' u iff ( A, GRZ-rules |- t & A, GRZ-rules |- u ) )

for t, u being GRZ-formula holds

( A, GRZ-rules |- t '&' u iff ( A, GRZ-rules |- t & A, GRZ-rules |- u ) )

proof end;

theorem Th61: :: GRZLOG_1:21

for A being non empty Subset of GRZ-formula-set

for t, u being GRZ-formula st A, GRZ-rules |- t & A, GRZ-rules |- t '=' u holds

A, GRZ-rules |- u

for t, u being GRZ-formula st A, GRZ-rules |- t & A, GRZ-rules |- t '=' u holds

A, GRZ-rules |- u

proof end;

theorem Th62: :: GRZLOG_1:22

for A being non empty Subset of GRZ-formula-set

for t, u being GRZ-formula st A, GRZ-rules |- t & A, GRZ-rules |- t => u holds

A, GRZ-rules |- u

for t, u being GRZ-formula st A, GRZ-rules |- t & A, GRZ-rules |- t => u holds

A, GRZ-rules |- u

proof end;

theorem :: GRZLOG_1:23

for A being non empty Subset of GRZ-formula-set

for t, u being GRZ-formula st A, GRZ-rules |- t '&' u holds

A, GRZ-rules |- u '&' t

for t, u being GRZ-formula st A, GRZ-rules |- t '&' u holds

A, GRZ-rules |- u '&' t

proof end;

:: deftheorem defines GRZ-axiomatic GRZLOG_1:def 34 :

for t being GRZ-formula holds

( t is GRZ-axiomatic iff t in GRZ-axioms );

for t being GRZ-formula holds

( t is GRZ-axiomatic iff t in GRZ-axioms );

:: deftheorem defines GRZ-provable GRZLOG_1:def 35 :

for t being GRZ-formula holds

( t is GRZ-provable iff GRZ-axioms , GRZ-rules |- t );

for t being GRZ-formula holds

( t is GRZ-provable iff GRZ-axioms , GRZ-rules |- t );

:: deftheorem defines LD-axiomatic GRZLOG_1:def 36 :

for t being GRZ-formula holds

( t is LD-axiomatic iff t in LD-axioms );

for t being GRZ-formula holds

( t is LD-axiomatic iff t in LD-axioms );

:: deftheorem defines LD-provable GRZLOG_1:def 37 :

for t being GRZ-formula holds

( t is LD-provable iff LD-axioms , GRZ-rules |- t );

for t being GRZ-formula holds

( t is LD-provable iff LD-axioms , GRZ-rules |- t );

registration

let t be GRZ-formula;

coherence

'not' (t '&' ('not' t)) is GRZ-axiomatic by Def10;

coherence

('not' ('not' t)) '=' t is GRZ-axiomatic by Def10;

coherence

t '=' (t '&' t) is GRZ-axiomatic by Def10;

let u be GRZ-formula;

coherence

(t '&' u) '=' (u '&' t) is GRZ-axiomatic by Def10;

coherence

('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) is GRZ-axiomatic by Def10;

coherence

(t '=' u) '=' (u '=' t) is GRZ-axiomatic by Def10;

coherence

(t '=' u) '=' (('not' t) '=' ('not' u)) is GRZ-axiomatic by Def10;

let v be GRZ-formula;

coherence

(t '&' (u '&' v)) '=' ((t '&' u) '&' v) is GRZ-axiomatic by Def10;

coherence

(t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) is GRZ-axiomatic by Def10;

coherence

(t '=' u) => ((t '&' v) '=' (u '&' v)) is LD-axiomatic

(t '=' u) => ((t 'or' v) '=' (u 'or' v)) is LD-axiomatic

(t '=' u) => ((t '=' v) '=' (u '=' v)) is LD-axiomatic

end;
coherence

'not' (t '&' ('not' t)) is GRZ-axiomatic by Def10;

coherence

('not' ('not' t)) '=' t is GRZ-axiomatic by Def10;

coherence

t '=' (t '&' t) is GRZ-axiomatic by Def10;

let u be GRZ-formula;

coherence

(t '&' u) '=' (u '&' t) is GRZ-axiomatic by Def10;

coherence

('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) is GRZ-axiomatic by Def10;

coherence

(t '=' u) '=' (u '=' t) is GRZ-axiomatic by Def10;

coherence

(t '=' u) '=' (('not' t) '=' ('not' u)) is GRZ-axiomatic by Def10;

let v be GRZ-formula;

coherence

(t '&' (u '&' v)) '=' ((t '&' u) '&' v) is GRZ-axiomatic by Def10;

coherence

(t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) is GRZ-axiomatic by Def10;

coherence

(t '=' u) => ((t '&' v) '=' (u '&' v)) is LD-axiomatic

proof end;

coherence (t '=' u) => ((t 'or' v) '=' (u 'or' v)) is LD-axiomatic

proof end;

coherence (t '=' u) => ((t '=' v) '=' (u '=' v)) is LD-axiomatic

proof end;

registration

coherence

for b_{1} being GRZ-formula st b_{1} is GRZ-axiomatic holds

b_{1} is LD-axiomatic
by XBOOLE_0:def 3;

coherence

for b_{1} being GRZ-formula st b_{1} is GRZ-axiomatic holds

b_{1} is GRZ-provable
by Th46;

coherence

for b_{1} being GRZ-formula st b_{1} is LD-axiomatic holds

b_{1} is LD-provable
by Th46;

coherence

for b_{1} being GRZ-formula st b_{1} is GRZ-provable holds

b_{1} is LD-provable

end;
for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

proof end;

registration

ex b_{1} being GRZ-formula st

( b_{1} is GRZ-axiomatic & b_{1} is GRZ-provable & b_{1} is LD-axiomatic & b_{1} is LD-provable )
end;

cluster V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like GRZ-axiomatic GRZ-provable LD-axiomatic LD-provable for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);

existence ex b

( b

proof end;

theorem Th70: :: GRZLOG_1:24

for A being non empty Subset of GRZ-formula-set

for t, u being GRZ-formula st GRZ-axioms c= A & A, GRZ-rules |- t '=' u holds

A, GRZ-rules |- u '=' t

for t, u being GRZ-formula st GRZ-axioms c= A & A, GRZ-rules |- t '=' u holds

A, GRZ-rules |- u '=' t

proof end;

theorem :: GRZLOG_1:25

theorem :: GRZLOG_1:26

for t, u being GRZ-formula st t '=' u is LD-provable holds

u '=' t is LD-provable by Th70, XBOOLE_1:7;

u '=' t is LD-provable by Th70, XBOOLE_1:7;

theorem Th74: :: GRZLOG_1:27

for t, u, v being GRZ-formula st t '=' u is LD-provable & u '=' v is LD-provable holds

t '=' v is LD-provable

t '=' v is LD-provable

proof end;

definition

let t, u be GRZ-formula;

reflexivity

for t being GRZ-formula holds t '=' t is LD-provable by Th75;

symmetry

for t, u being GRZ-formula st t '=' u is LD-provable holds

u '=' t is LD-provable by Th70, XBOOLE_1:7;

end;
reflexivity

for t being GRZ-formula holds t '=' t is LD-provable by Th75;

symmetry

for t, u being GRZ-formula st t '=' u is LD-provable holds

u '=' t is LD-provable by Th70, XBOOLE_1:7;

:: deftheorem Def76 defines LD-= GRZLOG_1:def 38 :

for t, u being GRZ-formula holds

( t LD-= u iff t '=' u is LD-provable );

for t, u being GRZ-formula holds

( t LD-= u iff t '=' u is LD-provable );

scheme :: GRZLOG_1:sch 1

BinReplace{ F_{1}() -> non empty set , F_{2}( Element of F_{1}(), Element of F_{1}()) -> Element of F_{1}(), P_{1}[ Element of F_{1}(), Element of F_{1}()] } :

BinReplace{ F

for a, b, c, d being Element of F_{1}() st P_{1}[a,b] & P_{1}[c,d] holds

P_{1}[F_{2}(a,c),F_{2}(b,d)]

providedP

A2:
for a, b, c being Element of F_{1}() st P_{1}[a,b] & P_{1}[b,c] holds

P_{1}[a,c]
and

A3: for a, b being Element of F_{1}() holds P_{1}[F_{2}(a,b),F_{2}(b,a)]
and

A4: for a, b, c being Element of F_{1}() st P_{1}[a,b] holds

P_{1}[F_{2}(a,c),F_{2}(b,c)]

P

A3: for a, b being Element of F

A4: for a, b, c being Element of F

P

proof end;

Lm77a: for t, u, v being GRZ-formula st t '=' u is LD-provable holds

(t '&' v) '=' (u '&' v) is LD-provable

proof end;

Lm78a: for t, u, v being GRZ-formula st t '=' u is LD-provable holds

(t '=' v) '=' (u '=' v) is LD-provable

proof end;

definition

ex b_{1} being Equivalence_Relation of GRZ-formula-set st

for t, u being GRZ-formula holds

( [t,u] in b_{1} iff t LD-= u )

for b_{1}, b_{2} being Equivalence_Relation of GRZ-formula-set st ( for t, u being GRZ-formula holds

( [t,u] in b_{1} iff t LD-= u ) ) & ( for t, u being GRZ-formula holds

( [t,u] in b_{2} iff t LD-= u ) ) holds

b_{1} = b_{2}
end;

func LD-EqR -> Equivalence_Relation of GRZ-formula-set means :Def80: :: GRZLOG_1:def 39

for t, u being GRZ-formula holds

( [t,u] in it iff t LD-= u );

existence for t, u being GRZ-formula holds

( [t,u] in it iff t LD-= u );

ex b

for t, u being GRZ-formula holds

( [t,u] in b

proof end;

uniqueness for b

( [t,u] in b

( [t,u] in b

b

proof end;

:: deftheorem Def80 defines LD-EqR GRZLOG_1:def 39 :

for b_{1} being Equivalence_Relation of GRZ-formula-set holds

( b_{1} = LD-EqR iff for t, u being GRZ-formula holds

( [t,u] in b_{1} iff t LD-= u ) );

for b

( b

( [t,u] in b

registration
end;

definition

Class LD-EqR is non empty Subset-Family of GRZ-formula-set ;

end;

func LD-EqClasses -> non empty Subset-Family of GRZ-formula-set equals :: GRZLOG_1:def 40

Class LD-EqR;

coherence Class LD-EqR;

Class LD-EqR is non empty Subset-Family of GRZ-formula-set ;

:: deftheorem defines LD-EqClassOf GRZLOG_1:def 41 :

for t being GRZ-formula holds LD-EqClassOf t = Class (LD-EqR,t);

for t being GRZ-formula holds LD-EqClassOf t = Class (LD-EqR,t);

scheme :: GRZLOG_1:sch 2

UnOpCongr{ F_{1}() -> non empty set , F_{2}( Element of F_{1}()) -> Element of F_{1}(), F_{3}() -> Equivalence_Relation of F_{1}() } :

UnOpCongr{ F

ex f being UnOp of (Class F_{3}()) st

for x being Element of F_{1}() holds f . (Class (F_{3}(),x)) = Class (F_{3}(),F_{2}(x))

provided
for x being Element of F

proof end;

scheme :: GRZLOG_1:sch 3

BinOpCongr{ F_{1}() -> non empty set , F_{2}( Element of F_{1}(), Element of F_{1}()) -> Element of F_{1}(), F_{3}() -> Equivalence_Relation of F_{1}() } :

BinOpCongr{ F

ex f being BinOp of (Class F_{3}()) st

for x, y being Element of F_{1}() holds f . ((Class (F_{3}(),x)),(Class (F_{3}(),y))) = Class (F_{3}(),F_{2}(x,y))

providedfor x, y being Element of F

A1:
for x1, x2, y1, y2 being Element of F_{1}() st [x1,x2] in F_{3}() & [y1,y2] in F_{3}() holds

[F_{2}(x1,y1),F_{2}(x2,y2)] in F_{3}()

[F

proof end;

definition

let x be LD-EqClass;

ex b_{1} being LD-EqClass ex t being GRZ-formula st

( x = LD-EqClassOf t & b_{1} = LD-EqClassOf ('not' t) )

for b_{1}, b_{2} being LD-EqClass st ex t being GRZ-formula st

( x = LD-EqClassOf t & b_{1} = LD-EqClassOf ('not' t) ) & ex t being GRZ-formula st

( x = LD-EqClassOf t & b_{2} = LD-EqClassOf ('not' t) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being LD-EqClass st ex t being GRZ-formula st

( b_{2} = LD-EqClassOf t & b_{1} = LD-EqClassOf ('not' t) ) holds

ex t being GRZ-formula st

( b_{1} = LD-EqClassOf t & b_{2} = LD-EqClassOf ('not' t) )

ex b_{1} being LD-EqClass ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & b_{1} = LD-EqClassOf (t '&' u) )

for b_{1}, b_{2} being LD-EqClass st ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & b_{1} = LD-EqClassOf (t '&' u) ) & ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & b_{2} = LD-EqClassOf (t '&' u) ) holds

b_{1} = b_{2}

for b_{1}, x, y being LD-EqClass st ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & b_{1} = LD-EqClassOf (t '&' u) ) holds

ex t, u being GRZ-formula st

( y = LD-EqClassOf t & x = LD-EqClassOf u & b_{1} = LD-EqClassOf (t '&' u) )

for x being LD-EqClass ex t, u being GRZ-formula st

( x = LD-EqClassOf t & x = LD-EqClassOf u & x = LD-EqClassOf (t '&' u) )

ex b_{1} being LD-EqClass ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & b_{1} = LD-EqClassOf (t '=' u) )

for b_{1}, b_{2} being LD-EqClass st ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & b_{1} = LD-EqClassOf (t '=' u) ) & ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & b_{2} = LD-EqClassOf (t '=' u) ) holds

b_{1} = b_{2}

for b_{1}, x, y being LD-EqClass st ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & b_{1} = LD-EqClassOf (t '=' u) ) holds

ex t, u being GRZ-formula st

( y = LD-EqClassOf t & x = LD-EqClassOf u & b_{1} = LD-EqClassOf (t '=' u) )

end;
attr x is LD-provable means :: GRZLOG_1:def 42

ex t being GRZ-formula st

( x = LD-EqClassOf t & t is LD-provable );

ex t being GRZ-formula st

( x = LD-EqClassOf t & t is LD-provable );

func 'not' x -> LD-EqClass means :Def91: :: GRZLOG_1:def 43

ex t being GRZ-formula st

( x = LD-EqClassOf t & it = LD-EqClassOf ('not' t) );

existence ex t being GRZ-formula st

( x = LD-EqClassOf t & it = LD-EqClassOf ('not' t) );

ex b

( x = LD-EqClassOf t & b

proof end;

uniqueness for b

( x = LD-EqClassOf t & b

( x = LD-EqClassOf t & b

b

proof end;

involutiveness for b

( b

ex t being GRZ-formula st

( b

proof end;

let y be LD-EqClass;
func x '&' y -> LD-EqClass means :Def92: :: GRZLOG_1:def 44

ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & it = LD-EqClassOf (t '&' u) );

existence ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & it = LD-EqClassOf (t '&' u) );

ex b

( x = LD-EqClassOf t & y = LD-EqClassOf u & b

proof end;

uniqueness for b

( x = LD-EqClassOf t & y = LD-EqClassOf u & b

( x = LD-EqClassOf t & y = LD-EqClassOf u & b

b

proof end;

commutativity for b

( x = LD-EqClassOf t & y = LD-EqClassOf u & b

ex t, u being GRZ-formula st

( y = LD-EqClassOf t & x = LD-EqClassOf u & b

proof end;

idempotence for x being LD-EqClass ex t, u being GRZ-formula st

( x = LD-EqClassOf t & x = LD-EqClassOf u & x = LD-EqClassOf (t '&' u) )

proof end;

func x '=' y -> LD-EqClass means :Def93: :: GRZLOG_1:def 45

ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & it = LD-EqClassOf (t '=' u) );

existence ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & it = LD-EqClassOf (t '=' u) );

ex b

( x = LD-EqClassOf t & y = LD-EqClassOf u & b

proof end;

uniqueness for b

( x = LD-EqClassOf t & y = LD-EqClassOf u & b

( x = LD-EqClassOf t & y = LD-EqClassOf u & b

b

proof end;

commutativity for b

( x = LD-EqClassOf t & y = LD-EqClassOf u & b

ex t, u being GRZ-formula st

( y = LD-EqClassOf t & x = LD-EqClassOf u & b

proof end;

:: deftheorem defines LD-provable GRZLOG_1:def 42 :

for x being LD-EqClass holds

( x is LD-provable iff ex t being GRZ-formula st

( x = LD-EqClassOf t & t is LD-provable ) );

for x being LD-EqClass holds

( x is LD-provable iff ex t being GRZ-formula st

( x = LD-EqClassOf t & t is LD-provable ) );

:: deftheorem Def91 defines 'not' GRZLOG_1:def 43 :

for x, b_{2} being LD-EqClass holds

( b_{2} = 'not' x iff ex t being GRZ-formula st

( x = LD-EqClassOf t & b_{2} = LD-EqClassOf ('not' t) ) );

for x, b

( b

( x = LD-EqClassOf t & b

:: deftheorem Def92 defines '&' GRZLOG_1:def 44 :

for x, y, b_{3} being LD-EqClass holds

( b_{3} = x '&' y iff ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & b_{3} = LD-EqClassOf (t '&' u) ) );

for x, y, b

( b

( x = LD-EqClassOf t & y = LD-EqClassOf u & b

:: deftheorem Def93 defines '=' GRZLOG_1:def 45 :

for x, y, b_{3} being LD-EqClass holds

( b_{3} = x '=' y iff ex t, u being GRZ-formula st

( x = LD-EqClassOf t & y = LD-EqClassOf u & b_{3} = LD-EqClassOf (t '=' u) ) );

for x, y, b

( b

( x = LD-EqClassOf t & y = LD-EqClassOf u & b

definition

let x, y be LD-EqClass;

coherence

'not' (('not' x) '&' ('not' y)) is LD-EqClass ;

commutativity

for b_{1}, x, y being LD-EqClass st b_{1} = 'not' (('not' x) '&' ('not' y)) holds

b_{1} = 'not' (('not' y) '&' ('not' x))
;

idempotence

for x being LD-EqClass holds x = 'not' (('not' x) '&' ('not' x)) ;

coherence

x '=' (x '&' y) is LD-EqClass ;

end;
coherence

'not' (('not' x) '&' ('not' y)) is LD-EqClass ;

commutativity

for b

b

idempotence

for x being LD-EqClass holds x = 'not' (('not' x) '&' ('not' x)) ;

coherence

x '=' (x '&' y) is LD-EqClass ;

:: deftheorem defines 'or' GRZLOG_1:def 46 :

for x, y being LD-EqClass holds x 'or' y = 'not' (('not' x) '&' ('not' y));

for x, y being LD-EqClass holds x 'or' y = 'not' (('not' x) '&' ('not' y));

:: deftheorem defines => GRZLOG_1:def 47 :

for x, y being LD-EqClass holds x => y = x '=' (x '&' y);

for x, y being LD-EqClass holds x => y = x '=' (x '&' y);

theorem Th91: :: GRZLOG_1:35

for x, y being LD-EqClass holds

( x '&' y is LD-provable iff ( x is LD-provable & y is LD-provable ) )

( x '&' y is LD-provable iff ( x is LD-provable & y is LD-provable ) )

proof end;

theorem :: GRZLOG_1:37

theorem :: GRZLOG_1:38

for t, u being GRZ-formula holds LD-EqClassOf (t '&' u) = (LD-EqClassOf t) '&' (LD-EqClassOf u) by Def92;

theorem :: GRZLOG_1:39

for t, u being GRZ-formula holds LD-EqClassOf (t '=' u) = (LD-EqClassOf t) '=' (LD-EqClassOf u) by Def93;

theorem :: GRZLOG_1:43

theorem Th101: :: GRZLOG_1:44

for x, y, z being LD-EqClass st x => y is LD-provable & y => z is LD-provable holds

x => z is LD-provable

x => z is LD-provable

proof end;

theorem :: GRZLOG_1:45

for t, u, v being GRZ-formula st t => u is LD-provable & u => v is LD-provable holds

t => v is LD-provable

t => v is LD-provable

proof end;

theorem :: GRZLOG_1:46

:: The Construction of Grzegorczyk's LD Language

::