SOME THEOREMS OF THE TERNARY DESCRIPTION LANGUAGE
3.1. Implications of elementary formulae.
The elementary formulae, in the genuine sense of this word, are only three: t, a, A. As for the derivative objects, like t¢, tÈ, tD, t°, Lt, the definienses of their definitions are rather complicated
609
formulae. But we can consider all of them as an elementary formulae of a sort. All basic and derivative objects are related to one another by implications. We will state these implications as the theorems of the TDL.
├─ A Þ a (189)
To prove it use the introduction rule for the attributive implication RB. The a-derivative formula for the formula A is a. According to RB we obtain (189).
├─ { t, Lt, a, t¢, tÈ, tD, t° } Þ a (190)
The theorem is proven with the help of substitution into the antecedent of the previous theorem according to the rule RA’ ’ ’1.
├─ t i® tÈ (191)
Take the axiom (93). On the basis of the substitution rule RA3 substitute i A for t and i AÈ for tÈ. Receive what must be proven.
├─ tÈ Þ t¢ (192)
To obtain (192), take the definition rule RF1, and apply it to the definition of tÈ.
├─ t Þ t¢ (193)
The result is received by application of the axiom of transitivity (98) (with the attributive implication Þ taken for ii®); the rule RA2 ; the rule of the deletion of iota operators RH2–1 (item a); and the theorems (191) – (192). Then we must use rule RC4 for lists and MP.
|
|
|
├─ { { t Þ t }, { Lt Þ Lt }, { a Þ a }, { t¢ Þ t¢ },
{ tÈÞ tÈ}, { tDÞ tD}, { t° Þ t° } } (194)
Take the law of identity (axiom 108: i A Þ i A ). On the base of the rule RA2 make the substitutions of both occurrences of A for t , Lt , etc. We can check that in each of the obtained cases the conditions of the rule RH2–1 are satisfied so that the iota operator can be deleted.
├─ a Þ t¢ (195)
Take the axiom (120). Using RA2, make the following substitutions: i A for i a, ii A for ii t, iii A for iii t¢, and iiii A for iiii t¢. Choose the attributive implication Þ as the meaning of ii®; then delete iota operators using RH2–1 (item a). We will receive:
{{ a Þ { t Ú t¢ }} · {{ t Þ t¢ }·{ t¢Þ t¢ }} } ® { a Þ t¢ }
The all three components of the antecedent of the neutral implications are provable. The first is the axiom (80), the second is the theorem (193), the third is implied by the theorem (194). The rule RC4 states that the whole antecedent is provable. Then the consequent is proved due to MP.
├─ A Þ t¢ (196)
Put together the theorems (189) and (195). The usage of the transitivity axiom (98) and the rules RC4 and MP gives the possibility to prove (196). It is also necessary to delete iota operators that occur in (98), so we must use RH2–1a and RH2–1b (the last allows to delete i in front of A ).
├─ { Lt , t¢ , tD , t° } Þ t¢ (197)
|
|
|
610
This theorem is proved by substitution into the antecedent of the previous theorem (196) according to the rule RA’ ’ ’1.
├─ tD i® t (198)
Take the axiom (95). Substitute i AD for i tD, and i A for i t on the base of RA3 and then delete iota operators using RH2–1a. We obtain (198).
├─ tD i® tÈ (199)
This can be proved by application of the transitivity axiom (98) to the theorems (198) and (191). Use RA2 and RH2–1a , and then the rules RC4 and MP.
├─ Lt Þ t (200)
This can be obtained by using the definition rule RF1 for the definition of Lt (see Part II, formula 3.43).
├─ Lt i® tÈ (201)
Put together the previous theorem and the theorem (191). Use the transitivity axioms (98) and (100). Using RA2 make the substitutions: i A for i Lt, ii A for ii t, and iii A for iii tÈ. Delete iota operators (RH2–1a). We receive from (98), taken Þ as ii® :
├─ {{ Lt Þ t } · { t Þ tÈ }} ® { Lt Þ tÈ }
Analogously from (100) we receive
├─ {{ Lt Þ t } · { t É tÈ }} ® { Lt É tÈ }
Put together the above two results, we obtain
|
|
|
├─ {{ Lt Þ t } · { t i® tÈ }} ® { Lt i® tÈ }
Applying RC4 and MP, we obtain (201) from the last formula.
├─ tD É Lt (202)
Accordingly to (198), taking É as i®, we have ├─ tD É t . Take the axiom (94): ├─ t É Lt. Use the transitivity axiom (98). Make the necessary substitutions (RA2) and delete iota operators (RH2–1a). We will obtain ├─ {{ tD É t } · { t É Lt }} ® { tD É Lt }. Applying RC4 and MP, we finally obtain (202).
3.2. Theorems that characterize relations between implications.
├─ { i A Þ ii A } Þ { i A ® ii A } (203)
Designate implications { i A Þ ii A }, { i A É ii A } and { i A ® ii A } by the symbols i3 A , i4 A and i5 A respectively. Accordingly to the axioms (105) and (106) we obtain:
├─ {i3 A Þ i4 A } and ├─ {i4 A Þ i5 A }. Both implications are accepted. Therefore, according to the rule RC4, the related list {i3 A Þ i4 A } · {i4 A Þ i5 A } is accepted, too. According to the transitivity axiom (98) we obtain
├─ {{i3 A Þ i4 A } · {i4 A Þ i5 A }} ® {i3 A Þ i5 A }
Finally, using MP, we obtain ├─ {i3 A Þ i5 A }, that is (203).
├─ { i A Þ ii A } ® { i A ® ii A } (204)
611
Let us designate the implication {i AÞii A} by the symbol i3 A, and the implication {i A®ii A} by the symbol i4 A. Accordingly to (203), we have ├─ { i3A Þ i4A } Þ { i3A ® i4A }, i.e.
|
|
|
├─ {{ i A Þ ii A }Þ { i A ® ii A } } Þ {{ i A Þ ii A }® { i A ® ii A } }
The antecedent of the main implication here is (203), so it is accepted. Therefore, the consequent, i.e. (204), is proved due to MP.
├─ { i A É ii A } ® { i A ® ii A } (205)
This theorem can be proven on the basis of the axiom (106) analogous to the proof of (204).
├─ { i A f ii A } ® { i A ® ii A } (206)
This theorem can be proven on the base of the axiom (107) analogous to the proof of (204).
3.3. Theorems of substantivation.
├─ [(i A)i A]Û i A (207)
Take the axiom (150): ├─ [(A)i A] Þ i A. Substitute [(i A)i A] onto the antecedent accordingly to the rule RA1. The comparison of the axioms (150) and (2.1.5.4) makes evident the identity of endings (condition e of the rule RA1). Obtain: ├─ [(i A)i A] Þ i A. Combination of the last result with axiom (154) gives the required theorem.
├─ [(i A) a]Û i A (208)
Take the theorem (207). According to the rule RJ4 we can substitute the second occurrence of i A in (207) for a. Thus (208) is accepted.
├─ [(a){ a, t, Lt, t¢, tÈ, tD, t° }] Û { a, t, Lt, t¢, tÈ, tD, t° } (209)
Take the axiom (150): ├─ [(A)i A] Þ i A. Substitute i A for i { a, t, Lt, t¢, tÈ, tD, t° } on the basis of RA2 to obtain
├─ [(A)i { a, t, Lt, t¢, tÈ, tD, t° }] Þ i { a, t, Lt, t¢, tÈ, tD, t° }
Delete the iota operators on the base of RH2–1a , then substitute the antecedent for
[(a)i { a, t, Lt, t¢, tÈ, tD, t° }] on the base of RA1 . The requirement e of RA1 is fulfilled because of the identity of the lists on the non-initial places. The other requirements of RA1 are fulfilled as well. We obtain:
├─ [(a){ a, t, Lt, t¢, tÈ, tD, t° }] Þ { a, t, Lt, t¢, tÈ, tD, t° }
Further, use the axiom (154): ├─ i A Þ [(i A)i A]. Substitute the second i A for a on the basis of RJ4: ├─ i A Þ [(a)i A]. Substitute i A for i{ a, t, Lt, t¢, tÈ, tD, t° } on the basis of RA2. Then delete the iota operators on the basis of RH2–1a, we obtain
├─ { a, t, Lt, t¢, tÈ, tD, t° } Þ [(a){ a, t, Lt, t¢, tÈ, tD, t° }]
Put together the two obtained results, we obtain (209).
├─ i A Û [(a*)i A] (210)
612
Use the substantivation axiom (151): ├─ [(i A*)i A] Û i A . The rule RJ4 allows us to substitute the first (from the left side) occurrence of i A for a, so (210) is provable.
├─ i A Û [i A(*a)] (211)
This theorem can be proven analogously to the previous one using the axiom (153) instead of (151).
Дата добавления: 2021-07-19; просмотров: 59; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!