(p.318) Appendix II (1960) Some Methods of Proof
(p.318) Appendix II (1960) Some Methods of Proof
§ 1. Propositional Calculus; Condensed Detachment
FOLLOWING Meredith, let us write Dxy for the most general result of detachment with x, or some substitution in x, for our Cαβ, and y, or some substitution in y, for our α (‘most general’ in the sense of having no unnecessary identifications of variables. For example, with 1. Cpp and 2. CpCqp, D21 is CqCpp, not CpCpp or CqCqq, though these also are obtainable by detachment with substitutions in 2 for our Cαβ and 1 or a substitution in it for our α).
With this method of abridgement we give, firstly, a proof of the Tarski-Bernays axioms, i.e. 2.11 of previous Appendix, from the C-pure axioms in Peirce’s 3.11:
The Tarski–Bernays set are 3, 4, 16. 1 is not independent, since it is D12.4, and is not itself used in the proof of 12. In the remaining three axioms, 2 is replaceable by 15, since D6.15 = 2, and the ‘synthetic theorem’ 6 (= DD33D33) follows from 3 alone. Since 3, 4, 15 are thus a sufficient set, so is the pair 4, 11 (2.14 (b) of previous Appendix); for DD11.4.4 = 1, and (see set 12.7) DD11.11.1 = 3 and DD11.1.1 = 15.
That 3, 4 and 15 suffice for C-pure was noted by Wajsberg; and Łukasiewicz’s more general result, the sufficiency of set 2.12, is demonstrated as follows:
Frege’s third axiom (set 1.1) is proved from his first two thus:
If, on the other hand, we take as axioms 1. CpCqp, 2. CCqCprCCpqCpr, 3. CCpCqrCqCpr, we obtain Frege’s 2 as DD2D3D123.
When thus investigating the deductive possibilities of different formulae, it is handy to refer to the more important of them by nicknames, e.g.
‘Simp’ is for Simplification, and Dilemma is so called because with q/o it becomes CCNprCCprr. Note that Comm and Comm Comm, i.e. D(Comm) (Comm), are interdeducible—put X for the latter, and Comm is DDXXX (cf. Łukasiewicz, Aristotle’s Syllogistic, p. 107). Syll Simp, i.e. D(Syll) (Simp), is a useful thesis—with Clavius or Peirce it gives Identity, Cpp; with CCNqNpCpq, CNpCpq; with CCCpqpCCpqq or with Roll, Modus Ponens.
§ 2. Suppositional Proof in Ontology
In developing their various characteristic disciplines, Leśniewski and his school often set out their proofs in ‘suppositional’ form, first listing the various components of the antecedent of the thesis to be proved, and then showing step by step how its consequent follows, gathering each formula proved into a continually enlarging conjunctive consequent, with the required consequent as the final conjunct.
We may illustrate this method by using it to set out (following B. Sobo-ciński) the proofs involved in the derivation of Leśniewski’s original onto-logical axiom of 1920 from his much abridged one of 1929 (see Appendix I, 9.21). General principles from prepositional logic and quantification theory, such as CEpqCqp or CCΣaf(a)pΠaCf(a)p, are simply assumed without being stated (those two, for example, in the proof of T1).
(Note how the existential quantification falls away when the variable which it binds disappears from the conclusion of the inference made from premisses within its scope. This is a frequent move in proofs of this type.)
This definition merits a little comment. Leśniewskian systems do not assume at the outset an infinity of types of variables for which appropriate substitutions may be made, if necessary by ‘apostrophe’; e.g. a variable ϕ for monadic proposition-forming functors of terms, such that by the substitution ϕ/ε’b we may pass from ϕa to εab. The procedure is rather first to define a functor ε′ such that its application to a term b forms a functor(ε′b) whose application to the term a forms a proposition equivalent to εab. (This is D2 above; propositions of such forms as (ε′b)a are described as ‘many-link functions’, as they are formed by means of functors which are themselves functions.) We may then, and only then, having a particular expression of the category of monadic proposition-forming functors of terms, introduce variables of this category, for which we can make substitutions (but not apostrophic ones; though it is clear that the actual effect of performing the substitution ϕ/ε’b in ϕa may be obtained by performing the substitution ϕ/(ε′b) and then passing form (ε′b)a to εab by D2). In this way the system becomes richer in its ‘semantic categories’ as well as in its theses as we go (p.321) along; and for each newly introduced category we may lay down its own law of extensionality, as T6 below for the category of (ε′b).
(The remaining steps are Leśniewski’s, 1929)
(T8; T3; T1; T7)
§3 Suppositional Proof in Propositional Calculus
The procedure of deriving the consequent of a thesis from its antecedents and affirming the whole implication on the basis of this derivation, is clearly capable of wider use, and in 1934, following a suggestion made by Łukasiewicz in 1936, S. Jaśkowski set up a system of rules for such derivations which could be used for establishing the propositional calculus in C and N. In sketching his procedure, I shall use some of the devices employed by later writers in connexion with the richer ‘natural deduction’ systems of G. Gentzen.
We write premisses and conclusions as numbered lines, putting at the left the number or numbers of the premiss or premisses (‘suppositions’) on which the given formula ultimately depends, and on the right the rule by which, and premiss or premisses from which, the line is immediately derived. Jaśowski’s four rules for C–N are then in effect the following:
(i) Rule of Premisses (P): Any formula may be laid down as a consequence of itself or of any set of assumptions including itself.
(ii) Rule of C-Introduction, Conditionalization, or Conditional Proof (CP): If a formula β is derivable from assumptions which include α, then we can derive Cαβ from any further assumptions on which β may depend.(p.322)
(iii) Rule of C-Elimination, Detachment, or Modus Ponens (MP): α, Cαβ → β. β will then depend on any assumptions on which either α or Cαβ may depend.
(iv) Rule of N-Elimination (NE): Given derivations of both β and Nβ from an assumption Nα, we may derive α from any further assumptions on which either β or Nβ may depend.
Of the three conclusions which here emerge as not depending on any particular supposition, (4) and (13) form Łukasiewicz’s basis for the positive implicational calculus (12.1), and in fact a suppositional proof or series of proofs using Rules (i)–(iii) above provides one of the most straightforward ways of showing that a formula is in that calculus. We may often sketch such proofs by tabulating the antecedents of a formula and indicating by arrows how its final consequent follows from them, thus (for the proof of (13)):
With (20) added, (4) and (13) give one of Łukasiewicz’s bases for classical C–N (1.4(c)). Jaśkowski noted also that if in his rule (iv) the assumption Nα is replaced by α, and the conclusion α by Nα, the rules no longer yield classical C–N but do yield Kolmogorov’s calculus (12.4). (iv) with this change is in fact an exact counterpart of Kolmogorov’s own axiom CCpqCCpNpNp for subjunction to C-positive.
The rule CP, when occurring as a derived rule in a system in which the originally given rules are different, is called the ‘deduction theorem’.