THE EXAMPLES OF SYSTEM-THEORETICAL LAWS
AS THEOREMS OF T.D.L.
4.1. Theorem 1. Any structurally open system is a structural-non-point system.
The proof. Let us take the definition of the superobject i AD (see formula 16). Definiendum is defined with the help of i A¢ , which is the Genus proximum of the definiens. On the basis of the rule RF1 we have
├─ i AD Þ i A¢ (212)
From this according to the rule of substitution RA3 we obtain
├─ i aD Þ i a¢ (213)
Let us take the axiom of the inverse relational restriction (136) and apply the rule of renaming iota operators RH3 to it:
├─ {i4 A Þ i5 A} « {[i4 A(*i6 A)]Þ [i5 A(*i6 A)]} (214)
Make the following substitutions in (214) using the rule RA2: substitute i4 A for i4 {i aD} ; i5 A – for i5 {i a¢} ; i6 A – for i6 {iii A}. Obtain:
├─ {i4 {i aD}Þ i5 {i a¢}} « {[i4 {i aD} (*i6 {iii A})]Þ [i5 {i a¢} (*i6 {iii A})]} (215)
Use the rule of iota operators deletion RH2–1a to delete i4 , i5 and i6 . Obtain:
├─ {i aD Þ i a¢ } « {[i aD (*iii A )]Þ [i a¢ (*iii A )]} (216)
Applying MP to (213) and (216) gives
├─ [i aD (*iii A )]Þ [i a¢ (*iii A )] (217)
Here we add and delete curly brackets according to the rule RL.
Now use the axiom of the direct attributive restriction (121) and rename iota operators in it (RH3). Obtain:
├─ {i4 A Þ i5 A} ® {[(i4 A)i6 A]Þ [(i5 A) i6 A]} (218)
Make the following substitutions in (218) using the rule RA2: substitute i4 A for
i4 [i aD(*iii A)] ; i5 A – for i5 [i a¢ (*iii A)] ; i6 A – for i6 t . Obtain:
|
|
|
├─ {i4 [i aD(*iii A)]Þ i5 [i a¢ (*iii A)]} ®
® {[(i4 [i aD(*iii A)])i6 t]Þ [(i5 [i a¢ (*iii A)])i6 t]} (219)
613
Delete iota operators i4 , i5 and i6 on the base of RH2–1a; obtain
├─ {[i aD(*iii A)]Þ [i a¢ (*iii A)]} ® {[([i aD(*iii A)]) t]Þ [([i a¢ (*iii A)]) t]} (220)
Applying MP to (217) and (220) gives
├─ [([i aD(*iii A)]) t]Þ [([i a¢ (*iii A)]) t] (221)
Here we have deleted external curly brackets according to the rule RL.
Now let us use the rule RJ2 that allows us to change the closed formulae in the antecedent and consequent by the open ones:
├─ {([i aD(*iii A)]) t}Þ {([i a¢ (*iii A)]) t} (222)
Using RH3, rename iota operator i as ii , and then rename iii as i . Obtain:
├─ {([ii aD(*i A)]) t}Þ {([ii a¢ (*i A)]) t} (223)
Now use the axiom of reistic restriction (140), adding to both sides of (223) the definiens of the systems concept definition: ([ii a(*i A)]) t . After applying MP to thus obtained formula and (223), we obtain:
├─ {{([ii a(*i A) ]) t}·{([ii aD(*i A)]) t}}Þ {{([ii a(*i A) ]) t}·{([ii a¢ (*i A)]) t}} (224)
Now take the axiom (126) and rename iota operators in it:
├─ {i4 A Þ i5 A} « {[(i6 A)i4 A]Þ [(i6 A)i5 A]} (225)
Make the following substitutions in (225) using the rule RA2:
i4 A – for i4 {{([ii a(*i A) ]) t}·{([ii aD(*i A)]) t}} ;
i5 A – for i5 {{([ii a(*i A) ]) t}·{([ii a¢ (*i A)]) t}} ;
i6 A – for i6 {i A} .
Obtain:
|
|
|
├─ {3i4 {2{1([ii a(*i A) ]) t1} ·{1([ii aD(*i A)]) t1} 2} Þ i5 {2{1([ii a(*i A) ]) t1} ·{1( [ii a¢ (*i A)]) t1} 2} 3} «
« {3 [(i6 {i A})i4 {2{1([ii a(*i A) ]) t1} ·{1( [ii aD(*i A)]) t1} 2} ]Þ
Þ [(i6 {i A})i5 {2{1( [ii a(*i A) ]) t1} ·{1([ii a¢ (*i A)]) t1} 2} ]3} (226)
In order to avoid confusion we have indexed the braces by numbers here.
Now delete iota operators i4 , i5 and i6 in (226) on the basis of RH2–1a; then apply MP to (224) and the obtained formula. We will obtain the attributive implication (Þ) between closed formulae. Use the rule RJ2 and replace these closed formulae by open ones. Obtain:
├─ (i A){ {([ii a(*i A) ]) t} · {( [ii aD(*i A)]) t} }Þ
Þ (i A){ {([ii a(*i A) ]) t} · {([ii a¢ (*i A)]) t} } (227)
The antecedent of (227) coincides with the definiens of the definition of the structurally open system, and the consequent coincides with the definiens of the structural-non-point system. Thus the theorem is proven.
614
4.2. Theorem 2. Any gomeomeric system is a non-minimal system.
The proof. Take the axiom of the direct attributive restriction (121) and substitute ii A for ii a on the base of RA2. Receive:
├─ {i A Þ ii a } ® {[(i A)iii A]Þ [(ii a)iii A]} (228)
Omit the iota operator ii before a on the basis of RH2–1a. Now we may delete the iota operator i before A on the base of RH2–1b, and receive
├─ {A Þ a} ® {[(A)iii A]Þ [(a)iii A]} (229)
because after this deletion substitutions in the second occurrence of non-iotified A will be forbidden since this occurrence is included to the consequent of the implication (see the rule RA’ ’ ’1). Therefore, the first occurrence of A remains a single occurrence that is free for substitutions, so RH2–1b is applicable.
|
|
|
The antecedent of (229) is the theorem (189). Therefore, due to MP:
├─ [(A)iii A]Þ [(a)iii A] (230)
(the braces were deleted on the basis of RL.) Now apply RA2 to substitute iii A for iii AÈ :
├─ [(A)iii AÈ ]Þ [(a)iii AÈ ] (231)
Renaming the iota operator iii (RH3) gives:
├─ [(A)i AÈ ]Þ [(a)i AÈ ] (232)
Now take the axiom of the inverse relational restriction (138) and rename iota operators in it (RH3) to get:
├─ {i4 A Þ i5 A } « {[i6 A(*i4 A)]Þ [i6 A(*i5 A)]} (233)
Make the following substitutions in (233) using the rule RA2: substitute i4 A for i4 [(A)i AÈ ] ; i5 A – for i5 [(a)i AÈ ] ; i6 A – for i6 {iii A} . Obtain:
├─ {i4 [(A)i AÈ ]Þ i5 [(a)i AÈ ] } «
« {[i6 {iii A}(*i4 [(A)i AÈ ])]Þ [i6 {iii A}(*i5 [(a)i AÈ ])]} (234)
We can delete the iota operator i4 on the basis of RH2–1b because substitutions in A in the second occurrence of i4[(A)i AÈ ] are forbidden (it occupies the non-initial place in the closed subformula [i6{iii A}(*i4[(A)i AÈ ])] ). Hence, A in the first occurrence of i4[(A)i AÈ ] is a single occurrence that is free for substitutions, so RH2–1b is applicable. Furthermore, iota operators i5 and i6 can be deleted on the base of RH2–1a. Thus we obtain:
├─ {[(A)i AÈ ]Þ [(a)i AÈ ]} « {[iii A(*[(A)i AÈ ])]Þ [iii A(*[(a)i AÈ ])]} (235)
|
|
|
Now take into account that (232) is the antecedent of (235), and use MP. Deleting the external braces, we obtain:
├─ [iii A(*[(A)i AÈ ])]Þ [iii A(*[(a)i AÈ ])] (236)
615
Use the rule RA2 to substitute iii A for iii a , and then rename iota operator iii for ii . We obtain:
├─ [ii a(*[(A)i AÈ ])]Þ [ii a(*[(a)i AÈ ])] (237)
Now take the axiom of the direct attributive restriction (121) and rename iota operators in it (RH3) to obtain:
├─ {i4 A Þ i5 A } ® {[(i4 A)i6 A]Þ [(i5 A)i6 A]} (238)
Using the rule RA2, substitute in (238): i4 A for i4 [ii a(*[(A)i AÈ ])] ; i5 A – for
i5 [ii a(*[(a)i AÈ ])] ; i6 A – for i6 t . Obtain:
├─ {i4 [ii a(*[(A)i AÈ ])]Þ i5 [ii a(*[(a)i AÈ ])] } ®
® {[(i4 [ii a(*[(A)i AÈ ])])i6 t]Þ [(i5 [ii a(*[(a)i AÈ ])])i6 t]} (239)
After the deletion of iota operators i4 , i5 and i6 in (239), possible due to RH2–1a and RH2–1b we obtain:
├─ { [ii a(*[(A)i AÈ ])]Þ [ii a(*[(a)i AÈ ])] } ®
® {[( [ii a(*[(A)i AÈ ])]) t]Þ [( [ii a(*[(a)i AÈ ])]) t]} (240)
Now apply MP to (237) and (240). Deleting the external curly brackets (RL) we obtain:
├─ [( [ii a(*[(A)i AÈ ])]) t]Þ [( [ii a(*[(a)i AÈ ])]) t] (241)
Take now the axiom of the reistic restriction (140); use Þ as i® ; and rename iota operators in it (RH3) to obtain:
├─ {i4 A Þ i5 A } « {{i4 A ·i6 A } Þ {i5 A ·i6 A } } (242)
Make the following substitutions in (242) using the rule RA2:
i4 A – for i4 {( [ii a(*[(A)i AÈ ])]) t} ;
i5 A – for i5 {( [ii a(*[(a)i AÈ ])]) t} ;
i6 A – for i6 {([ii a(*i A) ]) t} .
Obtain:
├─ {i4 {( [ii a(*[(A)i AÈ ])]) t}Þ i5 {( [ii a(*[(a)i AÈ ])]) t} } «
« {{i4 {( [ii a(*[(A)i AÈ ])]) t}·i6 {([ii a(*i A) ]) t}} Þ
Þ {i5 {( [ii a(*[(a)i AÈ ])]) t}·i6 {([ii a(*i A) ]) t}} } (243)
We can delete iota operator i4 because the occurrence of A in its scope occupies the non-initial place of the closed formula, so RH2–1b is applicable. We can also delete i5 and i6 on the basis of RH2–1a. Obtain:
├─ { {( [ii a(*[(A)i AÈ ])]) t]}Þ {( [ii a(*[(a)i AÈ ])]) t} } «
« { {{( [ii a(*[(A)i AÈ ])]) t}·{([ii a(*i A) ]) t}} Þ
Þ {{( [ii a(*[(a)i AÈ ])]) t}· {([ii a(*i A) ]) t}} } (244)
616
Now open the antecedent and the consequent of (241) (rule RJ2), and apply MP to the result obtained and (244). Then change the order of the list's components. We obtain:
├─ { {([ii a(*i A) ]) t} · {( [ii a(*[(A)i AÈ ])]) t} } Þ
Þ { {([ii a(*i A) ]) t}· {( [ii a(*[(a)i AÈ ])]) t} } (245)
Let us now take the axiom of the direct attributive restriction (126) and rename iota operators in it (RH3) to get:
├─ {i4 A Þ i5 A } « {[(i6 A)i4 A]Þ [(i6 A)i5 A]} (246)
Make the following substitutions in (246) using the rule RA2
i4 A – for i4 { {([ii a(*i A) ]) t} · {( [ii a(*[(A)i AÈ ])]) t} } ;
i5 A – for i5 { {([ii a(*i A) ]) t}· {( [ii a(*[(a)i AÈ ])]) t} } ;
i6 A – for i6 {i A } .
Obtain:
├─ {3 i4 {2 {1 ( [1ii a(*i A)1] ) t1} · {1 ( [2ii a(*[1(A)i AÈ 1] ) 2] ) t 1} 2} Þ
Þ i5 {2 {1( [1ii a(*i A)1] ) t1} · {1 ( [2ii a(*[1(a)i AÈ 1] ) 2] ) t 1} 2} 3} «
« {3 [4(i6 {1i A1} )i4 {2 {1([1ii a(*i A)1] ) t1} · {1( [2ii a(*[1(A)i AÈ 1] ) 2] ) t1} 2} 4] Þ
Þ [4(i6 {1i A1} )i5 {2 {1([1ii a(*i A)1] ) t 1} · {1( [2ii a(*[1(a)i AÈ 1] ) 2] ) t 1} 2} 4] 3} (247)
Here we have indexed the square and the curly brackets to make the formula more readable.
The rules RH2–1a and RH2–1b1 allow us to delete iota operators i4 , i5 and i6. We obtain:
├─ { { {([ii a(*i A) ]) t} · {([ii a(*[[(A)i AÈ ]) ]) t} } Þ
Þ{ {([ii a(*i A) ]) t}· {([ii a(*[[(a)i AÈ ]) ]) t} } } «
« { [(i A) {{([[ii a(*i A) ]) t} · {([ii a(*[[ (A)i AÈ ]) ]) t}}]Þ
Þ [(i A) {{([ii a(*i A) ]) t}· {([ii a(*[[(a)i AÈ ]) ]) t}} ] } (248)
In (248) we omit the indexes of brackets, but the reader can refer to the previous formula (247) if necessary.
Now apply MP to formulae (245) and (248). We obtain:
├─ [(i A) {{([[ii a(*i A) ]) t} · {([ii a(*[[ (A)i AÈ ]) ]) t}}]Þ
Þ [(i A) {{([ii a(*i A) ]) t}· {([ii a(*[[(a)i AÈ ]) ]) t}} ] (249)
Here we have omitted the external braces on the basis of RL.
To continue the proof of Theorem 2 we will prove the following lemma now:
Lemma 1. ├─ i AÈ Û [[(a)i AÈ ] .
617
The proof of lemma 1. Take the substantivation axiom (150): ├─ [(A)i A] Þ i A. Use the substitution rule RA2 and substitute i A for i AÈ . Obtain:
├─ [(A)i AÈ ] Þ i AÈ (250)
Use now the rule RA1 and substitute [(A)i AÈ ] , where A is on the initial place in the antecedent of (250), for [(a)i AÈ ]. Obtain:
├─ [(a)i AÈ ] Þ i AÈ (251)
Take now the axiom (154): ├─ i A Þ [(i A)i A] . Substitute i A for i AÈ (RA2):
├─ i AÈ Þ [(i AÈ )i AÈ ] (252)
Use the rule RJ4 to obtain:
├─ i AÈ Þ [(a)i AÈ ] (253)
Putting together (251) and (253) we finish the proof of Lemma 1.
We now return to the proof of Theorem 2. Take the above result (249) and substitute the occurrence of [(a)i AÈ ] in its consequent for i AÈ . It is possible on the basis of Lemma 1 and the rule RJ1. The application of RJ1 is correct, because [(a)i AÈ ] and i AÈ have the same iota operator. Obtain:
├─ [(i A) {{([[ii a(*i A) ]) t} · {([ii a(*[[ (A)i AÈ ]) ]) t}}]Þ
Þ [(i A) {{([ii a(*i A) ]) t}· {([ii a(* i AÈ ) ]) t}} ] (254)
In (254) the antecedent coincides with the definiens of gomeomery system, and the consequent coincides with the definiens of non-minimal system. Thus Theorem 2 is proven.
4.3. Theorem 3. Any external-centric system is a nonimmanent system.
The proof. Take the axiom (162), rename the iota operators (RH3) to receive:
├─ (i4 A){i5 A · A} Þ (i4 A)i5 A (255)
Use the substitution rule RA2 and substitute in (255) i4 A for i4 {i A} and i5 A for
i5 {([ a(*i A·i A° ) ]) t }. Receive:
├─ (i4{i A}){i5{([ a(*i A·i A° ) ]) t } · A} Þ (i4{i A})i5{([ a(*i A·i A° ) ]) t } (256)
Omit the iota operators i4 and i5 on the basis of RH2–1a. Obtain:
├─ (i A){ {([ a(*i A·i A° ) ]) t } · A} Þ (i A){([ a(*i A·i A° ) ]) t } (257)
Use now the rule RA0 and substitute A in the antecedent for the following formula:
{ii {i A° } · {[ A(*i A) ] Þ [ a(*ii {i A° }) ]} }. Obtain:
├─ (i A){ {([ a(*i A·i A° ) ]) t } · {ii {i A° } · {[ A(*i A) ] Þ [ a(*ii {i A° }) ]} }} Þ
Þ (i A){([ a(*i A·i A° ) ]) t } (258)
618
In (258) the antecedent coincides with the definiens of external-centric system, and the consequent coincides with the definiens of nonimmanent system. Thus Theorem 3 is proven.
Theorem 3a. If a system is external-centric, it is a centric one.
The proof. Look at the definition of external-centric system. Use the rule RJ4, changing i A° by a . Receive the definition of the centric system.
Theorem 3b. If a system is internal-centric, it is a centric one.
The proof is analogous to the proof of the previous theorem. Consider i AÈ instead of i A° .
4.4. Theorem 4. If a system is non-minimal, it is also non-elementary.
The proof. Compare the definienses of two definitions – (1) non-minimal system:
(i A){{( [ii a(*i A)] )t} · {( [ii a(*i AÈ)] )t}}
and 2) non-elementary system:
(i A){{( [ a(*i A)] )t} · {( [ a(*i AÈ)] )t }}
The difference is only in the presence of iota operators ii in the first case and their absence in the second. But according to the rule RH2–1 (item a) we can delete these iota operators in the first definition and thus obtain the second as its consequence. The theorem is proven.
4.5. Theorem 5. Any non-minimal system is a non-unique one.
The proof. Let us take the definition (15) of the object i AÈ :
i AÈ =def [(i A¢ ){ i A É i A¢ }] (259)
According to the rule RF1 this definition implies that the following formula is accepted:
├─ i AÈ Þ i A¢ (260)
Use the axiom of inverse relational restriction (138), rename iota operators in it (RH3) and obtain:
├─ {i4 A Þ i5 A } « {[i6 A(*i4 A)]Þ [i6 A(*i5 A)]} (261)
Use the substitution rule RA2 and substitute in (261) i4 A for i4 {i AÈ} , i 5A for i5 {i A¢} and i6 A for i6 {ii a }. Obtain:
├─ {i4 {i AÈ}Þ i5 {i A¢}} « {[i6 {ii a }(*i4 {i AÈ})]Þ [i6 {ii a }(*i5 {i A¢})]} (262)
Delete iota operators i4 , i5 and i6 on the basis of RH2–1a, then omit braces on the basis of RL
├─ {i AÈ Þ i A¢ } « {[ii a(*i AÈ )]Þ [ii a(*i A¢ )]} (263)
619
Apply MP to (260) and (263):
├─ [ii a(*i AÈ )]Þ [ii a(*i A¢ )] (264)
Use the axiom of direct attributive restriction (121) and rename iota operators in it to obtain:
├─ {i4 A Þ i5 A} ® {[(i4 A)i6 A]Þ [(i5 A)i6 A]} (265)
Make the following substitutions (RA2): i4 A for i4 [ii a(*i AÈ )] , i 5A for i5 [ii a(*i A¢ )] and i6 A for i6 t . Obtain:
├─ {i4 [ii a(*i AÈ )]Þ i5 [ii a(*i A¢ )]} ®
® {[(i4 [ii a(*i AÈ )])i6 t]Þ [(i5 [ii a(*i A¢ )])i6 t]} (266)
Delete iota operators i4 , i5 and i6 on the basis of RH2–1a, receive:
├─ { [ii a(*i AÈ )]Þ [ii a(*i A¢ )]} ® {[( [ii a(*i AÈ )]) t]Þ [([ii a(*i A¢ )]) t]} (267)
Apply MP to (264) and (267):
├─ [( [ii a(*i AÈ )]) t]Þ [([ii a(*i A¢ )]) t] (268)
Now use the axiom of the reistic restriction (140), taking Þ as i®. Rename iota operators in it to obtain:
├─ {i4 A Þ i5 A } « {{i4 A ·i6 A } Þ {i5 A ·i6 A } } (269)
Make the following substitutions (RA2): i4 A for i4 [( [ii a(*i AÈ )]) t] , i 5A for i5 [([ii a(*i A¢)]) t] and i6 A for i6 {([ii a(*i A )]) t} . Then change the order of related list components and obtain:
├─ {i4 [( [ii a(*i AÈ )]) t]Þ i5 [([ii a(*i A¢ )]) t] } «
« { {i6 {([ii a(*i A )]) t}·i4 [( [ii a(*i AÈ )]) t] } Þ
Þ {i6 {([ii a(*i A )]) t}·i5 [([ii a(*i A¢ )]) t] } } (270)
Delete iota operators i4 , i5 and i6 on the basis of RH2–1a, then apply MP to the result and formula (268); obtain:
├─ { {([ii a(*i A )]) t}· [( [ii a(*i AÈ )]) t] } Þ
Þ { {([ii a(*i A )]) t}· [([ii a(*i A¢ )]) t] } (271)
Now take the axiom of direct attributive restriction (126). Rename iota operators in it to receive:
├─ {i4 A Þ i5 A} « {[(i6 A)i4 A]Þ [(i6 A)i5 A]} (272)
Make the following substitutions (RA2):
i4 A for i4 { {([ii a(*i A )]) t}· [( [ii a(*i AÈ )]) t] } ,
i 5A for i5 { {([ii a(*i A )]) t}· [([ii a(*i A¢ )]) t] } ,
i6 A for i6 {i A } .
620
Receive:
├─ {3 i4 {2 {1([ii a(*i A )]) t 1} · [( [ii a(*i AÈ )]) t] 2} Þ
Þ i5 {2 {1 ([ii a(*i A )]) t 1} · [([ii a(*i A¢ )]) t] 2} 3} «
« {3 [(i6 {i A })i4 {2 {1 ([ii a(*i A )]) t 1} · [( [ii a(*i AÈ )]) t] 2} ]Þ
Þ [(i6 {i A })i5 {2 {1([ii a(*i A )]) t 1} · [([ii a(*i A¢ )]) t] 2} ] 3} (273)
Delete iota operators i4 , i5 and i6 on the basis of RH2–1a, then apply MP to the result and formula (271); receive:
├─ [(i A ){2 {1 ([ii a(*i A )]) t 1} · [( [ii a(*i AÈ )]) t] 2} ]Þ
Þ [(i A ){2 {1([ii a(*i A )]) t 1} · [([ii a(*i A¢ )]) t] 2} ] (274)
Accordingly to the rule RJ2 replace the closed antecedent and consequent in (274) by open formulae:
├─ {(i A ){2 {1 ([ii a(*i A )]) t 1} · [( [ii a(*i AÈ )]) t] 2} }Þ
Þ {(i A ){2 {1([ii a(*i A )]) t 1} · [([ii a(*i A¢ )]) t] 2} } (275)
The antecedent of (275) coincides with the definiens of non-minimal system, and the consequent with the definiens of non-unique system. Theorem 5 is proven.
4.6. Theorem 6. Any substratum-open system is a non-unique one.
The proof. Take the definition (16) of the object i AD :
i AD =def [(i A¢){ i A¢ É i A }]
According to the rule RF1 this definition implies that the following formula is accepted:
├─ i AD Þ i A¢
Analogous to the proof of the previous theorem, we can deduce from it the following:
├─ {(i A ){2 {1 ([ii a(*i A )]) t 1} · [( [ii a(*i AD )]) t] 2} }Þ
Þ {(i A ){2 {1([ii a(*i A )]) t 1} · [([ii a(*i A¢ )]) t] 2} }
Here the antecedent of the implication coincides with the definiens of substratum-open system, and its consequent coincides with the definiens of non-unique system, so the theorem is proven.
621
4.7. Theorem 7. If a system is (1) totalitarian and (2) structurally non-variable,
then it is also a rigid one.
The proof. Applying the rule RF2 to the definitions of totalitarian (30) and structurally non-variable (31) systems, we obtain the definition of a system that possesses both properties:
( i A )Totalitarian and structurally non-variable system =def
(i A){ {( [ a(*i A)] )t} · { t ® [A(*i A)]} ·
· {( [ii a(*i A)] )t} · { [A(*i A)] Þ ii a} } (276)
The first component of the related list in the definiens of (276) is the consequence of the third component due to the rule RH2–1a. Therefore, with the help of RC5, we can delete it from the list. Then put the component {([ii a (*i A)])t} of the list onto its first place, and bind the free occurrences of A in all components of the list with iota operator iii , which is possible due to RH9. We obtain the final definition:
( i A )Totalitarian and structurally non-variable system =def
(i A){ {( [ii a(*i A)] )t} · {t ® [iii A(*i A)]} · { [iii A(*i A)] Þ ii a} } (277)
Use the axiom of transitivity for neutral and attributive implication (103) and rename iota operators in it (RH3) to obtain
├─ {{i4 A ® i5 A} · {i5 A Þ i6 A}} ® {i4 A ® i6 A} (278)
Make the following substitutions (RA2) in (278): i4 A for i4 t , i 5 A for i5 [iii A(*i A)] and i6 A for i6 {ii a} . Obtain:
├─ {{i4 t ® i5 [iii A(*i A)]} · {i5 [iii A(*i A)]Þ i6 {ii a}}} ® {i4 t ® i6 {ii a}} (279)
Omit iota operators i4 , i5 and i6 on the basis of the rule RH2–1a. Obtain:
├─ {{t ® [iii A(*i A)]} · {[iii A(*i A)]Þ ii a}} ® { t ® ii a} (280)
Take now the axiom (89) with Þ as ii®. Rename iota operators in it (RH3) to obtain:
├─ {{(i4 A ·i5 A)T} · {i5 A Þ i6 A}} ® {i4 A ·i6 A} (281)
Make the following substitutions (RA2) in (281):
i4 A for i4 {( [ii a(*i A)] )t} ,
i 5 A for i5 {{t ® [iii A(*i A)]} · { [iii A(*i A)] Þ ii a} } ,
i6 A for i6 { t ® ii a} .
Obtain:
├─ {4 {3 (2 i4 {1([ii a(*i A)])t1} ·i5 {2{1t ® [iii A(*i A)]1} · {1 [iii A(*i A)] Þ ii a1} 2} 2) T 3} ·
· {3 i5 {2 {1 t ® [iii A(*i A)] 1} · {1 [iii A(*i A)] Þ ii a1} 2} Þ i6{ t ® ii a} 3} 4} ®
® {2 i4 {1([ii a(*i A)] )t1} · i6 { t ® ii a} 2} (282)
622
Omit iota operators i4 , i5 and i6 on the basis of the rule RH2–1a. Receive:
├─ {4 {3 (2 {1([ii a(*i A)])t1} · {2{1t ® [iii A(*i A)]1} · {1 [iii A(*i A)] Þ ii a1} 2} 2) T 3} ·
· {3 {2 {1 t ® [iii A(*i A)] 1} · {1 [iii A(*i A)] Þ ii a1} 2} Þ{ t ® ii a} 3} 4} ®
® {2 {1([ii a(*i A)] )t1} · { t ® ii a} 2} (283)
Now use the axiom (127) and rename iota operators in it (RH3) to obtain
├─ {i4 A ® i5 A} « {[(i6 A)i4 A]® [(i6 A)i5 A]} (284)
Make the following substitutions (RA2) in (284):
i4 A for the antecedent of the implication (283) preceded by i4 , i.e.:
i4 {4 {3 (2 {1([ii a(*i A)])t1} · {2{1t ® [iii A(*i A)]1} · {1 [iii A(*i A)] Þ ii a1} 2} 2) T 3} ·
· {3 {2 {1 t ® [iii A(*i A)] 1} · {1 [iii A(*i A)] Þ ii a1} 2} Þ{ t ® ii a} 3} 4} (285)
i 5 A for the consequent of (283) preceded by i5 , i.e.:
i5 {2 {1([ii a(*i A)] )t1} · { t ® ii a} 2} (286)
i6 A for i6 {i A} (287)
After these substitutions the rule RH2–1a will be applicable, so we can delete iota operators i4 , i5 and i6 from the result. Thus we obtain the implication, whose antecedent, i.e. (283), has been proved. Applying MP, we obtain the formula thus obtained from the consequent of (284), i.e. from
[(i6 A)i4 A]® [(i6 A)i5 A] (288)
should be accepted. On the basis of the rule RJ2 we can state that the implication
{(i6 A)i4 A}® {(i6 A)i5 A} (289)
obtained (after the above transformations) from (288) by opening its antecedent and consequent should be accepted, too:
├─ {(i A){4{3 (2 {1([ii a(*i A)])t1} · {2{1t ® [iii A(*i A)]1} · {1 [iii A(*i A)] Þ ii a1} 2} 2) T 3} ·
· {3 {2 {1 t ® [iii A(*i A)] 1} · {1 [iii A(*i A)] Þ ii a1} 2} Þ{ t ® ii a} 3} 4} }®
® {(i A){2 {1([ii a(*i A)] )t1} · { t ® ii a} 2} } (290)
The consequence of (290) coincides with the definiens of the rigid system. What about the antecedent? From the formal point of view there are two distinctions of the (290) antecedent from the definiens of the totalitarian and structurally non-variable system (277). The first is the presence of the valent sign T in the middle of the formula, but we may omit it due to RF4. The second distinction is the presence of the following neutral implication
623
in the (290) antecedent:
{2 {1 t ® [iii A(*i A)] 1} · {1 [iii A(*i A)] Þ ii a1} 2} Þ{ t ® ii a} (291)
This implication can be deduced from the axiom (103) by making necessary substitutions in it and then deleting some iota operators that is possible on the basis of the rule RH2–1a.
According to the rule RF3 the provable component of the list, that is (291), may be omitted from the definiens of the definition. Therefore, we obtain from (290):
├─ {(i A){2{1([ii a(*i A)])t1} · {1t ® [iii A(*i A)]1} · {1 [iii A(*i A)] Þ ii a1} 2} }®
® {(i A){2 {1([ii a(*i A)] )t1} · { t ® ii a} 2} }
Ergo, theorem 7 is proven.
During the proof of system-theoretical laws we have used only a part of the TDL resources. The usage of other resources permits us to enlarge the number of parametrical GST theorems.
Acknowledgements
I would like to express my big thanks to my colleague Mr. L. Leonenko for his assistance in the heavy work of the editing of my text.
References
Djdjan, R.Z. (1977) Broadened Syllogistics (University Press, Erevan). (In Russian)
Rapoport, A. (1966) “Mathematical aspects of general systems analysis”, General Systems 11, 3-11.
Subbotin, A.L. (1969) Traditional and Modern Formal Logic (“Nauka” Publ. House, Moscow). (In Russian)
Ujomov, A.I. (1965) Dinge, Eigenschaften und Relationen (Akademie Verlag, Berlin).
Uyemov, A.I. (1955) “Concerning conclusions by restrictions and conditions of their validity”, Transactions of Ivanovo Pedagogical Institute, 8, 251-265. (In Russian)
Дата добавления: 2021-07-19; просмотров: 65; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!