(original Polish notation) Arthur Prior, Formal Logic, Appendix 1: Postulate Sets for Logical Calcul

(original Polish notation) Arthur Prior, Formal Logic, Appendix 1: Postulate Sets for Logical Calculi

Contents
• 1. Classical Propositional Calculus: A–N, K–N, and D Systems
• 2. Classical Propositional Calculus: C–N Systems
• 3. Classical Propositional Calculus: C Fragment and C–0 Systems
• 4. Rules for Quantifiers
• 5. Classical Propositional Calculus: C–Π, C–δ–N, C–δ–0, C–δ, and C–δ–Π Systems
• 6. Modal Systems
• 7. Three-valued Systems
• 8. Intuitionist Propositional Calculus and Sub-systems
• 9. Classical Propositional Calculus: E, E–N, and E–J Fragments
• 10. Leśniewskian Systems
• 11. Formalized Syllogistic.
• 12. Formalized Arithmetic.
• 13. Logic of Assertion and Formalized Physics.

# 1. Classical Propositional Calculus: A–N, K–N, and D Systems

1.1. The system of Principia Mathematica (A–N) (1910).
• Axioms: (1) CAppp, (2) CqApq, (3) CApqAqp, (4) CApAqrAqApr, (5) CCqrCApqApr
• Definitions: (Df C) C:=AN, (Df K) Kpq:=NANpNq, (Df E) Epq:=KCpqCqp
• Rules: (1) Substitution, (2) Detachment (α, ANαβ→β)

1.2. Hilbert and Ackermann (A–N) (1928).
• Axioms: (1), (2), (3), (5), of 1.1, or same with (2) replaced by CpApq.
• Definitions and Rules as in 1.1.

1.3. Three-Axiom A–N System (Meredith, 1951).
• Axioms: (1) CAppp (cf. 1.1), (2) ApCpq, (3) CApqCCqrApr
• Definitions and Rules as in 1.1

1.4. Single-Axiom A–N System (Meredith, 1953).
• Axiom: CCCpqArAstCCspArAtp, or CCCpqArAstCCtsArAps, or CCCpqArAstCCrpAtAsp
• Definitions and Rules as in 1.1

1.5. K–N System (Sobociński, 1939).
• Axioms: (1) NKNKNprKNKNqrKNKpqr, (2) NKNpKpq, (3) NKNqKpKrq, (4) NKNKpqNNKpNNq
• Definitions: (Df C) Cpq:=NKpNq, (Df A) Apq:=NKNpNq, (Df E, as in 1.1) Epq:=KCpqCqp
• Rules: (1) Substitution, (2) Detachment (α, NKαNβ→β)

1.6. Single-Axiom Systems in D.
• Axiom: DDpDqrDDtDttDDsqDDpsDps (Nicod, 1918) or DDpDqrDDpDrpDDsqDDpsDps (Łukasiewicz, 1931)
• Definitions: (Df N) Np:=Dpp, (Df K) K:=ND, (Df C) Cpq:=DpNq, (Df A) Apq:=DNpNq
• Rules: (1) Substitution, (2) Detachment (α, DαDγβ→β)

# 2. Classical Propositional Calculus: C–N Systems

2.1. Łukasiewicz’s Standard C–N System (1929).
• Axioms: (1) CCpqCCqrCpr, (2) CCNppp, (3) CpCNpq
• Definitions: (Df A) A:=CN, (Df K) Kpq:=NCpNq, (Df E, as in 1.1) Epq:=KCpqCqp
• Rules: (1) Substitution, (2) Detachment (α, Cαβ→β)

2.2. Single-Axiom C–N System (Meredith, 1953).
• Axiom: CCCCCpqCNrNsrtCCtpCsp
• Definitions and Rules as in 2.1.

2.3. Axiomless C–N System (Suszko, 1948).
• Rules: (1) p,Cpq→q, (2) q→Cpq, (3) CCpqr→Cqr, (4) CpCqr→CCpqCpr, (5) Cpq→CCrpCCqsCrs, (6) CCpqr→CNPr, (7) Cpq,CNpq→q
• Definitions as in 2.1.

2.4. Trivially Axiomless Systems (Słupecki, 1949).
• To Rule (1) of 2.3 add any one of the following three sets:
    • (2) Ksp→p, (3) s→KsCCpqCCqrCpr, (4) s→KsCCNppp, (5) s→KsCpCNpq
    • (2)′ CCsqr→Cqr, (3)′ s→CCsCpqCCqrCpr, (4)′ s→CCsCNppp, (5)′ s→CCspCNpq
    • (2)″ s→CCspp, (3)″ CCpqr→Cqr, (4)″ Cpt→CCtqCCqrCpr, (5)″ Cpt→CCNppt, (6)″ Cpt→CpCNtq

As in 2.3, none of the initially given rules has a tautologous consequent. But by applying (2) to the result of applying (3)— (5)，or (2)′ to the result of applying (3)′—(5)′, or by deriving s→Cpp from (2)″ and (3)″ and combining this with (4)″—(6)″，the axioms of 2.1 are derivable from any arbitrary proposition s. Axiomless systems may be similarly constructed from any set of axioms.

# 3. Classical Propositional Calculus: C Fragment and C–0 Systems

3.1. Implicational Calculus (Tarski and Bernays, 1930).
• Axioms: (1) CCpqCCqrCpr, (2) CCCpqpp, (3) CpCqp
• Rules: Substitution and detachment as in 2.1.

3.2. Single-Axiom Implicational Calculus (Łukasiewicz, 1948)
• Axiom: CCCpqrCCrpCsp
• Rules as in 2.1.

3.3. Full Calculus in C and 0 (Wajsberg, 1937).
• Axioms: (1)–(3) as in 3.1, (4) C0p
• Definitions: (Df N) Np:= Cp0, (Df 1) 1:=N0, (Dff. A, K, E) as in 2.1.
• Rules as in 2.1.

3.4. Single-Axiom C–0 System (Meredith, 1953).
• Axiom: CCCCCpqCr0stCCtpCrp, or CCCpqCC0rsCCspCtCup
• Definitions and Rules as in 3.3.

# 4. Rules for Quantifiers

Where new types of variables are introduced, appropriate substitution rules are introduced along with them, and where there are quantifiers, substitutions must be made for free variables only, and only of variables which are not bound elsewhere in a formula. Of possible rules for introducing quantifiers, we list only those used in the text, which are so framed below as to allow for the appearance of ‘vacuous’ quantifications, i.e. expressions in which the variable bound by the quantifier either does not occur in the formula which follows, or is already bound in it (e.g. Πxρ, Πxφy, ΠxΣxφx). All such expressions may be proved equivalent to the corresponding expressions with the vacuous bindings omitted (ρ, φy, Σxφx). The rules are in all cases understood as adjoined to axioms, definitions, and rules for the propositional calculus; and the x occurring in the rule may be understood as a variable of any type, though the nature of the calculus will depend on the types of variables bound in it.

4.1. Π and Σ both undefined (Łukasiewicz).
• Π1: Cαβ → CΠxαβ
• Π2: Cαβ → CαΠxβ, for x not free in α
• Σ1: Cαβ → CΣxαβ, for x not free in β
• Σ2: Cαβ → CαΣxβ

4.2. With Π undefined.
• Definition: Df. Σ: Σx = NΠxN
• Rules: Π1, Π2, as in 4.1.

4.3. With Σ undefined.
• Definition: Df. Π: Πx = NΣxN
• Rules: Σ1, Σ2, as in 4.1.

# 5. Classical Propositional Calculus: C–Π, C–δ–N, C–δ–0, C–δ, and C–δ–Π Systems

5.1. The Theory of Implication (Russel’s term, 1906, for implicational calculus with quantifiers binding propositional variables, but without functorial variables).
• Axioms: As for implicational calculus (3.1 or 3.2)
• Definitions: (Df 0) 0:=Πpp, (Dff. N and 1) as in 3.3; (Dff. A, K, E) as in 2.1.
• Rules: Substitution; detachment as in 2.1; Π1, Π2, as in 4.1. (This system includes that of 3.3, since C0p is provable by applying Π1 to Cpp.)

5.2. C–N Calculus with Functorial Variables (Meredith, 1953).
• Axiom: CδpCδNpδq
• Definitions as in 2.1
• Rules: Substitution for both types of variables; detachment as in 2.1.

5.3. C–0 Calculus with Functorial Variables.
• Axiom: CδC00Cδ0δp (Łukasiewicz, 1951) or Cδδ0δp (Meredith, 1951)
• Definitions as in 3.3.
• Rules as in 5.2.

5.4. Implicational Fragment of Propositional Calculus with Functorial Variables (Meredith, 1951).
• Axiom: CδpCqδδq, or CpCδqδδp, or CδpδδCqq
• Rules as in 5.2.

5.5. Propositional Calculus with Functorial Variables and Quantifiers (Meredith, 1951).
• Axiom: As in 5.4; or CδδΠppδp
• Definitions: As in 5.1
• Rules: Substitution for both sorts of variable; detachment as in 2.1; Π1, Π2, as in 4.1.

# 6. Modal Systems

6.1. The Lewis (N–K–M) Systems (S3, 1918; others 1932; amended).
• (As the rules and definitions are the same in all these, we shall state them first)
• Definitions: (Df L) L:=NMN, (Df C′) C′pq:=NMKpNq, (Df E′) E′pq:=KC′pqC′qp
• Rules: (1) Substitution for propositional variables, (2) Adjunction (α,β→Kαβ), (3) Detachment (α,C′αβ→β), (4) Substitutability of strict equivalents
• Axioms for S1: (1) C′KpqKqp, (2) C′Kpqp, (3) C′pKpp, (4) C′KpKqrKqKpr, (5) C′KC′pqC′qrC′pr, (6) C′pMp
• Axioms for S2: (1)–(6) plus (7) C′MKpqMp
• Axioms for S3: (1)–(6) plus (8) C′C′pqC′mpMq
• Axioms for S4: (1)–(6) plus (9) C′MMpMp
• Axioms for S5: (1)–(6) plus (10) C′MpLMp
• Axioms for S6: (1)–(7), i.e. as for S2, plus (11) MMp
• Axioms for S7: (1)–(8), i.e. as for S3, plus (11) MMp
• Axioms for S8: (1)–(8), i.e. as for S3, plus (11) LMMp
• (Note: The Lewis systems are so framed that the unmodalized C and E do not occur in the axioms and rules; though they could be introduced by definition as in the K–N system 1.5. With these definitions, the full classical propositional calculus is provable in all the
systems.)

6.2. The Gõdel Systems (L undefined) (1933).
• (These are all understood as adjoined to some complete basis for the
classical propositional calculus, e.g. any from §1 or §2.)
• Definition: (Df M) M:=NLN
• Rule: α→Lα
• Axioms for Common Basis: (1) CLpp (2) CLCpqCLpLq
• Axioms for S4: (1) and (2), plus (3) CLpLLp
• Axioms for S5: (1) and (2), plus (4) CNLpLNLp
((1) and (2) alone, with the definition and rule, yield a system—Feys’s system T—equivalent to what we would obtain by adjoining the rule α→Lα to S2.)

6.3. The von Wright Systems (M undefined) (1951).
• (Again understood as adjoined to some complete basis for the classical propositional calculus)
• Definition: (Df L) L:=NMN
• Rules: (1) α→Lα, (2) Eαβ→EMαMβ
• Axioms for System M: (1) CpMp (2) EMApqAMpMq
• Axioms for System M′: (1) and (2), plus (3) CMMpMp
• Axioms for System M″: (1) and (2), plus (4) CMNMpNMp.
• (System M is equivalent to the system T of 6.2; M′ to S4; M″ to S5.)

6.4. Relations of the Lewis-von Wright Systems.
• (α→β means that in the system α we may prove whatever is provable in β, and more besides)
• S5 (M″) → S4 (M′); S8 → S7; S4 (M′) → T (M); S7 → S6; S7 → S3; S4 (M′) → S3; S6 → S2; S3 → S2; T (M) → S2; S2 → S1
• (T and S3 are independent; and T, S4, and S5 are inconsistent with S6–8.)

6.5. S5 without Added Axioms (Prior, 1953).
• Subjoin to the full classical propositional calculus the special rules (with L and M both undefined): (L1) Cαβ → CLαβ, (L2) Cαβ → CαLβ, if no propositional variable in β occurs unmodalized in α, (M1) Cαβ → CMαβ, if no propositional variable in α occurs unmodalized in β, (M2) Cαβ → CαMβ
• (p is modalized if and only if it is the whole or a part of a propositional formula prefixed by L or M)
• Or L1 and L2, with Df. M as in 6.2.
• Or M1 and M2, with Df. L as in 6.1.

6.6. The Ł-Modal System (Łukasiewicz, 1953).
(Understood as subjoined to 5.2, with M, L, etc., substitutable for δ as well as C, N, etc.; M undefined)
• Special Axiom: CφMp
• Axiomatic Rejections: (1) ∗CMpp, (2) ∗Mp
• Definition: Df. L as in 6.1
• Rules of Rejection: (1) Reject any formula with a rejected substitution, (2) ∗β, Cαβ → ∗α
• All formulae not provable are demonstrably rejected.

6.7. Alternative Basis for the Ł-Modal System (Prior, 1954).
• (Understood as subjoined to 5.2-with-rejection, i.e. with rules of rejection as in 6.6 and with the one axiomatic rejection ∗p. M, L, etc. substitutable for δ as well as C, N, etc.)
• Special Axiom: CδpCδCppδMp
• Definition: Df. L as in 6.1
• Special Rule: The substitutions M/′ and M/C″ may be performed in theses, provided that the same substitution is made throughout the formula.

# 7. Three-valued Systems

7.1. Wajsberg’s Axiomatization (1932) of the Three-valued Calculus in Łukasiewicz’s C and N.
• Matrices:
      C |  1   ½   0   |  N
      --+-------------+---
      1 |  1   ½   0   |  0
      ½ |  1   1   ½   |  ½
      0 |  1   1   1   |  1
• Axioms: (1) CCpqCCqrCpr, (2) CpCqp, (3) CCCpNppp, (4) CCNpNqCqp
• Definitions: (Df A) Apq := CCpqq, (Df K and E) as in 1.1; (Df M) Mp := CNpp
• Rules as in 2.1.
• This system is not strongly complete, but if we add the usual rules of rejection as in 6.6, and axiomatically reject CMpp (i.e. CCNppp) instead of the simple p, all formulae not provable are demonstrably rejected.

7.2. Słupecki’s Functionally and Strongly Complete Extension of Wajsberg’s System (1936).
• Matrices:
      C |  1   ½   0   |  N | T
      --+-------------+----+---
      1 |  1   ½   0   |  0 | ½
      ½ |  1   1   ½   |  ½ | ½
      0 |  1   1   1   |  1 | ½
• Axioms: (1)–(4) as in 7.1, (5) CTpNTp, (6) CNTpTp
• Definitions: (Df. (N)) (N)p := CTpNp, (Df. (C)) (C)pq := C(N)q(N)p
• Rules as in 2.1.
• (Axioms of the classical C–N system 2.1 provable for (C) and (N). Tzu-Hua Hoo, 1949.)


7.3. Słupecki’s Functionally and Strongly Complete System in C, N, and R (1946).
• Matrices:
      C |  1   ½   0   |  N | R
      --+-------------+----+---
      1 |  1   ½   0   |  0 | ½
      ½ |  1   1   1   |  ½ |  1
      0 |  1   1   1   |  1 |  0
• Axioms: (1)–(3) as in the classical C–N system 2.1, (4) CRpNp, (7) CRRpp, (5) CRCpqRq, (8) CpRRp, (6) CpCRqRCpq, (9) NRNp
• Rules as in 2.1.

# 8. Intuitionist Propositional Calculus and Sub-systems

8.1. Heyting’s Calculus of 1930 (Łukasiewicz’s Axioms, 1952).
• Axioms: (1) CpCqp, (2) CCpCqrCCpqCpr, (3) CKpqp, (4) CKpqq, (5) CpCqKpq, (6) CpApq, (7) CqApq, (8) CCprCCqrCApqr, (9) CCpNqCqNp, (10) CpCNpq
• Definitions: (Df. (C)) (C)pq := NKpNq
• Rules: Substitution and detachment as in 2.1.
• (The axioms and rules of the classical C–N system 2.1 are provable for (C) and N.)
• This system is not strongly complete; but Łukasiewicz has surmised
that if we have the usual axiomatic rejection *p, and add to the two
usual rules of rejection as stated in 6.6 the special rule (3) ∗α, ∗β → ∗Aαβ, then all formulae not provable are demonstrably rejected.

8.2. Johannsen’s Minimal Calculus of 1936 (Łukasiewicz’s Axioms).
• Axioms: (1)–(9) as in 8.1, or (1)–(8) as in 8.1, with (Df N) N:=Cpo
• Rules as in 2.1.

8.3. Kolmogorov’s Calculus (1925).
• Axioms: (1), (2), and (9) as in 8.1  or (1) and (2) as in 8.1, with Df. N: N = Cpo
• Rules as in 2.1.

8.4. Positive Logic.
• Axioms (Hilbert, 1928): (1) CCpCpqCpq, (2) CCqrCCpqCpr, (3) CCpCqrCqCpr, (4) CpCqp or (Łukasiewicz): (1) and (2) as in 7.1 or (Meredith, 1953): CCCpqrCsCqCrtCqt
• Rules as in 2.1.
• (With Df. N, or with (9) of 8.1, this gives 8.3.)

8.5. The Weak Positive Implicational Calculus (Church, 1951).
• Axioms: (1) CCpCpqCpq (cf. Hilbert, 8.4), (2) CCqrCCpqCpr (cf. Hilbert, 8.4), (3) CCpCqrCqCpr (cf. Hilbert, 8.4), (4) Cpp (contrast Hilbert, 8.4)
• Rules as in 2.1.
• (Note: In 8.2 and 8.3, or 8.4 with Df. N, CpCNpq is not provable, but CpCqp is. In 8.5, with or without Df. N, neither CpCNpq nor CpCqp is provable.)

# 9. Classical Propositional Calculus: E, E–N, and E–J Fragments

9.1. Two-axiom Equivalential Calculus (Leśniewski, 1929).
• Axioms: (1) EEpqEqp, (2) EEEpqrEpEqr
• Rules: (1) Substitution for propositional variables, (2) Detachment (α, Eαβ→β)

9.2. Single-Axiom Equivalential Calculus (Lukasiewicz, 1939).
• Axiom: EEpqEErqEpr, or EEpqEEprEErq, or EEpqEErpEEqr
• Rules as in 9.1.

9.3. Equivalential Calculus with Negation (Mihailescu, 1937).
• Axioms: (1) Any sufficient for E only, (2) EENpNqEpq
• Definition: (Df J) Jpq := EpNq (or NEpq)
• Rules as in 9.1.
• (Note: Though the pure E-calculi 9.1 and 9.2 are strongly complete, no E–N system can be so. In an E–N formula, either (i) no propositional variable occurs an odd number of times, and M does not occur an odd number of times; or (ii) at least one propositional variable occurs an odd nximber of times, or (iii) no propositional variable occurs an odd number of times, but N does. All E–N tautologies are of type (i), and all such are provable in 9.3; any formula of type (ii), if tried as an extra axiom, is disprovable by deriving the simple as a thesis; but those of type (iii) are neither provable nor thus disprovable. But if we axiomatically reject any one type (iii) formula, e.g. EpNp, and add the rules (1) Reject any formula with a rejected substitution, (2) ∗αβ, Eαβ → ∗β, then all formulae not provable, whether of type (ii) or type (iii), are demonstrably rejected.)

9.4. Equivalential Calculus with Exclusive Alternation (Mihăilescu, 1938).
• Axioms: (1) Any sufficient for E only, (2) EEJpqJrsEEpqErs
• Definition: (Df N) Np := EpJpp
• Rules as in 9.1.
• Metalogical remarks under 9.3 apply with N replaced by J.

9.5. Equivalential Calculus with Exclusive Alternation (Rasiowa, 1948).
• Axioms: (1) EEpqEErqEpr (cf. 9.2), (2) EEpqEJrqJpr
• Definition and Rules as in 9.4.

# 10. Leśniewskian Systems
(In these systems all variables in theses are bound，definitions are equivalences introduced by special rules; and these and the other rules will not be stated, but only the axioms and more important definitions. In 10.1 δ is a dyadic truth-operator-variable in the Axiom and monadic in Df. K; in 10.4, φ is a variable term-forming operator on terms.)

10.1. Protothetic (E undefined)
• Axiom: ΠpqEEpqΠδEδpδpΠuuΠrEδqrEqp (Sobociński, 1945)
• Definitions: (Df N) ΠpENpEpΠuu, (Df K) ΠpqEKpqΠδEpEδpδq (Tarski, 1923)

10.2. Ontology (ε undefined)
• (Understood as subjoined to protothetic)
• Axiom: ΠabEεabKKΠcCεcaεcbΣcεcaΠcdCKεcaεdaεcd (Leśniewski, 1920) or ΠabEεabΣcKεacεcb (Leśniewski, 1929)
• Definitions: (Df ex) ΠαEexaΣbεba, (Df ob) ΠαEobaΣbεab, (Df sol) ΠαEsolaΠbcCKεbaεcaεbc, (Df U) ΠabEUabΠcCεcaεcb, (Df ∧) ΠαEεa ∧ KεaaNεaa
• (Here ‘ex’ and ‘ob’ are the ∃! and E! of the text; ‘sol𝑎’， means ‘There is at most one 𝑎’, and U𝑎𝑏, ‘Every 𝑎 is a 𝑏’.)

10.3. Ontology (U undefined)
• Axiom: ΠabEUabΠcdCKNUcdUcaΣefKKKNUefUecUebΠghiCKKNUhiUgeUheUgh (Lejewski)
• Definitions: (Df ex) ΠαEexaΣbNUab, (Df sol) ΠαEsolaΠbcdCKKNUcdUbaUcaUbc, (Df ob) ΠaEobaKexasola, (Df ε) ΠabEεabKobaUab

10.4. Mereology (μ undefined)
• (Understood as subjoined to protothetic and ontology)
• Axiom: ΠabEεaμbKεbbΠφcKΠdEεdφcKΠeCεecεeμdΠeCεeμdΣfgKKεfcεgμeεgμfCKεbμbεbcεaμφc (Sobociński, 1949)
• Definition: (Df κ) ΠabEεaκbKKKεaaΣcεcbΠcCεcbεcμaΠcCεcμaΣdeKKεdbεeμdεeμc

# 11. Formalized Syllogistic

(All systems understood as subjoined to the full classical propositional calculus, with substitution for term-variables. U, Y, I, O for operators forming traditional A, E, I, O propositions.)

11.1. Aristotelian System admitting Empty Terms (Slupecki, 1946).
• Special Axioms:  (1) CUablab, (2) CIabIba, (3) CKUbcUabUac (Barbara), (4) CKUbcIabIac (Darii)
• Definitions: (Df Υ) Υ:=NI, (Df O) O:=NU
• Interpretations rendering Axioms provable within Ontology (10.2): (1) Uab = KΠcCεcαεcbΣcεcα, (2) Iab = ΣcKεcαεcb.
• (All Aristotelian laws but Uaa and Iaa provable.)

11.2. Brentano-Style System admitting Empty Terms.
• Special Axioms:  (1) Uaa, (2) CKUbcUabUac (Barbara), (3) CKUbcIbalac (Datisi)
• Definitions as in 11.1
• Interpretations rendering Axioms provable within Ontology: (1) Uab = ΠcCεcαεcb (cf. 10.2), (2) Iab = ΣcKεcαεcb (cf. 11.1)
• (Uaa provable, but not Iaa, nor laws of subalternation, contrariety, subcontrariety, conversion per accidens or syllogisms with ‘p’ in mood-name.)

11.3. System not admitting Empty Terms (Łukasiewicz, 1929. U and I
undefined).
• Special Axioms: (1) Uaa, (2) Iaa, (3) CKUbcUabUac (Barbara), (4) CKUbcIbalac (Datisi)
• Definitions as in 11.1.
• (No direct interpretation in ontology, but all Aristotelian laws provable.)

11.4. System not admitting Empty Terms (Bocheński, 1948. U and I undefined).
• Special Axioms: (1), (2), (3) as in 11.3, (4) CKYbcIabOac (Ferio)
• Definitions as in 11.1
• (Equivalent to system 11.3.)

11.5. System not admitting Empty Terms, but with Negative Terms (Thomas, 1949. U undefined; a′ for ‘non-a’).
• Special Axioms: (1), (2), and (4) of 11.4
• Definitions: (Df Y) Yab:=Uab′, (Df I) I:=NY, (Df O) O:=NU
• Special Rule: a″ and a are interchangeable.
• (All Aristotelian laws provable, together with obversion, contraposition, etc.)

11.6. System not admitting Empty Terms, but with Negative Terms (Wedberg, 1949. U undefined; a′ for ‘non-a’).
• Special Axioms: (1) Uaa″, (2) Ua″a, (3) CUabUb′a′, (4) CKUabUbcUac, (5) CUabNUab′
• Definitions as in 11.5
• No Special Rule for Negative Terms.
• (Equivalent to 11.5.)

11.7. System (Brentano style) admitting Empty Terms, and with Negative Terms (Wedberg, 1949).
• 11.6 with Axiom (5) replaced by CUaa′Uab

11.8. System not admitting Empty Terms, and without Negative Terms, but with Rejection (Łukasiewicz–Słupecki, 1951. U and I undefined).
• (Understood as subjoined to 2.1 with rules of rejection as in 6.6.
• In special rule below, U, Y, I, O forms are counted as elementary, and if α is a U, Y, I, or O form and β is elementary, Cαβ is elementary; and there are no other elementary forms.)
• Special Axioms, and Definitions, as in 11.3
• Special Axiomatic Rejection: ∗CKUcbUabIac
• Special Rule of Rejection: ∗Cαγ, ∗Cβγ → ∗CαCβγ, provided that α and β are Y or O forms and γ is elementary.
• (All formulae not provable are demonstrably rejected.)

# 12. Formalized Arithmetic

12.1. Theory of Natural Numbers (Łukasiewicz, 1950).
• (Understood as subjoined to the full classical propositional calculus and rules for quantifiers. The new variables a, b, c, etc., may be interpreted as standing for the integers from 1 upwards, the constant term 1 as the number, Sab as a + b, Iab as a = b, and Lab as a < b. 1 and S are undefined.)
• Special Axioms: (1) ISSabcSbSac, (2) CNL1aI1a, (3) CΠαCΠbCLbafbφαφα
• Definitions: (Df I) Iab:=ΠφCφaφb, (Df L) Lab:=ΣcISacb
• No special rules beyond new substitutions.

# 13. Logic of Assertion and Formalized Physics.

These systems are grouped together because of their structural resemblance. In 13.1 the variables x, y, etc., stand for persons, and Lxp is intended to be read as ‘x asserts that p’ (or perhaps more accurately as ‘x asserts that p, or in consistency ought to’), and Sp as ‘p is disputed’ (the system being consistent with ΣpSp). In 13.2 the variables t, t′, t″, etc., stand for instants; m, n, etc., for time-intervals; Utp is intended to be read as ‘It is the case that p at time t’; δtn as ‘The instant which is later than t by the interval n’; and ρtt′ as ‘t is the same instant as t′’. The system 2.1 is provable within all the systems (cf. 6.1).

13.1. Logic of Assertion (Łoś, 1948)
• Axioms: (1) LxCCpqCCqrCpr, (2) LxCCNppp, (3) LxCpCNpq, (4) EŁxNpNLxp, (5) CLxCpqCLxpLxq, (6) CΠxLxpp, (7) ELxLxpLxp
• Definitions: Dff. A, K, E as in 2.1. (Df S) Sp:=ΣxyKLxpLyNp
• Rules: Substitution for each type of variable.
• Detachment as in 2.1.
• Rules for quantifiers, with α → Πxα given or provable.

13.2. Formalized Physics with the Clock Axiom (Łoś, 1949).
• Axioms: (1) UtCCpqCCqrCpr, (2) UtCCNppp, (3) UtCpCNpq, (4) EUtNpNUtp, (5) CUtCpqCUtpUtq, (6) CΠtUtpp, (7) Σt′ρδtnt′, (8) Σt′ρδt′nt, (9) ΣpΠt′EUt′pρtt′
• Definitions: Dff. A, K, E as in 2.1. (Df ρ) ρtt′:=ΠpEUtpUt′p
• Rules as in 13.1.

13.3. Formalized Physics with the Axiom of Causality (Łoś, 1949).
• 13.2 with Axiom (9) replaced by ΣqEUδtnpUtq