:: Fundamentals of Finitary Proofs
:: by Taneli Huuskonen
::
:: Received December 24, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

::
:: The Construction of a Proof
::

definition

let R be Relation;

attr R is finitary means :Def1: :: PROOFS_1:def 1
for a being object st a in dom R holds
a is finite set ;

end;

:: deftheorem Def1 defines finitary PROOFS_1:def 1 :
for R being Relation holds
( R is finitary iff for a being object st a in dom R holds
a is finite set );

registration

cluster Relation-like empty -> finitary for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is finitary ;

cluster Relation-like finitary for set ;

existence
ex b₁ being Relation st b₁ is finitary by XBOOLE_0:def 2;

end;

notation

synonym Formula for object ;

end;

definition

mode Rule is finitary Relation;
mode Formula-finset is finite set ;
mode Formula-sequence is FinSequence;

end;

definition

let Fml be set ;

mode Rule of Fml -> Rule means :Def2: :: PROOFS_1:def 2
( dom it c= Fin Fml & rng it c= Fml );

existence
ex b₁ being Rule st
( dom b₁ c= Fin Fml & rng b₁ c= Fml )

proof end;

end;

:: deftheorem Def2 defines Rule PROOFS_1:def 2 :
for Fml being set
for b₂ being Rule holds
( b₂ is Rule of Fml iff ( dom b₂ c= Fin Fml & rng b₂ c= Fml ) );

definition

let Fml be non empty set ;

mode Formula of Fml -> Formula means :Def3: :: PROOFS_1:def 3
it in Fml;

existence
ex b₁ being Formula st b₁ in Fml

proof end;

end;

:: deftheorem Def3 defines Formula PROOFS_1:def 3 :
for Fml being non empty set
for b₂ being Formula holds
( b₂ is Formula of Fml iff b₂ in Fml );

definition

let Fml be set ;

mode Formula-finset of Fml -> Formula-finset means :Def4: :: PROOFS_1:def 4
it c= Fml;

existence
ex b₁ being Formula-finset st b₁ c= Fml by XBOOLE_1:2;

mode Formula-sequence of Fml -> Formula-sequence means :Def5: :: PROOFS_1:def 5
it is FinSequence of Fml;

existence
ex b₁ being Formula-sequence st b₁ is FinSequence of Fml

proof end;

end;

:: deftheorem Def4 defines Formula-finset PROOFS_1:def 4 :
for Fml being set
for b₂ being Formula-finset holds
( b₂ is Formula-finset of Fml iff b₂ c= Fml );

:: deftheorem Def5 defines Formula-sequence PROOFS_1:def 5 :
for Fml being set
for b₂ being Formula-sequence holds
( b₂ is Formula-sequence of Fml iff b₂ is FinSequence of Fml );

definition

let P be Formula-sequence;
:: original: rng
redefine func rng P -> Formula-finset;
coherence
rng P is Formula-finset ;

end;

definition

let Fml be non empty set ;
let B1, B2 be Subset of Fml;
:: original: \/
redefine func B1 \/ B2 -> Subset of Fml;
coherence
B1 \/ B2 is Subset of Fml by XBOOLE_1:8;

end;

definition

let S1, S2 be Formula-finset;
:: original: \/
redefine func S1 \/ S2 -> Formula-finset;
coherence
S1 \/ S2 is Formula-finset ;

end;

definition

let Fml be non empty set ;
let S1, S2 be Formula-finset of Fml;
:: original: \/
redefine func S1 \/ S2 -> Formula-finset of Fml;
coherence
S1 \/ S2 is Formula-finset of Fml

proof end;

end;

definition

let R1, R2 be Rule;
:: original: \/
redefine func R1 \/ R2 -> Rule;
coherence
R1 \/ R2 is Rule

proof end;

end;

definition

let Fml be non empty set ;
let R1, R2 be Rule of Fml;
:: original: \/
redefine func R1 \/ R2 -> Rule of Fml;
coherence
R1 \/ R2 is Rule of Fml

proof end;

end;

definition

let B be set ;
let R be Rule;
let P be Formula-sequence;
let n be Nat;

pred P,n is_a_correct_step_wrt B,R means :: PROOFS_1:def 6
( P . n in B or ex Q being Formula-finset st
( [Q,(P . n)] in R & ( for t being object st t in Q holds
ex k being Nat st
( k in dom P & k < n & P . k = t ) ) ) );

end;

:: deftheorem defines is_a_correct_step_wrt PROOFS_1:def 6 :
for B being set
for R being Rule
for P being Formula-sequence
for n being Nat holds
( P,n is_a_correct_step_wrt B,R iff ( P . n in B or ex Q being Formula-finset st
( [Q,(P . n)] in R & ( for t being object st t in Q holds
ex k being Nat st
( k in dom P & k < n & P . k = t ) ) ) ) );

definition

let B be set ;
let R be Rule;
let P be Formula-sequence;

attr P is B,R -correct means :: PROOFS_1:def 7
for k being Nat st k in dom P holds
P,k is_a_correct_step_wrt B,R;

end;

:: deftheorem defines -correct PROOFS_1:def 7 :
for B being set
for R being Rule
for P being Formula-sequence holds
( P is B,R -correct iff for k being Nat st k in dom P holds
P,k is_a_correct_step_wrt B,R );

registration

let B be set ;
let R be Rule;

cluster Relation-like Function-like FinSequence-like non B,R -correct -> non empty for set ;

coherence
for b₁ being Formula-sequence st not b₁ is B,R -correct holds
not b₁ is empty ;
let Fml be non empty set ;

cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like B,R -correct for Formula-sequence of Fml;

existence
ex b₁ being Formula-sequence of Fml st b₁ is B,R -correct

proof end;

end;

registration

let B be set ;
let R be Rule;

cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like B,R -correct for set ;

existence
ex b₁ being Formula-sequence st b₁ is B,R -correct

proof end;

end;

theorem Th40: :: PROOFS_1:1

for A being non empty set
for R being Rule
for a being Element of A holds <*a*> is A,R -correct

proof end;

registration

let A be non empty set ;
let R be Rule;

cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like A,R -correct for set ;

existence
ex b₁ being Formula-sequence st
( not b₁ is empty & b₁ is A,R -correct )

proof end;

end;

definition

let B be set ;
let R be Rule;
let S be Formula-finset;

attr S is B,R -derivable means :: PROOFS_1:def 8
ex P being Formula-sequence st
( S = rng P & P is B,R -correct );

end;

:: deftheorem defines -derivable PROOFS_1:def 8 :
for B being set
for R being Rule
for S being Formula-finset holds
( S is B,R -derivable iff ex P being Formula-sequence st
( S = rng P & P is B,R -correct ) );

Lm40: for p, q being FinSequence
for k, m being Nat st k in dom p & m in dom q & m < k holds
m in dom p

proof end;

Lm41: for B being set
for R being Rule
for P, P1, P2 being Formula-sequence
for n being Nat st n in dom P & P ^ P1,n is_a_correct_step_wrt B,R holds
P ^ P2,n is_a_correct_step_wrt B,R

proof end;

theorem :: PROOFS_1:2

for B being set
for R being Rule
for P, P1, P2 being Formula-sequence st P is B,R -correct & P = P1 ^ P2 holds
P1 is B,R -correct

proof end;

theorem Th42: :: PROOFS_1:3

for B being set
for R being Rule
for P1, P2 being Formula-sequence st P1 is B,R -correct & P2 is B,R -correct holds
P1 ^ P2 is B,R -correct

proof end;

theorem Th43: :: PROOFS_1:4

for B being set
for R being Rule
for S1, S2 being Formula-finset st S1 is B,R -derivable & S2 is B,R -derivable holds
S1 \/ S2 is B,R -derivable

proof end;

Lm44: for B, B1 being set
for R, R1 being Rule
for P being Formula-sequence
for k being Nat st B c= B1 & R c= R1 & P,k is_a_correct_step_wrt B,R holds
P,k is_a_correct_step_wrt B1,R1
;

theorem Th44: :: PROOFS_1:5

for B, B1 being set
for R, R1 being Rule
for P being Formula-sequence st B c= B1 & R c= R1 & P is B,R -correct holds
P is B1,R1 -correct by Lm44;

definition

let B be set ;
let a be object ;

attr a is B -axiomatic means :: PROOFS_1:def 9
a in B;

let R be Rule;

pred B,R |- a means :: PROOFS_1:def 10
ex P being Formula-sequence st
( a in rng P & P is B,R -correct );

end;

:: deftheorem defines -axiomatic PROOFS_1:def 9 :
for B being set
for a being object holds
( a is B -axiomatic iff a in B );

:: deftheorem defines |- PROOFS_1:def 10 :
for B being set
for a being object
for R being Rule holds
( B,R |- a iff ex P being Formula-sequence st
( a in rng P & P is B,R -correct ) );

definition

let B be set ;
let R be Rule;
let a be object ;

attr a is B,R -provable means :: PROOFS_1:def 11
B,R |- a;

end;

:: deftheorem defines -provable PROOFS_1:def 11 :
for B being set
for R being Rule
for a being object holds
( a is B,R -provable iff B,R |- a );

definition

let B, B1 be set ;

attr B1 is B -extending means :Def11: :: PROOFS_1:def 12
B c= B1;

end;

:: deftheorem Def11 defines -extending PROOFS_1:def 12 :
for B, B1 being set holds
( B1 is B -extending iff B c= B1 );

definition

let R, R1 be Rule;

attr R1 is R -extending means :Def12: :: PROOFS_1:def 13
R c= R1;

end;

:: deftheorem Def12 defines -extending PROOFS_1:def 13 :
for R, R1 being Rule holds
( R1 is R -extending iff R c= R1 );

registration

let B be set ;

cluster B -extending for set ;

existence
ex b₁ being set st b₁ is B -extending

proof end;

end;

registration

let R be Rule;

cluster Relation-like finitary R -extending for set ;

existence
ex b₁ being Rule st b₁ is R -extending

proof end;

end;

definition

let B be set ;
mode Extension of B is B -extending set ;

end;

registration

let Fml be non empty set ;
let B be Subset of Fml;

cluster B -extending for Element of bool Fml;

existence
ex b₁ being Subset of Fml st b₁ is B -extending

proof end;

end;

definition

let Fml be non empty set ;
let B be Subset of Fml;
mode Extension of B is B -extending Subset of Fml;

end;

definition

let R be Rule;
mode Extension of R is R -extending Rule;

end;

definition

let Fml be non empty set ;
let B be Subset of Fml;
let t be Formula of Fml;

func B + t -> Extension of B equals :: PROOFS_1:def 14
B \/ {t};

coherence
B \/ {t} is Extension of B

proof end;

end;

:: deftheorem defines + PROOFS_1:def 14 :
for Fml being non empty set
for B being Subset of Fml
for t being Formula of Fml holds B + t = B \/ {t};

theorem :: PROOFS_1:6

for B being set
for t, a being object holds
( a is B \/ {t} -axiomatic iff ( a is B -axiomatic or a = t ) )

proof end;

registration

let B be set ;
let C be Extension of B;

cluster C -extending -> B -extending for set ;

coherence
for b₁ being set st b₁ is C -extending holds
b₁ is B -extending

proof end;

cluster non C -axiomatic -> non B -axiomatic for Formula ;

coherence
for b₁ being object st not b₁ is C -axiomatic holds
not b₁ is B -axiomatic

proof end;

end;

registration

let R be Rule;
let E be Extension of R;

cluster Relation-like finitary E -extending -> R -extending for set ;

coherence
for b₁ being Rule st b₁ is E -extending holds
b₁ is R -extending

proof end;

end;

definition

let B be set ;
let R, R1 be Rule;

attr R1 is B,R -derivable means :: PROOFS_1:def 15
for S being Formula-finset
for t being object st [S,t] in R1 holds
B \/ S,R |- t;

end;

:: deftheorem defines -derivable PROOFS_1:def 15 :
for B being set
for R, R1 being Rule holds
( R1 is B,R -derivable iff for S being Formula-finset
for t being object st [S,t] in R1 holds
B \/ S,R |- t );

theorem Th45: :: PROOFS_1:7

for B being set
for R being Rule
for t being object holds
( B,R |- t iff ex S being Formula-finset st
( t in S & S is B,R -derivable ) )

proof end;

theorem Th46: :: PROOFS_1:8

for B being set
for R being Rule
for a being object st a in B holds
B,R |- a

proof end;

registration

let B be set ;
let R be Rule;

cluster non B,R -provable -> non B -axiomatic for Formula ;

coherence
for b₁ being object st not b₁ is B,R -provable holds
not b₁ is B -axiomatic by Th46;

end;

theorem Th47: :: PROOFS_1:9

for B being set
for R being Rule
for S being Formula-finset st ( for a being object st a in S holds
B,R |- a ) holds
ex S1 being Formula-finset st
( S c= S1 & S1 is B,R -derivable )

proof end;

theorem Th48: :: PROOFS_1:10

for B, B1 being set
for R being Rule
for S being Formula-finset st S is B,R -derivable & B /\ S c= B1 holds
S is B1,R -derivable

proof end;

theorem Th49: :: PROOFS_1:11

for B being set
for R being Rule
for t being object
for S being Formula-finset st ( for a being object st a in S holds
B,R |- a ) & [S,t] in R holds
B,R |- t

proof end;

theorem Th51: :: PROOFS_1:12

for B being set
for R being Rule
for a being object holds
( not B,R |- a or a in B or ex S being Formula-finset st
( [S,a] in R & ( for b being object st b in S holds
B,R |- b ) ) )

proof end;

Lm52: for B being set
for R being Rule
for P being Formula-sequence
for m, n being Nat st P,m is_a_correct_step_wrt B,R & m <= n & P . m = P . n holds
P,n is_a_correct_step_wrt B,R

proof end;

theorem Th52: :: PROOFS_1:13

for B being set
for R being Rule
for S1, S2 being Formula-finset st S1 is B,R -derivable & S2 is S1,R -derivable holds
S1 \/ S2 is B,R -derivable

proof end;

theorem Th53: :: PROOFS_1:14

for B being set
for R being Rule
for B1 being set
for a being object st B1,R |- a & ( for b being object st b in B1 holds
B,R |- b ) holds
B,R |- a

proof end;

theorem Th54: :: PROOFS_1:15

for B being set
for C being Extension of B
for R being Rule
for E being Extension of R
for a being object st B,R |- a holds
C,E |- a

proof end;

definition

let B be set ;
let R be Rule;
let a be object ;

redefine attr a is B,R -provable means :: PROOFS_1:def 16
for C being Extension of B
for E being Extension of R holds C,E |- a;

compatibility
( a is B,R -provable iff for C being Extension of B
for E being Extension of R holds C,E |- a )

proof end;

end;

:: deftheorem defines -provable PROOFS_1:def 16 :
for B being set
for R being Rule
for a being object holds
( a is B,R -provable iff for C being Extension of B
for E being Extension of R holds C,E |- a );

registration

let B be set ;
let R be Rule;
let C be Extension of B;

cluster non C,R -provable -> non B,R -provable for Formula ;

coherence
for b₁ being object st not b₁ is C,R -provable holds
not b₁ is B,R -provable ;
let E be Extension of R;

cluster non C,E -provable -> non B,R -provable for Formula ;

coherence
for b₁ being object st not b₁ is C,E -provable holds
not b₁ is B,R -provable ;

end;

theorem :: PROOFS_1:16

for B being set
for R, R1, R2 being Rule holds
( R1 \/ R2 is B,R -derivable iff ( R1 is B,R -derivable & R2 is B,R -derivable ) )

proof end;

Lm54: for B being set
for R being Rule
for t being object st B,R |- t holds
t in B \/ (rng R)

proof end;

Lm55: for Fml being non empty set
for B being Subset of Fml
for R being Rule of Fml
for P being b₂,b₃ -correct Formula-sequence holds P is Formula-sequence of Fml

proof end;

theorem Th57: :: PROOFS_1:17

for Fml being non empty set
for B being Subset of Fml
for R being Rule of Fml
for a being object st B,R |- a holds
a in Fml

proof end;

definition

attr c₁ is strict ;
struct ProofSystem -> 1-sorted ;
aggr ProofSystem(# carrier, Axioms, Rules #) -> ProofSystem ;
sel Axioms c₁ -> Subset of the carrier of c₁;
sel Rules c₁ -> Rule of the carrier of c₁;

end;

definition

let P be ProofSystem ;
mode Formula-finset of P is Formula-finset of the carrier of P;

end;

definition

let P be ProofSystem ;
let a be object ;

pred P |- a means :: PROOFS_1:def 17
the Axioms of P, the Rules of P |- a;

end;

:: deftheorem defines |- PROOFS_1:def 17 :
for P being ProofSystem
for a being object holds
( P |- a iff the Axioms of P, the Rules of P |- a );

registration

cluster non empty for ProofSystem ;

existence
not for b₁ being ProofSystem holds b₁ is empty

proof end;

end;

theorem :: PROOFS_1:18

for P being non empty ProofSystem
for a being object st P |- a holds
a is Element of P by Th57;

definition

let P be non empty ProofSystem ;
let B be Subset of P;

pred P |- B means :: PROOFS_1:def 18
for a being object st a in B holds
P |- a;

end;

:: deftheorem defines |- PROOFS_1:def 18 :
for P being non empty ProofSystem
for B being Subset of P holds
( P |- B iff for a being object st a in B holds
P |- a );

definition

let P be non empty ProofSystem ;
let B1, B2 be Subset of P;
:: original: \/
redefine func B1 \/ B2 -> Subset of P;
coherence
B1 \/ B2 is Subset of P by XBOOLE_1:8;

end;

definition

let P be non empty ProofSystem ;

attr P is consistent means :: PROOFS_1:def 19
ex a being object st
( a in P & not P |- a );

end;

:: deftheorem defines consistent PROOFS_1:def 19 :
for P being non empty ProofSystem holds
( P is consistent iff ex a being object st
( a in P & not P |- a ) );

definition

let P be non empty ProofSystem ;
let B be Subset of P;

func P \/ B -> non empty ProofSystem equals :: PROOFS_1:def 20
ProofSystem(# the carrier of P,( the Axioms of P \/ B), the Rules of P #);

coherence
ProofSystem(# the carrier of P,( the Axioms of P \/ B), the Rules of P #) is non empty ProofSystem ;

end;

:: deftheorem defines \/ PROOFS_1:def 20 :
for P being non empty ProofSystem
for B being Subset of P holds P \/ B = ProofSystem(# the carrier of P,( the Axioms of P \/ B), the Rules of P #);

registration

cluster non empty strict consistent for ProofSystem ;

existence
ex b₁ being non empty ProofSystem st
( b₁ is consistent & b₁ is strict )

proof end;

end;

registration

let P be strict ProofSystem ;
let E be empty Subset of P;

reduce P \/ E to P;

reducibility
P \/ E = P ;

end;

notation

let P be non empty ProofSystem ;
antonym inconsistent P for consistent ;

end;

definition

let P be non empty ProofSystem ;
let B be Subset of P;

attr B is consistent means :: PROOFS_1:def 21
P \/ B is consistent ;

end;

:: deftheorem defines consistent PROOFS_1:def 21 :
for P being non empty ProofSystem
for B being Subset of P holds
( B is consistent iff P \/ B is consistent );

registration

let P be non empty consistent ProofSystem ;

cluster consistent for Element of bool the carrier of P;

existence
ex b₁ being Subset of P st b₁ is consistent

proof end;

end;

notation

let P be non empty ProofSystem ;
let B be Subset of P;
antonym inconsistent B for consistent ;

end;

registration

let P be non empty ProofSystem ;

cluster inconsistent for Element of bool the carrier of P;

existence
ex b₁ being Subset of P st b₁ is inconsistent

proof end;

end;

definition

let P be non empty ProofSystem ;

attr P is paraconsistent means :: PROOFS_1:def 22
for S being finite Subset of P holds S is consistent ;

end;

:: deftheorem defines paraconsistent PROOFS_1:def 22 :
for P being non empty ProofSystem holds
( P is paraconsistent iff for S being finite Subset of P holds S is consistent );

registration

cluster non empty paraconsistent -> non empty consistent for ProofSystem ;

coherence
for b₁ being non empty ProofSystem st b₁ is paraconsistent holds
b₁ is consistent

proof end;

cluster non empty consistent non paraconsistent for ProofSystem ;

existence
ex b₁ being non empty ProofSystem st
( b₁ is consistent & not b₁ is paraconsistent )

proof end;

end;

:: Consistency, contradictions, Lindenbaum

definition

let P be non empty ProofSystem ;
let B, B1 be Subset of P;

attr B1 is B -omitting means :: PROOFS_1:def 23
ex a being object st
( a in B & not P \/ B1 |- a );

end;

:: deftheorem defines -omitting PROOFS_1:def 23 :
for P being non empty ProofSystem
for B, B1 being Subset of P holds
( B1 is B -omitting iff ex a being object st
( a in B & not P \/ B1 |- a ) );

theorem Th56: :: PROOFS_1:19

for P being non empty ProofSystem
for B, B1 being Subset of P st B is inconsistent holds
( B1 is consistent iff B1 is B -omitting )

proof end;

registration

let P be non empty ProofSystem ;
let B be inconsistent Subset of P;

cluster B -omitting -> consistent for Element of bool the carrier of P;

coherence
for b₁ being Subset of P st b₁ is B -omitting holds
b₁ is consistent by Th56;

cluster non B -omitting -> inconsistent for Element of bool the carrier of P;

coherence
for b₁ being Subset of P st not b₁ is B -omitting holds
b₁ is inconsistent by Th56;

end;

registration

let P be non empty ProofSystem ;
let B be Subset of P;

cluster non B -omitting for Element of bool the carrier of P;

existence
not for b₁ being Subset of P holds b₁ is B -omitting

proof end;

end;

theorem Th59: :: PROOFS_1:20

for P being non empty ProofSystem
for B, B1, B2 being Subset of P st B1 is B -omitting & B2 c= B1 holds
B2 is B -omitting

proof end;

definition

let P be non empty ProofSystem ;
let B be Subset of P;

func Omit (P,B) -> Subset-Family of P equals :: PROOFS_1:def 24
{ B1 where B1 is Subset of P : B1 is B -omitting } ;

coherence
{ B1 where B1 is Subset of P : B1 is B -omitting } is Subset-Family of P

proof end;

end;

:: deftheorem defines Omit PROOFS_1:def 24 :
for P being non empty ProofSystem
for B being Subset of P holds Omit (P,B) = { B1 where B1 is Subset of P : B1 is B -omitting } ;

definition

let P be non empty ProofSystem ;
let B be Subset of P;

redefine func Omit (P,B) means :Def17: :: PROOFS_1:def 25
for B1 being Subset of P holds
( B1 in it iff B1 is B -omitting );

compatibility
for b₁ being Subset-Family of P holds
( b₁ = Omit (P,B) iff for B1 being Subset of P holds
( B1 in b₁ iff B1 is B -omitting ) )

proof end;

end;

:: deftheorem Def17 defines Omit PROOFS_1:def 25 :
for P being non empty ProofSystem
for B being Subset of P
for b₃ being Subset-Family of P holds
( b₃ = Omit (P,B) iff for B1 being Subset of P holds
( B1 in b₃ iff B1 is B -omitting ) );

definition

let P be non empty ProofSystem ;
let B, B1 be Subset of P;

attr B1 is B -maximally-omitting means :: PROOFS_1:def 26
( B1 is B -omitting & ( for B2 being Subset of P st B1 c< B2 holds
not B2 is B -omitting ) );

end;

:: deftheorem defines -maximally-omitting PROOFS_1:def 26 :
for P being non empty ProofSystem
for B, B1 being Subset of P holds
( B1 is B -maximally-omitting iff ( B1 is B -omitting & ( for B2 being Subset of P st B1 c< B2 holds
not B2 is B -omitting ) ) );

registration

let P be non empty ProofSystem ;
let B be Subset of P;

cluster B -maximally-omitting -> B -omitting for Element of bool the carrier of P;

coherence
for b₁ being Subset of P st b₁ is B -maximally-omitting holds
b₁ is B -omitting ;

end;

definition

let X be set ;

attr X is finite-character means :Def20: :: PROOFS_1:def 27
for a being object holds
( a in X iff ex B being set st
( B = a & ( for S being finite Subset of B holds S in X ) ) );

end;

:: deftheorem Def20 defines finite-character PROOFS_1:def 27 :
for X being set holds
( X is finite-character iff for a being object holds
( a in X iff ex B being set st
( B = a & ( for S being finite Subset of B holds S in X ) ) ) );

definition

let X be set ;

redefine attr X is finite-character means :Def20r: :: PROOFS_1:def 28
for Y being set holds
( Y in X iff for S being finite Subset of Y holds S in X );

compatibility
( X is finite-character iff for Y being set holds
( Y in X iff for S being finite Subset of Y holds S in X ) )

proof end;

end;

:: deftheorem Def20r defines finite-character PROOFS_1:def 28 :
for X being set holds
( X is finite-character iff for Y being set holds
( Y in X iff for S being finite Subset of Y holds S in X ) );

definition

let X be set ;
let F be Subset-Family of X;

:: original: finite-character
redefine attr F is finite-character means :: PROOFS_1:def 29
for B being Subset of X holds
( B in F iff for S being finite Subset of B holds S in F );

compatibility
( F is finite-character iff for B being Subset of X holds
( B in F iff for S being finite Subset of B holds S in F ) )

proof end;

end;

:: deftheorem defines finite-character PROOFS_1:def 29 :
for X being set
for F being Subset-Family of X holds
( F is finite-character iff for B being Subset of X holds
( B in F iff for S being finite Subset of B holds S in F ) );

registration

let X be set ;

cluster non empty () for Element of bool (bool X);

existence
ex b₁ being Subset-Family of X st
( not b₁ is empty & b₁ is () )

proof end;

end;

registration

cluster empty -> finite-character for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is finite-character ;

cluster non empty finite-character for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is finite-character )

proof end;

end;

Lm58: for X being non empty finite-character set holds {} in X

proof end;

Lm59: for X being non empty finite-character set
for C being c=-linear Subset of X holds union C in X

proof end;

theorem Th60: :: PROOFS_1:21

for X being non empty finite-character set ex Y being Element of X st
for Z being Element of X holds not Y c< Z

proof end;

registration

let P be non empty ProofSystem ;
let F be finite Subset of P;

cluster Omit (P,F) -> () ;

coherence
Omit (P,F) is finite-character

proof end;

end;

theorem Th61: :: PROOFS_1:22

for P being non empty ProofSystem
for B being Subset of P
for F being finite Subset of P st B is F -omitting holds
ex B1 being Subset of P st
( B c= B1 & B1 is F -maximally-omitting )

proof end;

definition

let P be non empty ProofSystem ;
let B be Subset of P;

attr B is maximally-consistent means :: PROOFS_1:def 30
( B is consistent & ( for B1 being Subset of P st B c< B1 holds
B1 is inconsistent ) );

end;

:: deftheorem defines maximally-consistent PROOFS_1:def 30 :
for P being non empty ProofSystem
for B being Subset of P holds
( B is maximally-consistent iff ( B is consistent & ( for B1 being Subset of P st B c< B1 holds
B1 is inconsistent ) ) );

theorem :: PROOFS_1:23

for P being non empty ProofSystem
for B being Subset of P st P is consistent & not P is paraconsistent & B is consistent holds
ex B1 being Subset of P st
( B c= B1 & B1 is maximally-consistent )

proof end;

scheme :: PROOFS_1:sch 1
UnOpCongr{ F₁() -> non empty set , F₂( Element of F₁()) -> Element of F₁(), F₃() -> Equivalence_Relation of F₁() } :

ex f being UnOp of (Class F₃()) st
for x being Element of F₁() holds f . (Class (F₃(),x)) = Class (F₃(),F₂(x))

provided

A1: for x, y being Element of F₁() st [x,y] in F₃() holds
[F₂(x),F₂(y)] in F₃()

proof end;

scheme :: PROOFS_1:sch 2
BinOpCongr{ F₁() -> non empty set , F₂( Element of F₁(), Element of F₁()) -> Element of F₁(), F₃() -> Equivalence_Relation of F₁() } :

ex f being BinOp of (Class F₃()) st
for x, y being Element of F₁() holds f . ((Class (F₃(),x)),(Class (F₃(),y))) = Class (F₃(),F₂(x,y))

provided

A1: for x1, x2, y1, y2 being Element of F₁() st [x1,x2] in F₃() & [y1,y2] in F₃() holds
[F₂(x1,y1),F₂(x2,y2)] in F₃()

proof end;

scheme :: PROOFS_1:sch 3
ProofInduction{ F₁() -> set , F₂() -> Rule, P₁[ object ] } :

for a being object st F₁(),F₂() |- a holds
P₁[a]

provided

A1: for a being object st a in F₁() holds
P₁[a] and
A2: for X being set
for a being object st [X,a] in F₂() & ( for b being object st b in X holds
P₁[b] ) holds
P₁[a]

proof end;

definition

let R be Rule;
let X be set ;

attr X is R -closed means :Def28: :: PROOFS_1:def 31
for Y being set
for a being object st [Y,a] in R & Y c= X holds
a in X;

end;

:: deftheorem Def28 defines -closed PROOFS_1:def 31 :
for R being Rule
for X being set holds
( X is R -closed iff for Y being set
for a being object st [Y,a] in R & Y c= X holds
a in X );

definition

let D be non empty set ;
let R be Rule;

mode Theorem of D,R -> Formula means :: PROOFS_1:def 32
D,R |- it;

existence
ex b₁ being Formula st D,R |- b₁

proof end;

sethood
ex b₁ being set st
for b₂ being Formula st D,R |- b₂ holds
b₂ in b₁

proof end;

end;

:: deftheorem defines Theorem PROOFS_1:def 32 :
for D being non empty set
for R being Rule
for b₃ being Formula holds
( b₃ is Theorem of D,R iff D,R |- b₃ );

definition

let X be set ;
let R be Rule;

func Theorems (X,R) -> set equals :: PROOFS_1:def 33
{ t where t is Element of X \/ (rng R) : X,R |- t } ;

coherence
{ t where t is Element of X \/ (rng R) : X,R |- t } is set ;

end;

:: deftheorem defines Theorems PROOFS_1:def 33 :
for X being set
for R being Rule holds Theorems (X,R) = { t where t is Element of X \/ (rng R) : X,R |- t } ;

definition

let X be set ;
let R be Rule;

redefine func Theorems (X,R) means :Def30r: :: PROOFS_1:def 34
for a being object holds
( a in it iff X,R |- a );

compatibility
for b₁ being set holds
( b₁ = Theorems (X,R) iff for a being object holds
( a in b₁ iff X,R |- a ) )

proof end;

end;

:: deftheorem Def30r defines Theorems PROOFS_1:def 34 :
for X being set
for R being Rule
for b₃ being set holds
( b₃ = Theorems (X,R) iff for a being object holds
( a in b₃ iff X,R |- a ) );

registration

let X be set ;
let R be Rule;

cluster Theorems (X,R) -> X -extending R -closed ;

coherence
( Theorems (X,R) is X -extending & Theorems (X,R) is R -closed )

proof end;

cluster X -extending R -closed for set ;

existence
ex b₁ being set st
( b₁ is X -extending & b₁ is R -closed )

proof end;

end;

theorem Th65: :: PROOFS_1:24

for X being set
for R being Rule
for a being object holds
( X,R |- a iff for Y being b₁ -extending b₂ -closed set holds a in Y )

proof end;

definition

let P be non empty ProofSystem ;

func Theorems P -> Subset of P equals :: PROOFS_1:def 35
Theorems ( the Axioms of P, the Rules of P);

coherence
Theorems ( the Axioms of P, the Rules of P) is Subset of P

proof end;

let X be set ;

attr X is P -closed means :: PROOFS_1:def 36
( X is the Rules of P -closed & X is the Axioms of P -extending );

end;

:: deftheorem defines Theorems PROOFS_1:def 35 :
for P being non empty ProofSystem holds Theorems P = Theorems ( the Axioms of P, the Rules of P);

:: deftheorem defines -closed PROOFS_1:def 36 :
for P being non empty ProofSystem
for X being set holds
( X is P -closed iff ( X is the Rules of P -closed & X is the Axioms of P -extending ) );

registration

let P be non empty ProofSystem ;

cluster Theorems P -> P -closed ;

coherence
Theorems P is P -closed ;

cluster P -closed -> the Axioms of P -extending the Rules of P -closed for set ;

coherence
for b₁ being set st b₁ is P -closed holds
( b₁ is the Rules of P -closed & b₁ is the Axioms of P -extending ) ;

cluster the Axioms of P -extending the Rules of P -closed -> P -closed for set ;

coherence
for b₁ being set st b₁ is the Rules of P -closed & b₁ is the Axioms of P -extending holds
b₁ is P -closed ;

cluster P -closed for Element of bool the carrier of P;

existence
ex b₁ being Subset of P st b₁ is P -closed

proof end;

cluster P -closed for set ;

existence
ex b₁ being set st b₁ is P -closed

proof end;

end;

theorem :: PROOFS_1:25

for P being non empty ProofSystem
for a being object holds
( P |- a iff for X being b₁ -closed set holds a in X )

proof end;