Jump to ContentJump to Main Navigation
Formal Logic$

Arthur N. Prior

Print publication date: 1963

Print ISBN-13: 9780198241560

Published to Oxford Scholarship Online: October 2011

DOI: 10.1093/acprof:oso/9780198241560.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: 27 February 2017

(p.318) Appendix II (1960) Some Methods of Proof

(p.318) Appendix II (1960) Some Methods of Proof

Formal Logic
Oxford University Press

§ 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:

Appendix II (1960) Some Methods of Proof

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:

Appendix II (1960) Some Methods of Proof


Appendix II (1960) Some Methods of Proof

Frege’s third axiom (set 1.1) is proved from his first two thus:

Appendix II (1960) Some Methods of Proof

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.

Appendix II (1960) Some Methods of Proof

‘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).


Appendix II (1960) Some Methods of Proof
Appendix II (1960) Some Methods of Proof
Appendix II (1960) Some Methods of Proof

(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.)

Appendix II (1960) Some Methods of Proof

D2. ΠabEεab(ε′b)a

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

T6. ΠabEΠcEεcaεcbΠϕEϕaϕb

Appendix II (1960) Some Methods of Proof

(The remaining steps are Leśniewski’s, 1929)

Appendix II (1960) Some Methods of Proof


       (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:

  1. (i) Rule of Premisses (P): Any formula may be laid down as a consequence of itself or of any set of assumptions including itself.

  2. (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.

  3. (iii) Rule of C-Elimination, Detachment, or Modus Ponens (MP): α, Cαβ → β. β will then depend on any assumptions on which either α or Cαβ may depend.

  4. (iv) Rule of N-Elimination (NE): Given derivations of both β and from an assumption , we may derive α from any further assumptions on which either β or may depend.

Illustrative deductions:

Appendix II (1960) Some Methods of Proof

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)):

Appendix II (1960) Some Methods of Proof

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 is replaced by α, and the conclusion α by , 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’.