:: ZF_LANG semantic presentation

definition

func VAR -> Subset of NAT equals :: ZF_LANG:def 1
{ k where k is Nat : 5 <= k } ;
coherence

proof end;

end;

:: deftheorem defines VAR ZF_LANG:def 1 :

registration

cluster VAR -> non empty ;
coherence

proof end;

end;

definition

mode Variable is Element of VAR ;

end;

definition

let n be Nat;
func x. n -> Variable equals :: ZF_LANG:def 2
5 + n;
coherence

proof end;

end;

:: deftheorem defines x. ZF_LANG:def 2 :

definition

let x be Variable;
:: original: <*
redefine func <*x*> -> FinSequence of NAT ;
coherence

proof end;

end;

definition

let x, y be Variable;
func x '=' y -> FinSequence of NAT equals :: ZF_LANG:def 3
(<*0*> ^ <*x*>) ^ <*y*>;
coherence ;
func x 'in' y -> FinSequence of NAT equals :: ZF_LANG:def 4
(<*1*> ^ <*x*>) ^ <*y*>;
coherence ;

end;

:: deftheorem defines '=' ZF_LANG:def 3 :

:: deftheorem defines 'in' ZF_LANG:def 4 :

theorem :: ZF_LANG:1

canceled;

theorem :: ZF_LANG:2

canceled;

theorem :: ZF_LANG:3

canceled;

theorem :: ZF_LANG:4

canceled;

theorem :: ZF_LANG:5

canceled;

theorem :: ZF_LANG:6

for x, y, z, t being Variable st x '=' y = z '=' t holds
( x = z & y = t )

proof end;

theorem :: ZF_LANG:7

for x, y, z, t being Variable st x 'in' y = z 'in' t holds
( x = z & y = t )

proof end;

definition

let p be FinSequence of NAT ;
func 'not' p -> FinSequence of NAT equals :: ZF_LANG:def 5
<*2*> ^ p;
coherence ;
let q be FinSequence of NAT ;
func p '&' q -> FinSequence of NAT equals :: ZF_LANG:def 6
(<*3*> ^ p) ^ q;
coherence ;

end;

:: deftheorem defines 'not' ZF_LANG:def 5 :

:: deftheorem defines '&' ZF_LANG:def 6 :

theorem :: ZF_LANG:8

canceled;

theorem :: ZF_LANG:9

canceled;

theorem Th10: :: ZF_LANG:10

for p, q being FinSequence of NAT st 'not' p = 'not' q holds
p = q by FINSEQ_1:46;

definition

let x be Variable;
let p be FinSequence of NAT ;
func All x,p -> FinSequence of NAT equals :: ZF_LANG:def 7
(<*4*> ^ <*x*>) ^ p;
coherence ;

end;

:: deftheorem defines All ZF_LANG:def 7 :

theorem :: ZF_LANG:11

canceled;

theorem Th12: :: ZF_LANG:12

for p, q being FinSequence of NAT
for x, y being Variable st All x,p = All y,q holds
( x = y & p = q )

proof end;

definition

func WFF -> non empty set means :Def8: :: ZF_LANG:def 8
( ( for a being set st a in it holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in it & x 'in' y in it ) ) & ( for p being FinSequence of NAT st p in it holds
'not' p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds
p '&' q in it ) & ( for x being Variable
for p being FinSequence of NAT st p in it holds
All x,p in it ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All x,p in D ) holds
it c= D ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines WFF ZF_LANG:def 8 :

definition

let IT be FinSequence of NAT ;
attr IT is ZF-formula-like means :Def9: :: ZF_LANG:def 9
IT is Element of WFF ;

end;

:: deftheorem Def9 defines ZF-formula-like ZF_LANG:def 9 :

registration

cluster ZF-formula-like FinSequence of NAT ;
existence

proof end;

end;

definition

mode ZF-formula is ZF-formula-like FinSequence of NAT ;

end;

theorem :: ZF_LANG:13

canceled;

theorem :: ZF_LANG:14

for a being set holds
( a is ZF-formula iff a in WFF )

proof end;

registration

let x, y be Variable;
cluster x '=' y -> ZF-formula-like ;
coherence

proof end;

cluster x 'in' y -> ZF-formula-like ;
coherence

proof end;

end;

registration

let H be ZF-formula;
cluster 'not' H -> ZF-formula-like ;
coherence

proof end;

let G be ZF-formula;
cluster H '&' G -> ZF-formula-like ;
coherence

proof end;

end;

registration

let x be Variable;
let H be ZF-formula;
cluster All x,H -> ZF-formula-like ;
coherence

proof end;

end;

definition

let H be ZF-formula;
attr H is being_equality means :Def10: :: ZF_LANG:def 10
ex x, y being Variable st H = x '=' y;
attr H is being_membership means :Def11: :: ZF_LANG:def 11
ex x, y being Variable st H = x 'in' y;
attr H is negative means :Def12: :: ZF_LANG:def 12
ex H1 being ZF-formula st H = 'not' H1;
attr H is conjunctive means :Def13: :: ZF_LANG:def 13
ex F, G being ZF-formula st H = F '&' G;
attr H is universal means :Def14: :: ZF_LANG:def 14
ex x being Variable ex H1 being ZF-formula st H = All x,H1;

end;

:: deftheorem Def10 defines being_equality ZF_LANG:def 10 :

:: deftheorem Def11 defines being_membership ZF_LANG:def 11 :

:: deftheorem Def12 defines negative ZF_LANG:def 12 :

:: deftheorem Def13 defines conjunctive ZF_LANG:def 13 :

:: deftheorem Def14 defines universal ZF_LANG:def 14 :

notation

let H be ZF-formula;
synonym H is_equality for being_equality H;
synonym H is_membership for being_membership H;

end;

theorem :: ZF_LANG:15

canceled;

theorem :: ZF_LANG:16

for H being ZF-formula holds
( ( H is_equality implies ex x, y being Variable st H = x '=' y ) & ( ex x, y being Variable st H = x '=' y implies H is_equality ) & ( H is_membership implies ex x, y being Variable st H = x 'in' y ) & ( ex x, y being Variable st H = x 'in' y implies H is_membership ) & ( H is negative implies ex H1 being ZF-formula st H = 'not' H1 ) & ( ex H1 being ZF-formula st H = 'not' H1 implies H is negative ) & ( H is conjunctive implies ex F, G being ZF-formula st H = F '&' G ) & ( ex F, G being ZF-formula st H = F '&' G implies H is conjunctive ) & ( H is universal implies ex x being Variable ex H1 being ZF-formula st H = All x,H1 ) & ( ex x being Variable ex H1 being ZF-formula st H = All x,H1 implies H is universal ) ) by Def10, Def11, Def12, Def13, Def14;

definition

let H be ZF-formula;
attr H is atomic means :Def15: :: ZF_LANG:def 15
( H is_equality or H is_membership );

end;

:: deftheorem Def15 defines atomic ZF_LANG:def 15 :

definition

let F, G be ZF-formula;
func F 'or' G -> ZF-formula equals :: ZF_LANG:def 16
'not' (('not' F) '&' ('not' G));
coherence ;
func F => G -> ZF-formula equals :: ZF_LANG:def 17
'not' (F '&' ('not' G));
coherence ;

end;

:: deftheorem defines 'or' ZF_LANG:def 16 :

:: deftheorem defines => ZF_LANG:def 17 :

definition

let F, G be ZF-formula;
func F <=> G -> ZF-formula equals :: ZF_LANG:def 18
(F => G) '&' (G => F);
coherence ;

end;

:: deftheorem defines <=> ZF_LANG:def 18 :

definition

let x be Variable;
let H be ZF-formula;
func Ex x,H -> ZF-formula equals :: ZF_LANG:def 19
'not' (All x,('not' H));
coherence ;

end;

:: deftheorem defines Ex ZF_LANG:def 19 :

definition

let H be ZF-formula;
attr H is disjunctive means :Def20: :: ZF_LANG:def 20
ex F, G being ZF-formula st H = F 'or' G;
attr H is conditional means :Def21: :: ZF_LANG:def 21
ex F, G being ZF-formula st H = F => G;
attr H is biconditional means :Def22: :: ZF_LANG:def 22
ex F, G being ZF-formula st H = F <=> G;
attr H is existential means :Def23: :: ZF_LANG:def 23
ex x being Variable ex H1 being ZF-formula st H = Ex x,H1;

end;

:: deftheorem Def20 defines disjunctive ZF_LANG:def 20 :

:: deftheorem Def21 defines conditional ZF_LANG:def 21 :

:: deftheorem Def22 defines biconditional ZF_LANG:def 22 :

:: deftheorem Def23 defines existential ZF_LANG:def 23 :

theorem :: ZF_LANG:17

canceled;

theorem :: ZF_LANG:18

canceled;

theorem :: ZF_LANG:19

canceled;

theorem :: ZF_LANG:20

canceled;

theorem :: ZF_LANG:21

canceled;

theorem :: ZF_LANG:22

for H being ZF-formula holds
( ( H is disjunctive implies ex F, G being ZF-formula st H = F 'or' G ) & ( ex F, G being ZF-formula st H = F 'or' G implies H is disjunctive ) & ( H is conditional implies ex F, G being ZF-formula st H = F => G ) & ( ex F, G being ZF-formula st H = F => G implies H is conditional ) & ( H is biconditional implies ex F, G being ZF-formula st H = F <=> G ) & ( ex F, G being ZF-formula st H = F <=> G implies H is biconditional ) & ( H is existential implies ex x being Variable ex H1 being ZF-formula st H = Ex x,H1 ) & ( ex x being Variable ex H1 being ZF-formula st H = Ex x,H1 implies H is existential ) ) by Def20, Def21, Def22, Def23;

definition

let x, y be Variable;
let H be ZF-formula;
func All x,y,H -> ZF-formula equals :: ZF_LANG:def 24
All x,(All y,H);
coherence ;
func Ex x,y,H -> ZF-formula equals :: ZF_LANG:def 25
Ex x,(Ex y,H);
coherence ;

end;

:: deftheorem defines All ZF_LANG:def 24 :

:: deftheorem defines Ex ZF_LANG:def 25 :

theorem :: ZF_LANG:23

for x, y being Variable
for H being ZF-formula holds
( All x,y,H = All x,(All y,H) & Ex x,y,H = Ex x,(Ex y,H) ) ;

definition

let x, y, z be Variable;
let H be ZF-formula;
func All x,y,z,H -> ZF-formula equals :: ZF_LANG:def 26
All x,(All y,z,H);
coherence ;
func Ex x,y,z,H -> ZF-formula equals :: ZF_LANG:def 27
Ex x,(Ex y,z,H);
coherence ;

end;

:: deftheorem defines All ZF_LANG:def 26 :

:: deftheorem defines Ex ZF_LANG:def 27 :

theorem :: ZF_LANG:24

for x, y, z being Variable
for H being ZF-formula holds
( All x,y,z,H = All x,(All y,z,H) & Ex x,y,z,H = Ex x,(Ex y,z,H) ) ;

theorem Th25: :: ZF_LANG:25

for H being ZF-formula holds
( H is_equality or H is_membership or H is negative or H is conjunctive or H is universal )

proof end;

theorem Th26: :: ZF_LANG:26

for H being ZF-formula holds
( H is atomic or H is negative or H is conjunctive or H is universal )

proof end;

theorem Th27: :: ZF_LANG:27

for H being ZF-formula st H is atomic holds
len H = 3

proof end;

theorem Th28: :: ZF_LANG:28

for H being ZF-formula holds
( H is atomic or ex H1 being ZF-formula st (len H1) + 1 <= len H )

proof end;

theorem Th29: :: ZF_LANG:29

for H being ZF-formula holds 3 <= len H

proof end;

theorem :: ZF_LANG:30

for H being ZF-formula st len H = 3 holds
H is atomic

proof end;

theorem Th31: :: ZF_LANG:31

for x, y being Variable holds
( (x '=' y) . 1 = 0 & (x 'in' y) . 1 = 1 )

proof end;

theorem Th32: :: ZF_LANG:32

for H being ZF-formula holds ('not' H) . 1 = 2 by FINSEQ_1:58;

theorem Th33: :: ZF_LANG:33

for F, G being ZF-formula holds (F '&' G) . 1 = 3

proof end;

theorem Th34: :: ZF_LANG:34

for x being Variable
for H being ZF-formula holds (All x,H) . 1 = 4

proof end;

theorem Th35: :: ZF_LANG:35

for H being ZF-formula st H is_equality holds
H . 1 = 0

proof end;

theorem Th36: :: ZF_LANG:36

for H being ZF-formula st H is_membership holds
H . 1 = 1

proof end;

theorem Th37: :: ZF_LANG:37

for H being ZF-formula st H is negative holds
H . 1 = 2

proof end;

theorem Th38: :: ZF_LANG:38

for H being ZF-formula st H is conjunctive holds
H . 1 = 3

proof end;

theorem Th39: :: ZF_LANG:39

for H being ZF-formula st H is universal holds
H . 1 = 4

proof end;

theorem Th40: :: ZF_LANG:40

for H being ZF-formula holds
( ( H is_equality & H . 1 = 0 ) or ( H is_membership & H . 1 = 1 ) or ( H is negative & H . 1 = 2 ) or ( H is conjunctive & H . 1 = 3 ) or ( H is universal & H . 1 = 4 ) )

proof end;

theorem :: ZF_LANG:41

for H being ZF-formula st H . 1 = 0 holds
H is_equality by Th40;

theorem :: ZF_LANG:42

for H being ZF-formula st H . 1 = 1 holds
H is_membership by Th40;

theorem :: ZF_LANG:43

for H being ZF-formula st H . 1 = 2 holds
H is negative by Th40;

theorem :: ZF_LANG:44

for H being ZF-formula st H . 1 = 3 holds
H is conjunctive by Th40;

theorem :: ZF_LANG:45

for H being ZF-formula st H . 1 = 4 holds
H is universal by Th40;

theorem Th46: :: ZF_LANG:46

for H, F being ZF-formula
for sq being FinSequence st H = F ^ sq holds
H = F

proof end;

theorem Th47: :: ZF_LANG:47

for H, G, H1, G1 being ZF-formula st H '&' G = H1 '&' G1 holds
( H = H1 & G = G1 )

proof end;

theorem Th48: :: ZF_LANG:48

for F, G, F1, G1 being ZF-formula st F 'or' G = F1 'or' G1 holds
( F = F1 & G = G1 )

proof end;

theorem Th49: :: ZF_LANG:49

for F, G, F1, G1 being ZF-formula st F => G = F1 => G1 holds
( F = F1 & G = G1 )

proof end;

theorem Th50: :: ZF_LANG:50

for F, G, F1, G1 being ZF-formula st F <=> G = F1 <=> G1 holds
( F = F1 & G = G1 )

proof end;

theorem Th51: :: ZF_LANG:51

for x, y being Variable
for H, G being ZF-formula st Ex x,H = Ex y,G holds
( x = y & H = G )

proof end;

definition

let H be ZF-formula;
assume A1: H is atomic ;
func Var1 H -> Variable equals :Def28: :: ZF_LANG:def 28
H . 2;
coherence

proof end;

func Var2 H -> Variable equals :Def29: :: ZF_LANG:def 29
H . 3;
coherence

proof end;

end;

:: deftheorem Def28 defines Var1 ZF_LANG:def 28 :

:: deftheorem Def29 defines Var2 ZF_LANG:def 29 :

theorem :: ZF_LANG:52

for H being ZF-formula st H is atomic holds
( Var1 H = H . 2 & Var2 H = H . 3 ) by Def28, Def29;

theorem Th53: :: ZF_LANG:53

for H being ZF-formula st H is_equality holds
H = (Var1 H) '=' (Var2 H)

proof end;

theorem Th54: :: ZF_LANG:54

for H being ZF-formula st H is_membership holds
H = (Var1 H) 'in' (Var2 H)

proof end;

definition

let H be ZF-formula;
assume A1: H is negative ;
func the_argument_of H -> ZF-formula means :Def30: :: ZF_LANG:def 30
'not' it = H;
existence by A1, Def12;
uniqueness by Th10;

end;

:: deftheorem Def30 defines the_argument_of ZF_LANG:def 30 :

definition

let H be ZF-formula;
assume A1: ( H is conjunctive or H is disjunctive ) ;
func the_left_argument_of H -> ZF-formula means :Def31: :: ZF_LANG:def 31
ex H1 being ZF-formula st it '&' H1 = H if H is conjunctive
otherwise ex H1 being ZF-formula st it 'or' H1 = H;
existence by A1, Def13, Def20;
uniqueness by Th47, Th48;
consistency ;
func the_right_argument_of H -> ZF-formula means :Def32: :: ZF_LANG:def 32
ex H1 being ZF-formula st H1 '&' it = H if H is conjunctive
otherwise ex H1 being ZF-formula st H1 'or' it = H;
existence

proof end;

uniqueness by Th47, Th48;
consistency ;

end;

:: deftheorem Def31 defines the_left_argument_of ZF_LANG:def 31 :

:: deftheorem Def32 defines the_right_argument_of ZF_LANG:def 32 :

theorem :: ZF_LANG:55

canceled;

theorem :: ZF_LANG:56

for H, F being ZF-formula st H is conjunctive holds
( ( F = the_left_argument_of H implies ex G being ZF-formula st F '&' G = H ) & ( ex G being ZF-formula st F '&' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G '&' F = H ) & ( ex G being ZF-formula st G '&' F = H implies F = the_right_argument_of H ) ) by Def31, Def32;

theorem Th57: :: ZF_LANG:57

for H, F being ZF-formula st H is disjunctive holds
( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) )

proof end;

theorem Th58: :: ZF_LANG:58

for H being ZF-formula st H is conjunctive holds
H = (the_left_argument_of H) '&' (the_right_argument_of H)

proof end;

theorem :: ZF_LANG:59

for H being ZF-formula st H is disjunctive holds
H = (the_left_argument_of H) 'or' (the_right_argument_of H)

proof end;

definition

let H be ZF-formula;
assume A1: ( H is universal or H is existential ) ;
func bound_in H -> Variable means :Def33: :: ZF_LANG:def 33
ex H1 being ZF-formula st All it,H1 = H if H is universal
otherwise ex H1 being ZF-formula st Ex it,H1 = H;
existence by A1, Def14, Def23;
uniqueness by Th12, Th51;
consistency ;
func the_scope_of H -> ZF-formula means :Def34: :: ZF_LANG:def 34
ex x being Variable st All x,it = H if H is universal
otherwise ex x being Variable st Ex x,it = H;
existence

proof end;

uniqueness by Th12, Th51;
consistency ;

end;

:: deftheorem Def33 defines bound_in ZF_LANG:def 33 :

:: deftheorem Def34 defines the_scope_of ZF_LANG:def 34 :

theorem :: ZF_LANG:60

for x being Variable
for H, H1 being ZF-formula st H is universal holds
( ( x = bound_in H implies ex H1 being ZF-formula st All x,H1 = H ) & ( ex H1 being ZF-formula st All x,H1 = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st All x,H1 = H ) & ( ex x being Variable st All x,H1 = H implies H1 = the_scope_of H ) ) by Def33, Def34;

theorem Th61: :: ZF_LANG:61

for x being Variable
for H, H1 being ZF-formula st H is existential holds
( ( x = bound_in H implies ex H1 being ZF-formula st Ex x,H1 = H ) & ( ex H1 being ZF-formula st Ex x,H1 = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex x,H1 = H ) & ( ex x being Variable st Ex x,H1 = H implies H1 = the_scope_of H ) )

proof end;

theorem Th62: :: ZF_LANG:62

for H being ZF-formula st H is universal holds
H = All (bound_in H),(the_scope_of H)

proof end;

theorem :: ZF_LANG:63

for H being ZF-formula st H is existential holds
H = Ex (bound_in H),(the_scope_of H)

proof end;

definition

let H be ZF-formula;
assume A1: H is conditional ;
func the_antecedent_of H -> ZF-formula means :Def35: :: ZF_LANG:def 35
ex H1 being ZF-formula st H = it => H1;
existence by A1, Def21;
uniqueness by Th49;
func the_consequent_of H -> ZF-formula means :Def36: :: ZF_LANG:def 36
ex H1 being ZF-formula st H = H1 => it;
existence

proof end;

uniqueness by Th49;

end;

:: deftheorem Def35 defines the_antecedent_of ZF_LANG:def 35 :

:: deftheorem Def36 defines the_consequent_of ZF_LANG:def 36 :

theorem :: ZF_LANG:64

for H, F being ZF-formula st H is conditional holds
( ( F = the_antecedent_of H implies ex G being ZF-formula st H = F => G ) & ( ex G being ZF-formula st H = F => G implies F = the_antecedent_of H ) & ( F = the_consequent_of H implies ex G being ZF-formula st H = G => F ) & ( ex G being ZF-formula st H = G => F implies F = the_consequent_of H ) ) by Def35, Def36;

theorem :: ZF_LANG:65

for H being ZF-formula st H is conditional holds
H = (the_antecedent_of H) => (the_consequent_of H)

proof end;

definition

let H be ZF-formula;
assume A1: H is biconditional ;
func the_left_side_of H -> ZF-formula means :Def37: :: ZF_LANG:def 37
ex H1 being ZF-formula st H = it <=> H1;
existence by A1, Def22;
uniqueness by Th50;
func the_right_side_of H -> ZF-formula means :Def38: :: ZF_LANG:def 38
ex H1 being ZF-formula st H = H1 <=> it;
existence

proof end;

uniqueness by Th50;

end;

:: deftheorem Def37 defines the_left_side_of ZF_LANG:def 37 :

:: deftheorem Def38 defines the_right_side_of ZF_LANG:def 38 :

theorem :: ZF_LANG:66

for H, F being ZF-formula st H is biconditional holds
( ( F = the_left_side_of H implies ex G being ZF-formula st H = F <=> G ) & ( ex G being ZF-formula st H = F <=> G implies F = the_left_side_of H ) & ( F = the_right_side_of H implies ex G being ZF-formula st H = G <=> F ) & ( ex G being ZF-formula st H = G <=> F implies F = the_right_side_of H ) ) by Def37, Def38;

theorem :: ZF_LANG:67

for H being ZF-formula st H is biconditional holds
H = (the_left_side_of H) <=> (the_right_side_of H)

proof end;

definition

let H, F be ZF-formula;
pred H is_immediate_constituent_of F means :Def39: :: ZF_LANG:def 39
( F = 'not' H or ex H1 being ZF-formula st
( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All x,H );

end;

:: deftheorem Def39 defines is_immediate_constituent_of ZF_LANG:def 39 :

theorem :: ZF_LANG:68

canceled;

theorem Th69: :: ZF_LANG:69

for x, y being Variable
for H being ZF-formula holds not H is_immediate_constituent_of x '=' y

proof end;

theorem Th70: :: ZF_LANG:70

for x, y being Variable
for H being ZF-formula holds not H is_immediate_constituent_of x 'in' y

proof end;

theorem Th71: :: ZF_LANG:71

for F, H being ZF-formula holds
( F is_immediate_constituent_of 'not' H iff F = H )

proof end;

theorem Th72: :: ZF_LANG:72

for F, G, H being ZF-formula holds
( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )

proof end;

theorem Th73: :: ZF_LANG:73

for x being Variable
for F, H being ZF-formula holds
( F is_immediate_constituent_of All x,H iff F = H )

proof end;

theorem :: ZF_LANG:74

for H, F being ZF-formula st H is atomic holds
not F is_immediate_constituent_of H

proof end;

theorem Th75: :: ZF_LANG:75

for H, F being ZF-formula st H is negative holds
( F is_immediate_constituent_of H iff F = the_argument_of H )

proof end;

theorem Th76: :: ZF_LANG:76

for H, F being ZF-formula st H is conjunctive holds
( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) )

proof end;

theorem Th77: :: ZF_LANG:77

for H, F being ZF-formula st H is universal holds
( F is_immediate_constituent_of H iff F = the_scope_of H )

proof end;

definition

let H, F be ZF-formula;
pred H is_subformula_of F means :Def40: :: ZF_LANG:def 40
ex n being Nat ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) );

end;

:: deftheorem Def40 defines is_subformula_of ZF_LANG:def 40 :

theorem :: ZF_LANG:78

canceled;

theorem Th79: :: ZF_LANG:79

for H being ZF-formula holds H is_subformula_of H

proof end;

definition

let H, F be ZF-formula;
pred H is_proper_subformula_of F means :Def41: :: ZF_LANG:def 41
( H is_subformula_of F & H <> F );

end;

:: deftheorem Def41 defines is_proper_subformula_of ZF_LANG:def 41 :

theorem :: ZF_LANG:80

canceled;

theorem Th81: :: ZF_LANG:81

for H, F being ZF-formula st H is_immediate_constituent_of F holds
len H < len F

proof end;

theorem Th82: :: ZF_LANG:82

for H, F being ZF-formula st H is_immediate_constituent_of F holds
H is_proper_subformula_of F

proof end;

theorem Th83: :: ZF_LANG:83

for H, F being ZF-formula st H is_proper_subformula_of F holds
len H < len F

proof end;

theorem Th84: :: ZF_LANG:84

for H, F being ZF-formula st H is_proper_subformula_of F holds
ex G being ZF-formula st G is_immediate_constituent_of F

proof end;

theorem Th85: :: ZF_LANG:85

for F, G, H being ZF-formula st F is_proper_subformula_of G & G is_proper_subformula_of H holds
F is_proper_subformula_of H

proof end;

theorem Th86: :: ZF_LANG:86

for F, G, H being ZF-formula st F is_subformula_of G & G is_subformula_of H holds
F is_subformula_of H

proof end;

theorem :: ZF_LANG:87

for G, H being ZF-formula st G is_subformula_of H & H is_subformula_of G holds
G = H

proof end;

theorem Th88: :: ZF_LANG:88

for x, y being Variable
for F being ZF-formula holds not F is_proper_subformula_of x '=' y

proof end;

theorem Th89: :: ZF_LANG:89

for x, y being Variable
for F being ZF-formula holds not F is_proper_subformula_of x 'in' y

proof end;

theorem Th90: :: ZF_LANG:90

for F, H being ZF-formula st F is_proper_subformula_of 'not' H holds
F is_subformula_of H

proof end;

theorem Th91: :: ZF_LANG:91

for F, G, H being ZF-formula holds
( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H )

proof end;

theorem Th92: :: ZF_LANG:92

for x being Variable
for F, H being ZF-formula st F is_proper_subformula_of All x,H holds
F is_subformula_of H

proof end;

theorem :: ZF_LANG:93

for H, F being ZF-formula st H is atomic holds
not F is_proper_subformula_of H

proof end;

theorem :: ZF_LANG:94

for H being ZF-formula st H is negative holds
the_argument_of H is_proper_subformula_of H

proof end;

theorem :: ZF_LANG:95

for H being ZF-formula st H is conjunctive holds
( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H )

proof end;

theorem :: ZF_LANG:96

for H being ZF-formula st H is universal holds
the_scope_of H is_proper_subformula_of H

proof end;

theorem Th97: :: ZF_LANG:97

for x, y being Variable
for H being ZF-formula holds
( H is_subformula_of x '=' y iff H = x '=' y )

proof end;

theorem Th98: :: ZF_LANG:98

for x, y being Variable
for H being ZF-formula holds
( H is_subformula_of x 'in' y iff H = x 'in' y )

proof end;

definition

let H be ZF-formula;
func Subformulae H -> set means :Def42: :: ZF_LANG:def 42
for a being set holds
( a in it iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def42 defines Subformulae ZF_LANG:def 42 :

theorem :: ZF_LANG:99

canceled;

theorem Th100: :: ZF_LANG:100

for G, H being ZF-formula st G in Subformulae H holds
G is_subformula_of H

proof end;

theorem :: ZF_LANG:101

for F, H being ZF-formula st F is_subformula_of H holds
Subformulae F c= Subformulae H

proof end;

theorem Th102: :: ZF_LANG:102

for x, y being Variable holds Subformulae (x '=' y) = {(x '=' y)}

proof end;

theorem Th103: :: ZF_LANG:103

for x, y being Variable holds Subformulae (x 'in' y) = {(x 'in' y)}

proof end;

theorem Th104: :: ZF_LANG:104

for H being ZF-formula holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}

proof end;

theorem Th105: :: ZF_LANG:105

for H, F being ZF-formula holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}

proof end;

theorem Th106: :: ZF_LANG:106

for x being Variable
for H being ZF-formula holds Subformulae (All x,H) = (Subformulae H) \/ {(All x,H)}

proof end;

theorem :: ZF_LANG:107

for H being ZF-formula holds
( H is atomic iff Subformulae H = {H} )

proof end;

theorem :: ZF_LANG:108

for H being ZF-formula st H is negative holds
Subformulae H = (Subformulae (the_argument_of H)) \/ {H}

proof end;

theorem :: ZF_LANG:109

for H being ZF-formula st H is conjunctive holds
Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}

proof end;

theorem :: ZF_LANG:110

for H being ZF-formula st H is universal holds
Subformulae H = (Subformulae (the_scope_of H)) \/ {H}

proof end;

theorem :: ZF_LANG:111

for H, G, F being ZF-formula st ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F holds
H in Subformulae F

proof end;

scheme :: ZF_LANG:sch 1
ZFInd{ P₁[ ZF-formula] } :

for H being ZF-formula holds P₁[H]

provided

A1: for H being ZF-formula st H is atomic holds
P₁[H] and
A2: for H being ZF-formula st H is negative & P₁[ the_argument_of H] holds
P₁[H] and
A3: for H being ZF-formula st H is conjunctive & P₁[ the_left_argument_of H] & P₁[ the_right_argument_of H] holds
P₁[H] and
A4: for H being ZF-formula st H is universal & P₁[ the_scope_of H] holds
P₁[H]

proof end;

scheme :: ZF_LANG:sch 2
ZFCompInd{ P₁[ ZF-formula] } :

for H being ZF-formula holds P₁[H]

provided

A1: for H being ZF-formula st ( for F being ZF-formula st F is_proper_subformula_of H holds
P₁[F] ) holds
P₁[H]

proof end;