1. Im Jahre 1919 wurde mir das Wort Selbstbestimmung, das in aller Leute Munde war, Anlaß eines Versuches, mir einen klaren Begriff zu dem Wort zu bilden. Natürlich stieß ich dabei alsbald auf die Schwierigkeiten und Dunkelheiten des Sollensbegriffes: das Problem wandelte sich. Grundbegriff aller Ethik, kann der Begriff des Sollens ein brauchbares Fundament ihres Aufbaus nur geben, wenn er in einem System von Axiomen festgelegt ist. Ein solches Axiomensystem führe ich hier vor (Mally 1926, Preface, p. I).

2. Menger (1939, p. 57) and Føllesdal and Hilpinen (1981, pp. 2-3) made the same decision.

3. Menger (1939, p. 58) said that Mally derived "fifty" theorems, while Føllesdal and Hilpinen (1981, p. 3) said that Mally derived "about fifty" theorems. They probably included some of Mally’s unnumbered theorems, which Mally mentioned only in passing. Our list consists of Mally’s thirty-six explicitly numbered theorems.

4. Diese letzten Sätze, die Seinsollen und Tatsächlichsein zu identifizieren scheinen, sind unter unseren "befremdlichen Folgerungen" wohl die befremdlichsten (Mally 1926, p. 25).

5. The formula on this line is a theorem of the classical propositional calculus because A → (B → B) and A → (B → A) are theorems of this calculus.

6. The formula on this line is a theorem of the classical propositional calculus because

7. The proofs that A → !A and A ↔ !A are theorems of S0.9⁰ enriched with ! and supplemented with I′ and III′ are to be found in Lokhorst 2010.

8. We only prove that I* is a theorem of RD. The other five cases (II* and III* are theorems of RD and I–III follow from I*–III*) are left to the reader.

Axiom II* is actually redundant. The following formulas are theorems:

We therefore have:

We owe this proof to John Slaney.

9. Most cases are obvious but some hints for (16)–(18) and (30) may be helpful. (16) is a consequence of I* and IV. (17) follows from (16) and (18). (18) may be proven as follows:

(30) is proven as follows: we have ∩ → (V → ∩) by Ax. t, whence ∩ → (U → Λ) by Contraposition and Double Negation, whence ∩ → !Λ by (16).

10. In order to prove this claim, we first have to remove an obstacle: (2), (5), (15) and (27) do not belong to the language of RD because they contain propositional quantifiers. If such quantifiers were added in the usual way (Anderson, Belnap & Dunn 1992, sec. 32), then we could easily prove that (2), (5), (15) and (27) are deductively equivalent with (2′), (5′), (15′) and (27′), respectively:

To avoid needless complications, we will not equip RD with quantifiers, but confine our attention to the unquantified versions of (2), (5), (15) and (27). We may now proceed with the actual proof. We use the following matrices:

Each theorem M of RD has the following property: v(M)∈{1, 3, 5} for every assignment v of values to the variables in M such that

• v(A) ∈ {0, 1, 2, 3, 4, 5},
• v(V) = 1,
• v(U) = 2,
• v(¬A), v(A → B) and v(A & B) are as indicated in the tables,
• v(A ∨ B) = v(¬(¬A & ¬B)), and
• v(!A) = v(U → A).

(1), (2), (5), (7), (12), (13), (15), (19)–(23), (24)–(29), (31)–(35), A → !A and !A → A (unquantified versions) lack this property, so these formulas are not theorems of RD. (These matrices were discovered by the computer program MaGIC. See the section Other Internet Resources for information on this program.)

11. Menger’s theorem A ↔ !A is a theorem of both RD+(34) and RD+(35):

However, neither (34) nor (35) is derivable in RD supplemented with A ↔ !A. To prove this, we use the following table from Anderson and Belnap 1975, p. 148:

Each theorem M of RD+{A ↔ !A} has the following property: v(M) ∈ {1, 2} for every assignment v of values to the variables in M such that

• v(A) ∈ {0, 1, 2},
• v(V) = 1,
• v(U) = 2,
• v(¬A) and v(A → B) are as indicated in the table,
• v(A & B) = min{v(A), v(B)},
• v(A ∨ B) = max{v(A), v(B)}, and
• v(!A) = v(A).

But v((34)) = v(U → V) = 0 and v((35)) = v(Λ → ∩) = 0, so (34) and (35) are not theorems of RD+{A ↔ !A}.

12. See Lokhorst 1999, pp. 277-278.

13. One may use the three-valued matrices of note 11 to prove this.

14. Anderson 1967, p. 348. However, Menger (1939, p. 59) had already defined "I command p" as "unless p, something unpleasant will happen," or in symbols: Cp ↔ (¬p → A), where Cp stands for "I command p" and A denotes the statement that the unpleasant thing will happen.

15. One may use the six-valued matrices of note 10 to prove this.

16. Wer richtig will, will nicht (auch nicht impliziterweise) das Negat des Gewollten; richtiges Wollen ist widerspruchsfrei (Mally 1926, p. 49). Mally regarded this as a paraphrase of Axiom V, but this is not entirely correct. Morscher (1998, p. 106) has suggested that ARD2 expresses Mally’s intentions more adequately than Axiom V does.

17. ARD1 is a theorem of RD+ARD1( → ) by virtue of theorem (16), i.e., ARD1( ← ). This completes the proof. Notice that Axiom V is redundant because we have !U by Ax. IV, whence ¬!∩ by ARD2, whence ¬(U → ∩) by ARD1, whence ¬(U → (U → ∩)) by R, whence ¬(U → !∩) by ARD1, whence Axiom V by Def. f.

18. Proof:

19. Proof. First, !A ↔ ¬ ¬ A is a theorem of ID:

Second, the axioms of ID can be derived from the following theorems of IPC plus !A ↔ ¬ ¬ A and (34):

20. Proof.

21. Proof: see Figure 1: ¬ ¬ (2 ∨ 3) → (¬ ¬ 2 ∨ ¬ ¬ 3) = ¬ ¬ 4 → 4 = 1 → 4 = 4.

Figure 1. ∧ and ∨ are interpreted as lattice meet and join, respectively. The designated value is 1. Matrix from McKinsey 1939, p. 157.

22. Proof: see Figure 1: ¬ (2 & ¬ ¬ ¬ 2) ↔ (¬ 2 ∨ ¬ ¬ 2) = 1 ↔ 4 = 4.

23. Proof. First, if (13b) is a theorem, then !(A ∨ B) → (!A ∨ !B) is also a theorem:

Second, if !(A ∨ B) → (!A ∨ !B) is a theorem, then (13b) is also a theorem:

24. Proof: see Figure 2: ¬ ¬ 2 → 2 = 1 → 2 = 2.

Figure 2. ∧ and ∨ are interpreted as lattice meet and join, respectively. The designated value is 1. Matrix from McKinsey 1939, p. 157.

25. Proof. IPC provides (A → ¬ ¬ B) ↔ (¬ ¬ A → ¬ ¬ B), so ID provides (A → !B) ↔ (!A → !B) by Fact 1. ID provides !A ↔ ¬ ¬ A by Fact 1.

26. Morscher (1998) has made a somewhat similar proposal, but the details are different. The present approach was inspired by a number of suggestions made by Lou Goble.