appendix a Postulates for Modal Logic, TenseLogic, and UCalculi
appendix a Postulates for Modal Logic, TenseLogic, and UCalculi
(p.175) (All postulates are for appending to propositional calculus with substitution and detachment.)
I. Modal Logic
(Only systems of modal logic with established correlations with systems of tenselogic are included.)
§ 1. Gödel–Feys systems
(L undefined)
§ 1.1. Feys’s (1950) system T (= von Wright’s M of § 9.2)
Df. M:M = NLN 
RL: ├α → ├Lα 
Axioms: 1. CLCpqCLpLq, 2. CLpp. 
§ 1.2. The system S4 (Gödel’s axiomatization, 1933): T+CLpLLp.
§ 1.3. The system S5 (Gödel, 1933): T+CNLpLNLp (or CMLpLp).
§ 2. Von Wright’s (1951) systems
(M undefined)
§ 2.1. The system M (= T of § 1.1):
Df. L:L = NMN 
RL:├α → ├NMNα 
RE:├Eαβ→ ├EMαMβ 
Axioms: 1. EMApqAMpMq; 2. CpMp. 
(If Ax. 1 is replaced by CNMNCpqCMpMq, RE may be dropped, and the equivalence to T made more obvious.)
§ 2.2. The System M' (= S4): M+CMMpMp.
§ 2.3. The system M″ (= S5): M+CMNMpNMp (or CMpLMp).
§ 3. Systems between T and S5
§ 3.1. The ‘Brouwersche’ system, or system B: T+CpLMp (or CMLpp).
§ 3.2. The system S4.2: S4+CMLpLMp (simplified from Prior’s CMLpLMLp; Geach 1957).
(p.176) § 3.3. The system S4.3: S4+ALCLpqLCLqp (simplified from Lemmon’s ALCLpLqLCLqLp; Geach 1957), or CKMpMqAMKpMqMKgMp (Hintikka, 1957).
§ 3.4. The ‘Diodorean’ system D: S4.3+CLCLCpLppCMLpp (simplified from Dummett’s CLCLCpLpLpCMLpLp, Geach 1959; completeness proved by Kripke 1963, and Bull 1963).
II. Tense Logic
§ 4. The minimal tenselogic K_{t}
(Lemmon, 1965)
§ 4.1. With G and H undefined:
Df. F:F = NGN 
Df. P:P = NHN 
RG: ├α → ├Gα 
RH: ├α → ├Hα 
Axioms: 

1.1. CGCpqCGpGq 
1.2. CHCpqCHpHq 
2.1. CNHNGpp 
2.2. CNGNHpp. 
§ 4.2. With F and P undefined: 

Df. G: G = NFN 
Df. H:H = NPN 
RG: ├α → ├NFNα 
RH: ├α → ├NPNα 
Axioms: 

1.1. CNFNCpqCFpFq 
1.2. CNPNCpqCPpPq 
2.1. CPNFNpp 
2.2. CFNPNpp. 
Notes. (a) The 2’s, in each case, are abbreviable to CPGpp and CFHpp, and could be replaced by CpGPp and CpHFp.
(b)With Lα for KαGα, or Mα for AαFα, the ‘modal’ fragment of K_{t} is the system T of § 1.1, or M of § 2.1.
(c)With Lα for KKαGαHα, or Mα for AAαFαPα, the ‘modal’ fragment of K_{t} is the system B of § 3.1.
§ 5. Standard enlargements of the minimal system
§ 5.1. Axioms to be drawn upon, for addition to K_{t}:
3. CGpGGp (= CFFpFp = CHpHHp = CPPpPp = CFHpHp = CPpGPp = CPGpGp = CFpHFp; Lemmon, 1965)
4. CGGpGp (= GFpFFp = CHHpHp = CPpPPp = CFHpHp = CPGpPp = CGpGPp = CFHpFp)
5.1 CGpNGNp (= CNFNpFp = CNFpFNp = CGNpNGp = NGNCpp = FCpp)
5.2. CHpNHNp (= CNPNpPp = CNPpPNp = CHNpNGp = NHNCpp = PCpp)
(Definitionally, 5.1. = CGpFp and 5.2 = CHpPp.)
(p.177) 6.1. GKFpFqAAFKpqFKpFqFKqFp (= AGCpCGqrGCNpGGrq; Lemmon, 1965) (= AGCpCGpqGCGqp; C. Howard, 1966)
6.2. CKPpPqAAPKpqPKpPqPKqPp (= AHCpCHqrHCNpCHrq = AHCpCHpqHCHqp)
7.1. CKKpGpHpHGp (= CPFpAApFpPp)
7.2. CKKpHpGpGHp (= CFPpAApPpFp).
§ 5.2. System of ‘The Syntax of TimeDistinctions’ (1954) for dense, nonending, nonbeginning time
Add 3, 4, 5.1, and 5.2 to K_{t}.
§ 5.3. System for relativistic causal time (Cocchiarella, 1965; superfluous axioms deleted).
Add 3 only to K_{t}.
With Lα for KαGα, or Mα for AαGα, the ‘modal’ fragment is S4 of § 1.2. or § 2.2.
§ 5.4. System for linear time (Cocchiarella, 1965; superfluous axioms deleted).
Add 3, 6.1 and 6.2 to K_{t}.
With Lα for KαGα or Mα for AαGα, the ‘modal’ fragment is S4.3 § § 3.3.
With La for KKαGαHα or Mα for AAαGαHα, the ‘modal’ fragment is S5 of § 3.1 or § 2.3.
§ 5.5. System for linear, nonending, nonbeginning time (Scott, 1965).
Add 3, the 5’s and the 7’s to K_{t}.
‘Modal’ fragments as in § 5.4.
§ 5.6. System for dense, linear, nonending, nonbeginning time (Prior, 1965; superfluous axioms deleted).
Add 3, 4, the 5’s and the 7’s.
‘Modal’ fragments as in § 5.4.
§ 5.7. System designed for the work of 5.6 (Hamblin, 1958) and in fact giving logic of F as ‘is or will be’ and P as ‘is or has been’. (F and P undefined, dff. G and H as in § 23.4).
RG: ├α → ├Gα
RE: ├Eαβ → ├EFαFβ
RMI: In any thesis we may simultaneously replace every F by P, every P by F, every G by H, and every H by G.
Axioms:
1. CGpFp 
2. EFApqAFpFq 
3. EFFpFp 
4. EApPpGPp 
5. EAApPpFpFPp. 
§ 5.8. Equivalent system with G and H undefined.
RG, RMI, and Axioms 1. CGCpqCGpGq, 2. CGpp, 3. CGpGGp, 4. CpGPp, 5. CGpCHpGHp; or simply add 2, 3, 5, and 5’s image to K_{t}.
(p.178) § 6. Systems for circular time
§ 6.1. Without change of sign
Add to § 31.5 the axioms
1. CGpHp (= CHpGp = CFpPp = CPpFp = CFGpp = CPHpp = CpGFp = CpHPp; Lemmon, 1965).
2. CGpp (= CHpp = CpFp = CpPp).
3. CGpGGp.
§ 6.2. With change of sign, and antipodes both past and future (Lemmon 1965).
Add to K_{t} the axiom CGpPp (= CHpFp = CGGpp = CHHpp CpFFp = CpPPp).
§ 6.2. With change of sign, and antipodes neither past nor future.
Add to K_{t} the axiom CFGpPp (Hamblin, 1965), which = CPHpFp = CGpHPp = CHpGFp = CGGpHp = CHHpGp = CPpFFp = CFpPPp = CFGGpp = CPHHpp = CpGFFp = CpHPPp.
§ 7. Systems for the next moment (T) and the last moment (Y)
§ 7.1. For appending to S5 (of § 3.1) for undefined L (‘always’) (Scott 1964):
1. ELpTLp 
2. ELpLTp 
3. ETNpNTp 
4. ETCpqCTpTq 
5. ETYpp 
6. CLCpTpCLCqYqCMKpqLApq. 
§ 7.2. For use with G for ‘It is and always will be’ and H as ‘It is and always has been’ (Lemmon, 1964).
Use RG and axioms 1 and 2 of § 5.8, and the axioms 3. ETNpNTp, 4. ETCpqCTpTq, 5. ETGpGTp, 6. CGpTGp, 7. CGCpTpCpGp, and 8. ETYpp;’ and their mirror images.
§ 7.3. For use with normal G and H (Scott, 1965).
Add to the system of § 33.5 the axioms 1. CGpTp, 2. ENTNpTp, 3. CTCpqCTpTq, 4. CpYTp, 5. CTpCGCpTpGp, and their mirror images.
§ 46.7 For use alone (Clifford, 1965):
RT: ├α → ├Tα, ├ϒα
Axioms: 1. CTNpNTp, 2. CNTpTNp, 3. CTCpqCTpTq, 4. CpYTp, and their mirror images.
(Axioms with only T suffice for formulae with only T; ditto ϒ.)
§ 7.5. Equivalent of Tfragment with dyadic primitive (von Wright, 1965).
(The primitive form is Tpq for ‘p now and q next’.) RE: ├Eαβ → ├Efαfβ (for any f of the system).
(p.179) Axioms: 1. ETApqArsAAATprTpsTqrTqs, 2. EKTpqTrsTKprKqs, 3. EpTpAqNq, 4. NTpKqNq.
III. UCalculi
§ 8. Basic U–T postulates
U1. ETaNpNTap
U2. ETaCpqCTapTaq
and for tenselogic
U3. ETaGpΠbCUabTbp
U4. ETaHpΠbCUbaTbp
and for modal logic
U5. ETaLpΠbCUabTbp.
(All for appending not merely to propositional calculus with substitution and detachment, but to firstorder predicate calculus with identity.)
If and only if ha in the modal system determined by RL: ├α → ├Lαand the axiom A1. CLCpqCLpLq, then ├Taα in the system determined by U1, U2, and U5.
If and only if ├α in K_{t} of § 4, then ├Taα in the system determined by U1, U2, U3, U4.
§ 9. Correspondences between Ucalculi, modal logics, and tenselogics
(mostly suggested by Lemmon)
We write ‘γ ∼ β’ for ‘├α in the modal logic determined by RL, A1, and ├β, if and only if ├Taα in the Ucalculus determined by U1, U2, U5, and ├γ’, or for ‘├α in the tenselogic determined by K_{t}+├β if and only if ├Taα in the Ucalculus determined by U1, U2, U3, U4, and ├γ’.
§ 9.1. Correspondence of formulae
1. Uaa (reflexiveness) 
∼ CLpp (CGpp, CHpp) 
2. CUabUbb (right reflexiveness) 
∼ LCLpp (GCGpp) 
3. CUabUba (symmetry) 
∼ CpLMp (CpGFp) 
4. CUabCUbcUac (transitiveness) 
∼ CLpLLp (CGpGGp) 
5. CUabCUacUbc 
∼ CMLpLp 
6. CKUabUacAUbcUcb 
∼ CKMpMqAMKpMqMKqMp 
7. CKUabUacΣdKUbdUcd (convergence) 
∼ CMLpLMp 
8. CKUabUacAAIbcUbcUcb (nonbranching to right) 
CKFpFqAAFKpqFKpFqFKqFp 
9. CKUbaUcaAAIbcUbcUcb (nonbranching to left) 
∼ CKPpPqAPKpqPKpPqPKqPp 
10. ΣbUab (existence of successor) 
∼ CGpFp (CLpMp) 
11. ΣbUba (existence of predecessor) 
∼ CHpPp 
12. ΣbKUabUba 
∼ CGGpp (CLLpp) 
13. CUabΣcKUacUcb (‘density’) 
∼ CGGpGp(CLLpLp). 
(p.180) § 9.2. Entailments of formulae
(Where n and m are numbered conditions from § 9.1, ’n entails m’ means that (a) if the Uformula n is added as an axiom to the lower predicate calculus, m is deducible from it, and also that (b) if the modal formula n is added as an axiom to the modal system determined by RL and A1, or the tenselogical formula n is added to K_{t}, the modal or tenselogical formula m is deducible.)

1 entails 2, 10, 11, 12, 13.

2 entails 13, and is entailed by 1, 5, 6.

3 entails 7.

5 entails 2, 6, 8.

6 entails 2, 8, and is entailed by 5.

7 is entailed by 3.

10 is entailed by 1, 12.

11 is entailed by 1, 12.

12 entails 10, 11, and is entailed by 1.

13 is entailed by 1, 2.

(1+5) entails 3, 4.

(3+4) entails 5.

(1+6) entails 7.
§ 9.3. Correspondence of systems
(‘Condition n’ means the Ucondition n of § 9.1, supposed added to the basic postulates of § 8.)
System T of § 1.1 
∼ condition 1 
System S4 of § 2.1 
∼ (1+4) 
System S5 of § 3.1 
∼ (1+5) i.e. (1+3+4) 
System B of § 14.3 
∼ (1 +3) 
System S4.2 of § 15.3 
∼ (1+4+7) 
System S4.3 of § 16.3 
∼ (1 +4+6) 
System of § 31.5 (Cocchiarella, relativistic causal time) 
∼ 4 
System of § 32.5 (Cocchiarella, linear time) 
∼ (4+8+9) 
System of § 33.5 (Scott: doubly in finite linear time) 
∼ (4+8+9+10+11) 
System of § 34.5 (Prior: dense Scott) 
∼ (4+8+9+10+11+13) 
System of § 36.6 (normal circular time) 
∼ (1+3+4) (as S5) 
System of § 37.6 (‘eastwest’ circular time with antipodes) 
∼ 12. 