Jump to ContentJump to Main Navigation
Past, Present and Future$

Arthur Prior

Print publication date: 1967

Print ISBN-13: 9780198243113

Published to Oxford Scholarship Online: October 2011

DOI: 10.1093/acprof:oso/9780198243113.001.0001

Show Summary Details
Page of

PRINTED FROM OXFORD SCHOLARSHIP ONLINE (www.oxfordscholarship.com). (c) Copyright Oxford University Press, 2017. All Rights Reserved. Under the terms of the licence agreement, an individual user may print out a PDF of a single chapter of a monograph in OSO for personal use (for details see http://www.oxfordscholarship.com/page/privacy-policy). Subscriber: null; date: 30 March 2017

appendix a Postulates for Modal Logic, Tense-Logic, and U-Calculi

appendix a Postulates for Modal Logic, Tense-Logic, and U-Calculi

Source:
Past, Present and Future
Publisher:
Oxford University Press

(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 tense-logic 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: ├α → ├

          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 tense-logic Kt

(Lemmon, 1965)

§ 4.1. With G and H undefined:

            Df. F:F = NGN

Df. P:P = NHN

            RG: ├α → ├

RH: ├α → ├

          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 for KαGα, or for AαFα, the ‘modal’ fragment of Kt is the system T of § 1.1, or M of § 2.1.

(c)With for KKαGαHα, or Mα for AAαFαPα, the ‘modal’ fragment of Kt is the system B of § 3.1.

§ 5. Standard enlargements of the minimal system

§ 5.1. Axioms to be drawn upon, for addition to Kt:

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 ofThe Syntax of Time-Distinctions’ (1954) for dense, non-ending, non-beginning time

Add 3, 4, 5.1, and 5.2 to Kt.

§ 5.3. System for relativistic causal time (Cocchiarella, 1965; superfluous axioms deleted).

Add 3 only to Kt.

With for KαGα, or 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 Kt.

With for KαGα or for AαGα, the ‘modal’ fragment is S4.3 § § 3.3.

With La for KKαGαHα or for AAαGαHα, the ‘modal’ fragment is S5 of § 3.1 or § 2.3.

§ 5.5. System for linear, non-ending, non-beginning time (Scott, 1965).

Add 3, the 5’s and the 7’s to Kt.

‘Modal’ fragments as in § 5.4.

§ 5.6. System for dense, linear, non-ending, non-beginning 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 asis or will beand P asis or has been’. (F and P undefined, dff. G and H as in § 23.4).

RG: ├α → ├

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 Kt.

(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 Kt the axiom CGpPp (= CHpFp = CGGpp = CHHpp CpFFp = CpPPp).

§ 6.2. With change of sign, and antipodes neither past nor future.

Add to Kt 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 forIt is and always will beand H asIt 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: ├α → ├, ├ϒα

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 T-fragment 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. U-Calculi

§ 8. Basic U–T postulates

   U1. ETaNpNTap

   U2. ETaCpqCTapTaq

and for tense-logic

   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 first-order predicate calculus with identity.)

If and only if ha in the modal system determined by RL: ├α → ├and the axiom A1. CLCpqCLpLq, then ├Taα in the system determined by U1, U2, and U5.

If and only if ├α in Kt of § 4, then ├Taα in the system determined by U1, U2, U3, U4.

§ 9. Correspondences between U-calculi, modal logics, and tense-logics

(mostly suggested by Lemmon)

We write ‘γ ∼ β’ for ‘├α in the modal logic determined by RL, A1, and ├β, if and only if ├Taα in the U-calculus determined by U1, U2, U5, and ├γ’, or for ‘├α in the tense-logic determined by Kt+├β if and only if ├Taα in the U-calculus 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 (non-branching to right)

CKFpFqAAFKpq--FKpFqFKqFp

    9. CKUbaUcaAAIbcUbcUcb (non-branching 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 U-formula 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 tense-logical formula n is added to Kt, the modal or tense-logical formula m is deducible.)

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

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

  3. 3 entails 7.

  4. 5 entails 2, 6, 8.

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

  6. 7 is entailed by 3.

  7. 10 is entailed by 1, 12.

  8. 11 is entailed by 1, 12.

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

  10. 13 is entailed by 1, 2.

  11. (1+5) entails 3, 4.

  12. (3+4) entails 5.

  13. (1+6) entails 7.

§ 9.3. Correspondence of systems

(‘Condition n’ means the U-condition 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 (‘east-west’ circular time with antipodes)

∼ 12.

(p.181)