Friday, September 26, 2025

Postulate Sets for Logical Calculi

This blog post is a translation from Polish notation into modern notation of Appendix 1, “Postulate Sets for Logical Calculi”, from Arthur Prior’s Formal Logic. It contains a wealth of axiom systems from different sources, many of which are little known today. Since Prior gave citations of the literature where he found these systems, the post also transcribes Prior’s Appendix 2, “Select Bibliography”, though making it a new numbered section within the text.

To do this, I first transcribed the appendix (see plaintext transcription here) and then translated. Any inaccuracies are my fault.

Although this blog can display LaTeX formulas, I have decided that, since the main use of having this resource is to easily copy and paste the axioms, using Unicode symbols was preferable. However, I have kept Prior’s references between sections, in case something is off with those.

Noteworthy is the inclusion of C.I. Lewis’s modal systems S1 through S8 (apparently S6 is due to Alban and S7–S8 to Halldén, per SEP). Prior’s rendering is different from the one found, as of now, in John D. Cook’s blog and in the SEP article by Roberta Ballarin, and is more accurate. Cook and Ballarin had apparently looked at the appendix 2 to Lewis and Langford’s Symbolic Logic and copied the axioms named there as part of the systems; in addition to this, Cook silently changed the strict implication (⥽) to material implication (→). This method of transcription was faulty, since the axiom list as given by Lewis and Langford’s appendix doesn’t capture how they used the symbols in the actual body text. Their appendix itself says that S1 “contains all the theorems of Sections 1–4 in Chapter VI”, which should have made Cook and Ballarin pause, since theorem 18.4, within section 4 of chapter VI (page 163), is the formula ⌜p ⥽ ◇p⌝, which is given by Prior as the sixth axiom of S1. “Materialized”, this is ⌜p → ◇p⌝, a form of what is now known as the Axiom T of modal logic (sometimes written, equivalently, as ⌜□p → p⌝). The Cook/Ballarin version of S1, especially after Cook’s materialization of the implications, has no modal operators at all, which I did think was strange (isn’t S1 a system of modal logic?), but only thought to question after seeing Prior’s transcription of the Lewis–Langford S-systems. Prior also gives Modus Ponens as an inference rule rather than an axiom (as Lewis and Langford had given it), which is now the custom.

Neither Symbolic Logic nor Prior’s rendering mention axiom K or the rule of Necessitation being added to either S4 or S5, but it is widely held (as in the SEP article) that both had both, so I’m not sure what’s going on with that. Were K and Necessitation even originally part of Lewis’s systems, or were they only added by other authors later?

1. Classical Propositional Calculus: ∨–¬, ∧–¬, and ↑ Systems

1.1. The system of Principia Mathematica (∨–¬) (1910).

Axioms

  • (1) (p ∨ p) → p
  • (2) q → (p ∨ q)
  • (3) (p ∨ q) → (q ∨ p)
  • (4) (p ∨ (q ∨ r)) → (q ∨ (p ∨ r))
  • (5) (q → r) → ((p ∨ q) → (p ∨ r))

Definitions

  • (Df →) p → q ≝ (¬p ∨ q)
  • (Df ∧) p ∧ q ≝ ¬(¬p ∨ ¬q)
  • (Df ↔) p ↔ q ≝ (p → q) ∧ (q → p)

Rules

  • (1) Substitution
  • (2) Detachment (α, (¬α ∨ β)⊢β)

1.2. Hilbert and Ackermann (∨–¬) (1928).

Axioms

  • (1), (2), (3), (5), of 1.1, or
  • Same with (2) replaced by p → (p ∨ q).

Definitions and Rules as in 1.1.

1.3. Three-Axiom ∨–¬ System (Meredith, 1951).

Axioms

  • (1) (p ∨ p) → p (cf. 1.1)
  • (2) p ∨ (p → q)
  • (3) (p ∨ q) → ((q → r) → (p ∨ r))

Definitions and Rules as in 1.1.

1.4. Single-Axiom ∨–¬ System (Meredith, 1953).

Axiom

  • ((p → q) → (r ∨ (s ∨ t))) → ((s → p) → (r ∨ (t ∨ p))), or
  • ((p → q) → (r ∨ (s ∨ t))) → ((t → s) → (r ∨ (p ∨ s))), or
  • ((p → q) → (r ∨ (s ∨ t))) → ((r → p) → (t ∨ (s ∨ p)))

Definitions and Rules as in 1.1.

1.5. ∧–¬ System (Sobociński, 1939).

Axioms

  • (1) ¬((¬((¬p) ∧ r)) ∧ (¬((¬q) ∧ r) ∧ ((¬(p ∧ q)) ∧ r)))
  • (2) ¬((¬p) ∧ (p ∧ q))
  • (3) ¬((¬q) ∧ (p ∧ (r ∧ q))), (4) ¬((¬(p ∧ q)) ∧ (¬(¬(p ∧ (¬(¬q))))))

Definitions

  • (Df →) p → q ≝ ¬(p ∧ ¬q)
  • (Df ∨) p ∨ q ≝ ¬(¬p ∧ ¬q)
  • Df. ↔ as in 1.1.

Rules

  • (1) Substitution
  • (2) Detachment (α, ¬(α ∧ ¬β)⊢β)

1.6. Single-Axiom Systems in ↑.

Axiom

  • ((p ↑ (q ↑ r)) ↑ ((t ↑ (t ↑ t)) ↑ ((s ↑ q) ↑ ((p ↑ s) ↑ (p ↑ s))))) (Nicod, 1918) or
  • (p ↑ (q ↑ r)) ↑ ((p ↑ (r ↑ p)) ↑ ((s ↑ q) ↑ ((p ↑ s) ↑ (p ↑ s)))) (Łukasiewicz, 1931).

Definitions

  • (Df ¬) ¬p ≝ (p ↑ p)
  • (Df ∧) p ∧ q ≝ ¬(p ↑ q)
  • (Df →) p → q ≝ p ↑ (¬q)
  • (Df ∨) p ∨ q ≝ (¬p) ↑ (¬q)

Rules

  • (1) Substitution
  • (2) Detachment (α, (α ↑ (γ ↑ β))⊢β)

2. Classical Propositional Calculus: →–¬ Systems

2.1. Łukasiewicz’s Standard →–¬ System (1929).

Axioms

  • (1) (p → q) → ((q → r) → (p → r))
  • (2) ((¬p → p) → p)
  • (3) p → (¬p → q)

Definitions

  • (Df ∨) p ∨ q ≝ (¬p → q)
  • (Df ∧) p ∧ q ≝ ¬(p → ¬q)
  • Df. ↔ as in 1.1.

Rules

  • (1) Substitution,
  • (2) Detachment (α, α → β ⊢ β)

2.2. Single-Axiom →–¬ System (Meredith, 1953).

Axiom

  • ((((p → q) → (¬r → ¬s)) → r) → t) → ((t → p) → (s → p)).

Definitions and Rules as in 2.1.

2.3. Axiomless →–¬ System (Suszko, 1948).

Rules

  • (1) p, p → q ⊢ q
  • (2) q ⊢ p → q
  • (3) ((p → q) → r) ⊢ (q → r)
  • (4) (p → (q → r)) ⊢ ((p → q) → (p → r))
  • (5) (p → q) ⊢ ((r → p) → ((q → s) → (r → s)))
  • (6) ((p → q) → r) ⊢ (¬p → r)
  • (7) p → q, ¬p → q ⊢ 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

Set 1:

  • (2) s ∧ p ⊢ p
  • (3) s ⊢ s ∧ ((p → q) → ((q → r) → (p → r)))
  • (4) s ⊢ s ∧ ((¬p → p) → p)
  • (5) s ⊢ s ∧ (p → (¬p → q))

Set 2:

  • (2)′ ((s → q) → r) ⊢ (q → r)
  • (3)′ s ⊢ (s → (p → q)) → ((q → r) → (p → r))
  • (4)′ s ⊢ (s → (¬p → p)) → p
  • (5)′ s ⊢ (s → p) → (¬p → q)

Set 3:

  • (2)″ s ⊢ (s → p) → p
  • (3)″ ((p → q) → r) ⊢ (q → r)
  • (4)″ (p → t) ⊢ (t → q) → ((q → r) → (p → r))
  • (5)″ (p → t) ⊢ ((¬p → p) → t)
  • (6)″ (p → t) ⊢ p → (¬t → q)

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 ⊢ p → p 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: → Fragment and →–⊥ Systems

3.1. Implicational Calculus (Tarski and Bernays, 1930).

Axioms

  • (1) (p→q)→((q→r)→(p→r))
  • (2) (((p→q)→p)→p)
  • (3) p→(q→p)

Rules

Substitution and detachment as in 2.1.

3.2. Single-Axiom Implicational Calculus (Łukasiewicz, 1948)

Axiom

  • ((p→q)→r)→((r→p)→(s→p))

Rules as in 2.1.

3.3. Full Calculus in → and ⊥ (Wajsberg, 1937).

Axioms

  • (1)–(3) as in 3.1
  • (4) ⊥→p

Definitions

  • (Df ¬) ¬p ≝ (p→⊥)
  • (Df ⊤) ⊤ ≝ ¬⊥, (Dff. ∨, ∧, ↔) as in 2.1.

Rules as in 2.1.

3.4. Single-Axiom →–⊥ System (Meredith, 1953).

Axiom

  • (((((p→q)→(r→⊥))→s)→t)→((t→p)→(r→p))), or
  • (((p→q)→((⊥→r)→s))→((s→p)→(t→(u→p))))

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: (α → β) ⊢ ((∀x α) → β)
  • ∀2: (α → β) ⊢ (α → ∀x β), for x not free in α
  • ∃1: (α → β) ⊢ ((∃x α) → β), for x not free in β
  • ∃2: (α → β) ⊢ (α → ∃x β)

4.2. With ∀ undefined.

Definition

  • (Df ∃) ∃x φ ≝ ¬∀x ¬φ

Rules

  • ∀1, ∀2, as in 4.1.

4.3. With ∃ undefined.

Definition

  • (Df ∀) ∀x φ ≝ ¬∃x ¬φ

Rules

  • ∃1, ∃2, as in 4.1.

5. Classical Propositional Calculus: →–∀, →–δ–¬, →–δ–⊥, →–δ, and →–δ–∀ 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 ⊥) ⊥ ≝ ∀p(p), (Dff. ¬ and 1) as in 3.3
  • (Dff. ∨, ∧, ↔) 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 ⊥ → p is provable by applying ∀1 to p → p.)

5.2. →–¬ Calculus with Functorial Variables (Meredith, 1953).

Axiom

  • δ(p) → (δ(¬p) → δ(q))

Definitions as in 2.1

Rules

  • Substitution for both types of variables
  • Detachment as in 2.1.

5.3. →–⊥ Calculus with Functorial Variables.

Axiom

  • δ(⊥ → ⊥) → (δ(⊥) → δ(p)) (Łukasiewicz, 1951) or δ(δ(⊥)) → δ(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

  • δ(p) → (q → δ(δ(q))), or
  • p → (δ(q) → δ(δ(p))), or δ(p) → δ(δ(q → q))

Rules as in 5.2.

5.5. Propositional Calculus with Functorial Variables and Quantifiers (Meredith, 1951).

Axiom

  • As in 5.4; or
  • δ(δ(∀p(p))) → δ(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 (¬–∧–◇) Systems (S3, 1918; others 1932; amended).

(As the rules and definitions are the same in all these, we shall state them first.)

Definitions

  • (Df □) □φ ≝ ¬◇¬φ
  • (Df ⥽) p ⥽ q ≝ ¬◇(p ∧ ¬q)
  • (Df ≍) p ≍ q ≝ (p ⥽ q) ∧ (q ⥽ p)

Rules

  • (1) Substitution for propositional variables
  • (2) Adjunction (from α, β ⊢ α ∧ β)
  • (3) Detachment (from α, α ⥽ β ⊢ β)
  • (4) Substitutability of strict equivalents

Axioms for S1

  • (1) (p ∧ q) ⥽ (q ∧ p)
  • (2) (p ∧ q) ⥽ p
  • (3) p ⥽ (p ∧ p)
  • (4) (p ∧ (q ∧ r)) ⥽ (q ∧ (p ∧ r))
  • (5) ((p ⥽ q) ∧ (q ⥽ r)) ⥽ (p ⥽ r)
  • (6) p ⥽ ◇p

Axioms for S2

  • (1)–(6), plus
  • (7) ◇(p ∧ q) ⥽ ◇p

Axioms for S3

  • (1)–(6), plus
  • (8) (p ⥽ q) ⥽ (◇p ⥽ ◇q)

Axioms for S4

  • (1)–(6), plus
  • (9) ◇◇p ⥽ ◇p

Axioms for S5

  • (1)–(6), plus
  • (10) ◇p ⥽ □◇p

Axioms for S6

  • (1)–(7), i.e. as for S2, plus
  • (11) ◇◇p

Axioms for S7

  • (1)–(8), i.e. as for S3, plus
  • (11) ◇◇p

Axioms for S8

  • (1)–(8), i.e. as for S3, plus
  • (11) □◇◇p

(Note: The Lewis systems are so framed that the unmodalized → and ↔ do not occur in the axioms and rules; though they could be introduced by definition as in the ∧–¬ system 1.5. With these definitions, the full classical propositional calculus is provable in all the systems.)

6.2. The Gödel Systems (□ 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 ◇) ◇φ ≝ ¬□¬φ

Rule

From ⊢ α infer ⊢ □α.

Axioms for Common Basis

  • (1) □p → p
  • (2) □(p → q) → (□p → □q)

Axioms for S4

  • (1) and (2), plus
  • (3) □p → □□p

Axioms for S5

  • (1) and (2), plus
  • (4) ¬□p → □¬□p

((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 “from ⊢ α infer ⊢ □α” to S2.)

6.3. The von Wright Systems (◇ undefined) (1951).

(Again understood as adjoined to some complete basis for the classical propositional calculus.)

Definition

  • (Df □) □φ ≝ ¬◇¬φ

Rules

  • (1) From ⊢ α infer ⊢ □α
  • (2) From α ↔ β infer ◇α ↔ ◇β

Axioms for System M

  • (1) p → ◇p
  • (2) ◇(p ∨ q) ↔ (◇p ∨ ◇q)

Axioms for System M′

  • (1) and (2), plus
  • (3) ◇◇p → ◇p

Axioms for System M″

  • (1) and (2), plus
  • (4) ◇¬◇p → ¬◇p

(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 □ and ◇ both undefined)

  • (L1) from ⊢ α → β infer ⊢ □α → β
  • (L2) from ⊢ α → β infer ⊢ α → □β, if no propositional variable in β occurs unmodalized in α
  • (M1) from ⊢ α → β infer ⊢ ◇α → β, if no propositional variable in α occurs unmodalized in β
  • (M2) from ⊢ α → β infer ⊢ α → ◇β.

(p is modalized if and only if it is the whole or a part of a propositional formula prefixed by □ or ◇)

  • Or L1 and L2, with Df. ◇ as in 6.2.
  • Or M1 and M2, with Df. □ as in 6.1.

6.6. The Ł-Modal System (Łukasiewicz, 1953).

(Understood as subjoined to 5.2, with ◇, □, etc., substitutable for δ(·) as well as →, ¬, etc.; ◇ undefined)

Special Axiom

  • φ → ◇p

Axiomatic Rejections

  • (1) ∗(◇p → p)
  • (2) ∗◇p

Definition

  • Df. □ as in 6.1

Rules of Rejection

  • (1) Reject any formula with a rejected substitution
  • (2) from ∗β and ⊢ α → β infer ∗α

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. ◇, □, etc. substitutable for δ(·) as well as →, ¬, etc.)

Special Axiom

  • δ(p) → (δ(p → p) → δ(◇p))

Definition

  • Df. □ as in 6.1

Special Rule

  • The substitutions ◇/¬ and ◇/→ 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 → and ¬.

Matrices

  → |  1   ½   0   |  ¬
  --+-------------+---
  1 |  1   ½   0   |  0
  ½ |  1   1   ½   |  ½
  0 |  1   1   1   |  1

Axioms

  • (1) ((p → q) → ((q → r) → (p → r)))
  • (2) (p → (q → p))
  • (3) (((p → ¬p) → p) → p)
  • (4) ((¬p → ¬q) → (q → p))

Definitions

  • (Df ∨) p ∨ q ≝ ((p → q) → q)
  • Dff. ∧ and ↔ as in 1.1.
  • (Df M) M p ≝ (¬p → p)

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 (M p → p) (i.e. ((¬p → p) → p)) 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

  → |  1   ½   0   |  ¬ | T
  --+-------------+----+---
  1 |  1   ½   0   |  0 | ½
  ½ |  1   1   ½   |  ½ | ½
  0 |  1   1   1   |  1 | ½

Axioms

  • (1)–(4) as in 7.1
  • (5) (T p → ¬(T p))
  • (6) (¬(T p) → T p)

Definitions

  • (Df. (¬)) (¬)p ≝ (Tp → ¬p)
  • (Df. (→)) (→)pq ≝ ((¬)q → (¬)p)

Rules as in 2.1.

(Axioms of the classical →–¬ system 2.1 provable for (→) and (¬). Tzu-Hua Hoo, 1949.)

7.3. Słupecki’s Functionally and Strongly Complete System in →, ¬, and R (1946).

Matrices

  → |  1   ½   0   |  ¬ | R
  --+-------------+----+---
  1 |  1   ½   0   |  0 | ½
  ½ |  1   1   1   |  ½ |  1
  0 |  1   1   1   |  1 |  0

Axioms

  • (1)–(3) as in the classical →–¬ system 2.1
  • (4) (Rp → ¬p)
  • (5) (R(p → q) → Rq)
  • (6) (p → (Rq → R(p → q)))
  • (7) (RRp → p)
  • (8) (p → RRp)
  • (9) ¬R¬p

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) p → (q → p)
  • (2) (p → (q → r)) → ((p → q) → (p → r))
  • (3) (p ∧ q) → p
  • (4) (p ∧ q) → q
  • (5) p → (q → (p ∧ q))
  • (6) p → (p ∨ q)
  • (7) q → (p ∨ q)
  • (8) (p → r) → ((q → r) → ((p ∨ q) → r))
  • (9) (p → ¬q) → (q → ¬p)
  • (10) p → (¬p → q)

Definitions

  • (Df. (→)) (→)pq ≝ ¬(p ∧ ¬q)

Rules

  • Substitution and detachment as in 2.1.

(The axioms and rules of the classical →–¬ system 2.1 are provable for (C) and ¬.)

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 ¬) ¬p ≝ p → ⊥

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. ¬: ¬p ≝ p → ⊥

Rules as in 2.1.

8.4. Positive Logic.

Axioms (Hilbert, 1928)

  • (1) ((p → (p → q)) → (p → q))
  • (2) (q → r) → ((p → q) → (p → r))
  • (3) (p → (q → r)) → (q → (p → r))
  • (4) p → (q → p)

Or (Łukasiewicz):

  • (1) and (2) as in 7.1

Or (Meredith, 1953):

  • (((p → q) → r) → (s → ((q → (r → t)) → (q → t))))

Rules as in 2.1.

(With Df. ¬, or with (9) of 8.1, this gives 8.3.)

8.5. The Weak Positive Implicational Calculus (Church, 1951).

Axioms

  • (1) ((p → (p → q)) → (p → q)) (cf. Hilbert, 8.4)
  • (2) (q → r) → ((p → q) → (p → r)) (cf. Hilbert, 8.4)
  • (3) (p → (q → r)) → (q → (p → r)) (cf. Hilbert, 8.4)
  • (4) p → p (contrast Hilbert, 8.4)
  • Rules as in 2.1.

(Note: In 8.2 and 8.3, or 8.4 with Df. ¬, p → (¬p → q) is not provable, but p → (q → p) is. In 8.5, with or without Df. ¬, neither p → (¬p → q) nor p → (q → p) is provable.)

9. Classical Propositional Calculus: ↔, ↔–¬, and ↔–⊕ Fragments

9.1. Two-axiom Equivalential Calculus (Leśniewski, 1929).

Axioms

  • (1) (p ↔ q) ↔ (q ↔ p)
  • (2) ((p ↔ q) ↔ r) ↔ (p ↔ (q ↔ r))

Rules

  • (1) Substitution for propositional variables
  • (2) Detachment (α, (α ↔ β) ⊢ β)

9.2. Single-Axiom Equivalential Calculus (Lukasiewicz, 1939).

Axiom

  • (p ↔ q) ↔ ((r ↔ q) ↔ (p ↔ r)), or
  • (p ↔ q) ↔ ((p ↔ r) ↔ (r ↔ q)), or
  • (p ↔ q) ↔ ((r ↔ p) ↔ (q ↔ r))

Rules as in 9.1.

9.3. Equivalential Calculus with Negation (Mihailescu, 1937).

Axioms

  • (1) Any sufficient for ↔ only
  • (2) (¬p ↔ ¬q) ↔ (p ↔ q)

Definition

  • (Df ⊕) p ⊕ q ≝ (p ↔ ¬q) (or ¬(p ↔ q))
  • Rules as in 9.1.

(Note: Though the pure ↔-calculi 9.1 and 9.2 are strongly complete, no ↔–¬ system can be so. In an ↔–¬ 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 ¬ does. All ↔–¬ 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. (p ↔ ¬p), and add the rules (1) Reject any formula with a rejected substitution, (2) ∗αβ, (α ↔ β) ⊢ ∗β, 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 ↔ only
  • (2) ((p ⊕ q) ↔ (r ⊕ s)) ↔ ((p ↔ q) ↔ (r ↔ s))

Definition

  • (Df ¬) ¬p ≝ (p ↔ (p ⊕ p))

Rules as in 9.1.

Metalogical remarks under 9.3 apply with ¬ replaced by ⊕.

9.5. Equivalential Calculus with Exclusive Alternation (Rasiowa, 1948).

Axioms

  • (1) (p ↔ q) ↔ ((r ↔ q) ↔ (p ↔ r)) (cf. 9.2)
  • (2) (p ↔ q) ↔ ((r ⊕ q) ↔ (p ⊕ r))

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 (↔ undefined)

Axiom

  • ∀p∀q[(p↔q)↔∀δ(δ(p,p)↔((∀u(u))∧∀r(δ(q,r)↔(q↔p))))] (Sobociński, 1945)

Definitions

  • (Df N) ∀p [¬p↔(p↔(∀u(u)))], (Df K) ∀p∀q[p∧q↔∀δ(p↔(δ(p)↔δ(q)))] (Tarski, 1923)

10.2. Ontology (ε undefined)

(Understood as subjoined to protothetic)

Axiom

  • ∀ab [ εab ↔ ((∀c (εca → εcb)) ∧ (∃c εca) ∧ (∀cd ((εca ∧ εda) → εcd))) ] (Leśniewski, 1920) or
  • ∀ab [ εab ↔ ∃c (εac ∧ εcb) ] (Leśniewski, 1929)

Definitions

  • (Df ex) ∀a [ ex a ↔ ∃b εba ]
  • (Df ob) ∀a [ ob a ↔ ∃b εab ]
  • (Df sol) ∀a [ sol a ↔ ∀b c ((εba ∧ εca) → εbc) ]
  • (Df U) ∀ab [ Uab ↔ ∀c (εca → εcb) ]
  • (Df Λ) ∀a [ εaΛ ↔ (εaa ∧ ¬εaa) ]

(Here ‘ex’ and ‘ob’ are the ∃! and E! of the text; ‘sol a’ means ‘There is at most one a’, and Uab, ‘Every a is a b’.)

10.3. Ontology (U undefined)

Axiom

  • ∀ab[Uab↔∀cd(((¬Ucd)∧Uca)→∃ef((((¬Uef)∧Uec)∧Ueb)∧∀ghi((((¬Uhi)∧Uge)∧Uhe)→Ugh)))] (Lejewski)

Definitions

  • (Df ex) ∀a [ ex a ↔ ∃b ¬Uab ]
  • (Df sol) ∀a [ sol a ↔ ∀bcd ( ((¬Ucd ∧ Uba) ∧ Uca) → Ubc) ]
  • (Df ob) ∀a [ ob a ↔ (ex a ∧ sol a) ]
  • (Df ε) ∀a b [ εab ↔ (ob a ∧ Uab) ]

10.4. Mereology (μ undefined)

(Understood as subjoined to protothetic and ontology)

Axiom

  • ∀a∀b[ε(a,μb)↔(ε(b,b)∧∀φ∀c(∀d[ε(d,φc)↔(∀e(ε(e,c)→ε(e,μd))∧∀e(ε(e,μd)→∃f∃g(((ε(f,c)∧ε(g,μe))∧ε(g,μf))∧((ε(b,μb)∧ε(b,c))→ε(a,μ(φc))))))])))] (Sobociński, 1949)

Definition

  • (Df κ) ∀a∀b[ε(a,κb)↔((ε(a,a)∧∃c(ε(c,b)))∧(∀c(ε(c,b)→ε(c,μa))∧∀c(ε(c,μa)→∃d∃e((ε(d,b)∧ε(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) Uab → Iab
  • (2) Iab → Iba
  • (3) (Ubc ∧ Uab) → Uac (Barbara)
  • (4) (Ubc ∧ Iab) → Iac (Darii)

Definitions

  • (Df Y) Y ≝ ¬I
  • (Df O) O ≝ ¬U

Interpretations rendering Axioms provable within Ontology (10.2)

  • (1) Uab = ((∀c (c ∈ α → c ∈ b)) ∧ (∃c c ∈ α))
  • (2) Iab = ∃c (c ∈ α ∧ c ∈ b).

(All Aristotelian laws but Uaa and Iaa provable.)

11.2. Brentano-Style System admitting Empty Terms.

Special Axioms

  • (1) Uaa
  • (2) (Ubc ∧ Uab) → Uac (Barbara)
  • (3) (Ubc ∧ Iba) → Iac (Datisi)

Definitions as in 11.1

Interpretations rendering Axioms provable within Ontology

  • (1) Uab = ∀c (c ∈ α → c ∈ b) (cf. 10.2)
  • (2) Iab = ∃c (c ∈ α ∧ c ∈ b) (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) (Ubc ∧ Uab) → Uac (Barbara)
  • (4) (Ubc ∧ Iba) → Iac (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) (Ybc ∧ Iab) → Oac (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 ≝ Ua b′
  • (Df I) I ≝ ¬Y
  • (Df O) O ≝ ¬U

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) Uab → Ub′a′
  • (4) (Uab ∧ Ubc) → Uac
  • (5) Uab → ¬Uab′

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

  • Uaa′ → 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, (α → β) is elementary; and there are no other elementary forms.)

Special Axioms, and Definitions, as in 11.3

Special Axiomatic Rejection

  • ∗((Ucb ∧ Uab) → Iac)

Special Rule of Rejection

  • ∗(α → γ), ∗(β → γ) ⊢ ∗(α → (β → γ)), 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. 1 and + are undefined.)

Special Axioms

  • (1) ((a + b) + c) = (b + (a + c))
  • (2) ¬(1 < a) → (1 = a)
  • (3) (∀a ((∀b (b < a → (φ(b) → φ(a))) → φ(a))) → ∀a φ(a))

Definitions

  • (Df I) a = b ≝ ∀φ (φ(a) → φ(b))
  • (Df L) a < b ≝ ∃c (a + c = b)

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 ∃p Sp). 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) Lx((p → q) → ((q → r) → (p → r)))
  • (2) Lx((¬p → p) → p)
  • (3) Lx(p → (¬p → q))
  • (4) (Łx¬p) ↔ ¬Lxp
  • (5) (Lx(p → q) → (Lxp → Lxq))
  • (6) ∀x(Lxp) → p
  • (7) (LxLxp) ↔ Lxp

Definitions

  • Dff. ∨, ∧, ↔ as in 2.1.
  • (Df S) Sp ≝ ∃x∃y(Lxp ∧ Ly¬p)

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) Ut((p → q) → ((q → r) → (p → r)))
  • (2) Ut((¬p → p) → p)
  • (3) Ut(p → (¬p → q))
  • (4) (Ut¬p) ↔ ¬Utp
  • (5) (Ut(p → q) → (Utp → Utq))
  • (6) ∀t(Utp) → p
  • (7) ∃t′(ρδtnt′)
  • (8) ∃t′(ρδt′nt)
  • (9) ∃p∀t′(Ut′p ↔ ρtt′)

Definitions

  • Dff. ∨, ∧, ↔ as in 2.1.
  • (Df ρ) ρtt′ ≝ ∀p (Utp ↔ Ut′p)

Rules as in 13.1.

13.3. Formalized Physics with the Axiom of Causality (Łoś, 1949).

13.2 with Axiom (9) replaced by

  • ∃q (Uδtn p ↔ Utq)

14. Prior’s Bibliography

The following abbreviations are used for periodicals:

  • JSL for The Journal of Symbolic Logic, published for the Association for Symbolic Logic.
  • JCS for The Journal of Computing Systems, published by the Institute of Applied Logic, 3101 E. 42nd St., Minneapolis 6, Minn., U.S.A.
  • RPL for Revue philosophique de Louvain (Éditions de L’Institut Supérieure de Philosophie, Louvain).

Ajdukiewicz, Kasimierz (1890— )

  1. ‘On the Notion of Existence’, Studia Philosophica, iv (Poznań, 1951), pp. 8 ff.
    See Lejewski, Łukasiewicz 7, Quine 5.

Aristotle (384–321 B.C.)

  1. The Works of Aristotle Translated into English, vol. i (Oxford University Press, 1928).
  2. Aristotle’s Prior and Posterior Analytics: A Revised Text with Introduction and Commentary by W. D. Ross (Clarendon Press, 1949). The notes contain useful elucidations and tabulations of Aristotle’s arguments; see, for example, the notes to An. Pr. i. 46, ii. 2–7, 22, 23.

Barcan, Ruth (Mrs. J. A. Marcus) (1921— )

  1. ‘A Functional Calculus of First Order Based on Strict Implication’, JSL, xi (1946), pp. 1–16.
  2. ‘The Identity of Individuals in a Strict Functional Calculus of the Second Order’, ibid., xii (1947), pp. 12–15.

Bennett, Jonathan Francis (1930— )

  1. ‘Meaning and Implication’, Mind, 1954, pp. 451–63.

Bocheński, Innocentius M. (1902— )

  1. La Logique de Théophraste (Librairie de l’Université de Fribourg en Suisse, 1947).
  2. ‘On the Categorical Syllogism’, Dominican Studies, i (1948), pp. 35–37. See also Thomas 2.
  3. ‘On the Syntactical Categories’, The New Scholasticism, 1949, pp. 257–80. See also 4.
  4. ‘Logical Remarks on A-Sentences’, Dominican Studies, ii (1949), pp. 249–54. A comment on Thomas 1.
  5. Précis de logique mathématique (F. G. Kroonder, Bussum, Holland, 1949).
  6. Ancient Formal Logic (North-Holland Publishing Co., Amsterdam, 1951). See also Petrus Hispanus.

Boehner, Philotheus (1901— )

  1. Medieval Logic: An Outline of its Development from 1250 to c. 1400 (Manchester University Press, 1952).
    See also Burleigh, Ockham, Thomas 5.

Boethius, Anicius Manlius Severinus (455–526)

  1. Opera Omnia, Tomus Posterior; being vol. 64 of J. P. Migne’s Patrologiae Latinae (1891). See esp. Introductio ad Syllogismos Categoricos (pp. 761–92) and De Syllogismo Hypothetico (pp. 831–76).
    See Bocheński 6, Prior 2.

Brentano, Franz (1838–1917)

  1. Psychologie vom Empirischen Standpunkt (Leipzig, 1874; French translation by Maurice de Gandillac, Psychologie de point de vue empirique, Aubier, Paris, 1944), bk. ii, ch. 7, esp. §§ 7, 15.

Burleigh, Walter (1237–1345)

  1. De Puritate Artis Logicae, edited by P. Boehner (Franciscan Institute, St. Bonaventure, N.Y., 1951).
    See Boehner, Ockham, Prior 4.

Carroll, Lewis (Charles Lutwidge Dodgson, 1832–98)

  1. ‘A Logical Paradox’, Mind, 1894, pp. 436–8. See Johnson 2 and 3, Sidgwick 1 and 2.
  2. ‘What the Tortoise said to Achilles’, Mind, 1895, pp. 278–80. Answer to Sidgwick 2?

Church, Alonzo (1903— )

  1. A Bibliography of Symbolic Logic (Association for Symbolic Logic). Covers the period 1666–1935. (The JSL has aimed, in its reviews, at a complete coverage of the period from 1936 onwards, and also has occasional supplementations of Church’s Bibliography for the earlier period.)
  2. Reviews of Quine in JSL, vii (1942), pp. 100–1 and viii (1943), pp. 45–47. These, with 3, develop an answer from a Fregean point of view to the puzzles about ‘reference and modality’ raised in Quine 6 and 7.
  3. ‘A Formulation of the Logic of Sense and Denotation’, in Structure, Method and Meaning (Liberal Arts Press, N.Y., 1951).
  4. ‘The Weak Theory of Implication’, in Kontrolliertes Denken (Kommissions-Verlag Karl Alber, Munich, 1951).

Clark, Joseph T. (1911— )

  1. Conventional Logic and Modern Logic. A Prelude to Transition (Woodstock College Press, Woodstock, Md., 1952). Introduction by Quine.

Couturat, Louis (1868–1914)

  1. La Logique de Leibniz d’après des documents inédits (Alcan, Paris 1901). See especially the discussion of syllogistic logic, ch. i, §§ 1–10 (cf. Thomas 7), and of algebraic interpretations of propositional forms, ch. viii (cf. de Morgan 3).

De Morgan, Augustus (1806–78)

  1. Formal Logic (London, 1847; reprinted by Open Court Publishing Co., 1926, with original page-numbering incorporated in text).
  2. ‘On the Structure of the Syllogism, and on the Application of the Theory of Probabilities to Questions of Argument and Authority’, Transactions of the Cambridge Philosophical Society, viii (1849), pp. 379–408.
  3. ‘On the Symbols of Logic, the Theory of the Syllogism, and in Particular of the Copula, and the Application of the Theory of Probabilities to Some Questions of Evidence’, ibid., ix (1856), part i, pp. 79–127.
  4. ‘On the Syllogism, No. III, and on Logic in General’, ibid., x (1864), pp. 173–230.
  5. ‘On the Syllogism, No. IV, and on the Logic of Relations’ (with Appendix ‘On Syllogisms of Transposed Quantity’), ibid., pp. 331–58.
  6. ‘On the Syllogism, No. V, and on Various Points of the Onymatic System’, ibid., pp. 428–87.
  7. Articles ‘Logic’ and ‘Relation (Logic)’, in The English Cyclopedia, Arts and Sciences Division, v (1860), pp. 340–54, and vi (1861), pp. 1016–17.
    See Couturat, Keynes, Ladd-Franklin.

Dummett, Michael (1925— )

  1. Review of Frege 2 in Mind, 1954, pp. 102–5.

Feys, Robert (1889— )

  1. ‘Les Logiques nouvelles des modalités’, Revue néoscolastique de philosophie (Louvain), 1937, pp. 517–33; 1938, pp. 217–52. See Sobociński 4.
  2. ‘La Technique de la logique combinatoire’, RPL, 1946, pp. 74–103, 237–70.
  3. ‘Les Méthodes récentes de déduction naturelle’, ibid., 1946, pp. 340–400; 1947, pp. 60–72.
  4. ‘A Simple Notation for Relations’, Methodos, i (1949), pp. 79–93.
  5. ‘Les Systèmes formalisés des modalités aristotéliciennes’, RPL, 1950, pp. 478–509.

Frege, Gottlob (1848–1925)

  1. Die Grundlagen der Arithmetik (Breslau, 1884; reprinted with English translation by J. L. Austin, The Foundations of Arithmetic, Basil Blackwell, Oxford, 1950).
  2. Translations from the Philosophical Writings of Gottlob Frege, edited by Peter Geach and Max Black (Basil Blackwell, Oxford, 1952).
    See also Church 2 and 3, Dummett, Hailperin 2, Henkin.

Hailperin, Theodore (1915— )

  1. ‘Quantification Theory and Empty Individual-Domains’, JSL, xviii (1953), pp. 197–200. See Quine 9.
  2. ‘Remarks on Identity and Description in First-Order Axiom Systems’, ibid., xix (1954), pp. 14–20. Contains in § 3 a development of one of the methods of dealing with descriptions favoured by Frege.

Halldén, Sören (1923— )

  1. ‘Results Concerning the Decision Problem of Lewis’s Calculi S3 and S6’, JSL, xiv (1949), pp. 230–6.
  2. ‘On the Semantic Non-completeness of Certain Lewis Calculi’, ibid., xvi (1951), pp. 127–9.
    See Sobociński 4.

Henkin, Leon (1921— )

  1. ‘On the Primitive Symbols of Quine’s Mathematical Logic’, RPL, 1953, pp. 591–3. Simplifies Quine 4 (cf. also Quine 6, pp. 94–95) by making use of characteristic notions of Frege and Church.

Heyting, Arend (1898— )

  1. ‘On Weakened Quantification’, JSL, xi (1946), pp. 119–21.

Hilbert, David (1862–1943), and Ackermann, Wilhelm (1896— )

  1. Principles of Mathematical Logic (Chelsea Publishing Co., N.Y., 1950; translation of Grundzüge der Theoretischen Logik, edition of 1938).

Hofstadter, Albert (1910— ), and McKinsey, J. C. C.

  1. ‘On the Logic of Imperatives’, Philosophy of Science, vi (1939), pp. 446–57.

Johnson, William Ernest (1858–1931)

  1. ‘The Logical Calculus’, Mind, 1892, pp. 3–30, 235–50, 340–57.
  2. ‘A Logical Paradox’, ibid., 1894, p. 583. Answer to Carroll 1.
  3. ‘Hypotheticals in a Context’, ibid., 1895, pp. 143–4. Answer to Sidgwick 2.
  4. Logic (Cambridge University Press; Part I, 1921; Part II, 1922; Part III, 1924). Mill and Keynes on singular and general terms carried further in I. vi, vii, ix. 1, 2; II. i. 4–6, iv. 4; Keynes on existential import in I. ix. 3, 4; see also discussion of functions in II. iii and vi, and of fact and law in iii. i.
    Many of Johnson’s logical reflections also appear in footnotes to the later editions of Keynes 1.

Jordan, Z. (1911— )

  1. The Development of Mathematical Logic and of Logical Positivism in Poland between the Two Wars, being Polish Science and Learning No. 6 (Oxford University Press, 1945).

Keynes, John Neville (1852–1949)

  1. Studies and Exercises in Formal Logic (Macmillan; 1st ed. 1884; 2nd ed. 1887; 3rd ed. 1894; 4th ed. 1906). See especially his development of Mill’s views on singular and general terms in i. ii, iii; ii. vi; his discussion of existential import in i. viii; and of complex terms (in the tradition of de Morgan) in Appendix C (References to 4th ed.).

Ladd-Franklin, Christine (1847–1930)

  1. ‘Some Proposed Reforms in Common Logic’, Mind, 1890, pp. 75–88.

Lejewski, Czesław (1913— )

  1. ‘Logic and Existence’, British Journal for the Philosophy of Science, Aug. 1954, pp. 104–19. Develops a system equivalent to Leśniewski’s ontology but with ‘Every … is a …’ instead of ‘The … is a …’ as primitive operator; and discusses, from a Leśniewskian point of view, problems about the verb ‘exists’ raised in Quine 4 and 6.

Leonard, Henry S. (1905— ) and Goodman, Nelson (1906— )

  1. ‘The Calculus of Individuals and its Uses’, JSL, v (1940), pp. 45–55. A system akin to Leśniewski’s mereology.

Lewis, Clarence Irving (1883— ), and Langford, Cooper Harold (1895— )

  1. Symbolic Logic (New York, 1932).
    See also Barcan 1 and 2, Bennett, Church 3, Feys 1 and 5, Halldén 1 and 2, Łukasiewicz 6, McKinsey 2, Moody, Parry 1, Prior 6, Sobociński 4, Strawson 1, von Wright 2.

Łukasiewicz, Jan (1878— )

  1. ‘The Shortest Axiom of the Implicational Calculus of Propositions’, Proceedings of the Royal Irish Academy, 52 A 3 (Hodges, Figgis & Co., Dublin, and Williams & Norgate, London, 1948).
  2. ‘On Variable Functors of Propositional Arguments’, Proceedings of the Royal Irish Academy, 54 A 2 (Hodges, Figgis & Co., Dublin, 1951). See also Meredith 1.
  3. Aristotle’s Syllogistic (Clarendon Press, Oxford, 1951). See also Meredith 2, Thomas 5 and 6.
  4. ‘On the Intuitionistic Theory of Deduction’, Koninkl. Nederl. Akademie van Wetenschappen, Proceedings, Series A, 55, No. 3, and Indagationes Mathematicae, 14, No. 3 (North-Holland Publishing Co., Amsterdam, 1952).
  5. ‘Sur la formalisation des théories mathématiques’, in Les Méthodes formelles en axiomatique: Colloques Internationaux du Centre National de la Recherche Scientifique, No. 36 (published by the Centre, Paris, 1953).
  6. ‘A System of Modal Logic’, JCS, vol. i, No. 3 (July 1953), Paper 8. See Thomas 8.
  7. ‘The Principle of Individuation’, Proceedings of the Aristotelian Society, supplementary volume xxvii (London, 1953), esp. pp. 77 ff. See also Ajdukiewicz, Lejewski, Quine 5, Sobociński 2.

McKinsey, John Charles Chenoweth (1908–53)

  1. ‘Proof of the Independence of the Primitive Symbols of Heyting’s Calculus of Propositions’, JSL, iv (1939), pp. 155–8.
  2. ‘On the Syntactical Construction of Systems of Modal Logic’, ibid., x (1945), pp. 83–94.
  3. Review of Popper 3 in ibid., xiii (1948), pp. 114–15.
    See Hofstadter and McKinsey, McKinsey and Tarski.

McKinsey, J. C. C., and Tarski, Alfred

  1. ‘Some Theorems about the Sentential Calculi of Lewis and Heyting’, JSL, xiii (1948), pp. 1–15.

Mates, J. R. Benson (1919— )

  1. Stoic Logic (University of California Press, 1953). See Prior 5.

Meredith, Carew Arthur (1904— )

  1. ‘On an Extended System of the Propositional Calculus’, Proceedings of the Royal Irish Academy, 54 A 3 (Hodges, Figgis & Co., Dublin, 1951).
  2. ‘The Figures and Moods of the n-Term Aristotelian Syllogism’, Dominican Studies, vi (1953), pp. 42–47.
  3. ‘Single Axioms for the Systems (C, N), (C, O) and (A, N) of the Two-valued Propositional Calculus’, JCS, vol. i, No. 3 (July 1953), Paper 10.
  4. ‘A Single Axiom of Positive Logic’, ibid., Paper 12. See also Łukasiewicz 5 and 6, Rose 1.

Mill, John Stuart (1806–73)

  1. A System of Logic (1st ed., 1843; final edition the 8th). Mill’s characteristic views on singular and general terms are developed in I. ii. 3, 5; v. 1–4; vi; viii. 1; viii; II. ii and iii.
    See Whately, Keynes, Johnson 4, Brentano.

Moh Shaw-Kwei

  1. ‘Logical Paradoxes for Many-valued Systems’, JSL, xix (1954), pp. 37–40.

Moody, Ernest Addison (1903— )

  1. Truth and Consequence in Mediaeval Logic (North-Holland Publishing Co., Amsterdam, 1953).

Ockham, William of (c. 1285–1349)

  1. Tractatus de Praedestinatione et de Praescientia Dei et de Futuris Contingentibus, edited with a Study on the Mediaeval Problem of a Three-valued Logic by Philotheus Boehner (Franciscan Institute, St. Bonaventure, N.Y., 1945).

Parry, William Tuthill (1908— )

  1. ‘Modalities in the Survey System of Strict Implication’, JSL, iv (1939), pp. 137–54. See Feys 4.
  2. ‘A New Symbolism for the Logical Calculus’, ibid., xix (1954), pp. 161–8. Contains in § 3 an explanation of Leśniewski’s wheel symbolism for truth-operators, mentioned in Sobociński 1.

Peirce, Charles Sanders (1839–1914)

  1. Collected Papers of Charles Sanders Peirce, edited by Charles Hartshorne and Paul Weiss (Harvard University Press, 6 volumes, 1931–5). Of particular value to the formal logician are the following items and passages: On his own development, 4. 2–4; on the history of logic, 4. 21–37; on various aspects of the traditional syllogism, 2. 445–516, 619–31; 3. 154–97, 407–14, 5. 320–32; on truth-operators, 4. 12–20, 257–65; on implication, 2. 344–56, 3. 154–97, 365–91, 440–8, 4. 69–73; on the logic of relations, 3. 45–149, 328–58, 416–22 (on nouns and verbs), 571–608, 4. 453; on ‘not’ as a relation, 2. 550, 597–9, 3. 407–14; on logic systematically viewed as the theory of implication with lower- and higher-order quantification, 3. 365–403 M; on higher-order quantification, 4. 80–84; on logical puzzles and paradoxes, 2. 618, 4. 78, 546, 5. 333–40.
  2. Article ‘Syllogism’, in The Century Dictionary (London, 1900–1).

Petrus Hispanus (c. 1215–77)

  1. Summulae Logicales, edited by I. M. Bocheński (Marietti, Turin, 1947).
    See Boehner, Moody, Prior 1.

Popper, Karl Raimund (1902— )

  1. ‘What is Dialectic?’, Mind, 1940, pp. 403–26.
  2. ‘New Foundations for Logic’, ibid., 1947, pp. 193–235.
  3. ‘Logic without Assumptions’, Proceedings of the Aristotelian Society, 1946–7.
    See McKinsey 3.
  4. ‘The Trivialization of Mathematical Logic’, Proceedings of the Xth International Congress of Philosophy (Amsterdam, 1949), pp. 722–7.
  5. ‘Self-Reference and Meaning in Ordinary Language’, Mind, 1954, pp. 162–9.

Prior, Arthur Norman (1914— )

  1. ‘The Parva Logicalia in Modern Dress’, Dominican Studies, v (1952), pp. 78–87.
  2. ‘The Logic of Negative Terms in Boethius’, Franciscan Studies, March 1953, pp. 1–6.
  3. ‘Negative Quantifiers’, Australasian Journal of Philosophy, Aug. 1953, pp. 107–23.
  4. ‘On Some Consequentiae in Walter Burleigh’, The New Scholasticism, Oct. 1953, pp. 433–46.
  5. ‘Diodoran Modalities’, Philosophical Quarterly, 1955.
  6. ‘Many-valued and Modal Systems: An Intuitive Approach’, Philosophical Review, 1955.

Prior, Mary Laura (1922— ), and Prior, A. N.

  1. ‘Erotetic Logic’, Philosophical Review, 1955, pp. 43–59.

Quine, Willard van Orman (1908— )

  1. ‘A Note on Nicod’s Postulate’, Mind, 1932, pp. 345–50.
  2. A System of Logistic (Harvard University Press, 1934).
  3. ‘Completeness of the Propositional Calculus’, JSL, iii (1938) pp. 37–40.
  4. Mathematical Logic (Harvard University Press, revised edition, 1951).
  5. Review of Ajdukiewicz 1, JSL, xvii (1952), pp. 141–2.
  6. From a Logical Point of View (Harvard University Press, 1953).
  7. ‘Three Grades of Modal Involvement’, Proceedings of XIth International Congress of Philosophy (Brussels, 1953), vol. xiv.
  8. ‘Mr. Strawson on Logical Theory’, Mind, 1953, pp. 433–51. A review article on Strawson 3.
  9. ‘Quantification and the Empty Domain’, JSL, xix (1954), pp. 177–9. A simplification of Hailperin 1. See Church 2 and 3, Clark, Henkin, Lejewski.

Rose, Alan (1927— )

  1. ‘An Axiom System for Three-valued Logic’, Methodos, iii (1951), pp. 233–9. Contains a proof, by Meredith and the author, of postulate set 1.2 (see previous Appendix) from set 1.3.

Russell, Bertrand Arthur William (1872— )

  1. ‘On Denoting’, Mind, 1905, pp. 479–93 (reproduced in Feigl and Sellars, Readings in Philosophical Analysis, Appleton-Century-Crofts, 1949). See Frege 2, Hailperin 2, Lejewski, Strawson 2.
  2. Introduction to Mathematical Philosophy (Allen & Unwin, London, 1919). See Whitehead and Russell.

Sidgwick, Alfred (1850–1943)

  1. ‘A Logical Paradox’, Mind, 1894, p. 582. Answer to Carroll 1.
  2. ‘Hypotheticals in a Context’, ibid., 1895, p. 143. Answer to Johnson 2.
    See Johnson 3, Carroll 2.

Sobociński, Bolesław (1906— )

  1. An Investigation of Protothetic, Éditions de l’Institut d’Études Polonaises en Belgique (Brussels, 1949). See Parry 2.
  2. ‘L’Analyse de l’Antinomie Russellienne par Leśniewski’, Methodos, i (1949), pp. 94–107, 220–8, 308–16; ii (1950), pp. 237–57. See also Leonard and Goodman.
  3. ‘On a Universal Decision Element’, JCS, vol. i, No. 2, Jan. 1953, Paper 5. Contains (Note 4) tabulated definitions of truth-functions in terms of S (i.e. our X) and D; and in the text, an account of a tetradic operator Q such that all monadic and dyadic truth-functions are obtainable by substitutions of p, q, 1 or 0 in Qpqrs. (A by-product, perhaps, of the work detailed in the main text of 1.)
  4. ‘Note on a Modal System of Feys–von Wright’, JCS, vol. i, No. 3, July 1953, Paper 13.

Strawson, Peter Frederick (1919— )

  1. ‘Necessary Propositions and Entailment-Statements’, Mind, 1948, pp. 184–200. Cf. Quine 7.
  2. ‘On Referring’, ibid., 1950, pp. 320–44.
  3. Introduction to Logical Theory (Methuen, 1952). See Quine 8.

Tarski, Alfred (1902— )

  1. Introduction to Logic and to the Methodology of Deductive Sciences (Oxford University Press, revised edition 1946).
  2. Studies in Logic and the Foundations of Mathematics (Clarendon Press, 1955).
    See also McKinsey and Tarski.

Thomas, Ivo (1912— )

  1. ‘Logic and Theology’, Dominican Studies, i (1948), pp. 291–312. See Bocheński 4.
  2. ‘CS(n): An Extension of CS’, ibid., ii (1949), pp. 145–60.
  3. ‘Farrago Logica’, ibid., iv (1951), pp. 69–79.
  4. ‘St. Vincent Ferrer’s De Suppositionibus’, ibid., v (1952), pp. 88–102.
  5. ‘Recent Contributions to Logic’, ibid., pp. 205–16 (Review of Łukasiewicz 3, Boehner 1, and others).
  6. ‘A New Decision Procedure for Aristotle’s Syllogistic’, Mind, Oct. 1952, pp. 564–6.
  7. ‘Kilwardby on Conversion’, Dominican Studies, vi (1953), pp. 56–76.
  8. ‘Note on a Modal System of Łukasiewicz’, ibid., pp. 167–70.

Von Wright, Georg Hendrik (1916— )

  1. Form and Content in Logic (Cambridge University Press, 1949).
  2. An Essay in Modal Logic (North-Holland Publishing Co., Amsterdam, 1951). See Sobociński 4.

Whately, Richard (1787–1863)

  1. Elements of Logic (1st ed. 1826; last edition the 9th). Mill’s views on singular and general terms foreshadowed in 1.6. See Prior, M. L.

Whitehead, Alfred North (1861–1947), and Russell, Bertrand Arthur William

  1. Principia Mathematica (Cambridge University Press; 1st ed., vol. i, 1910; vol. ii, 1912; vol. iii, 1913; 2nd ed., vol. i, 1925, vols. ii and iii, 1927).
at

No comments:

Post a Comment