When did mathematicians first use the contrapositive form to prove a conditional statement?

Question

I am reading parts of Euclid’s Elements and I am surprised, rightly or wrongly, to see that Euclid did not recognize that a conditional is logically equivalent to its contrapositive form. Indeed, one often sees one proposition immediately followed by another proposition giving its contrapositive and a separate proof (usually by a reductio argument on the original statement) .

The Stoics, who came just after Euclid, were the first to explicitly recognise modus tollens as valid argument form, and the equivalence of a conditional and its contrapositive follows from the application of modus tollens.

Since the equivalence of the two forms is evident from their truth tables, I was equally surprised to read that truth tables have their origins in the late 19th century. (According to the wiki entry on truth tables it was the logician C.S. Pierce who is credited with first formulating truth tables, including them in an unpublished manuscript dated 1893.)

So that “narrows” down the recognition of the equivalence of the two forms to sometime between Euclid and Pierce - a period of about 2200 years.

Q : When did mathematicians first use the contrapositive form to prove a conditional?

Answer 1

This is one of those cases where it is easy to take modern ideas for granted, and wonder how something so "obvious" could be missed. Modern formal logic with its array of logical operations, Boolean algebra and predicates is the creation of late 19th century, only finalized after much labor by Russell and Whitehead around 1910. Logical analysis that translates natural sentences into formally manipulable ones was also a 19th century invention (especially Frege's), and so was the axiomatic method (especially Pasch's, Peano's and Hilbert's). Stoics did introduce some propositional forms in the 3rd century BC, but not in relation to mathematics, and they never took. Between them and 19th century the only person to pursue propositional logic was Leibniz, who does list contraposition as a valid form in Generales Inquisitiones (1686). But like most of his logical works it was not published until 1902.

For everybody else formal logic was identical to Aristotle's syllogistic, where one could get from "all humans are mortal" to "all immortals are non-human", but which did not have expressive means for intricate mathematical reasoning. Friedman discusses in detail (pp.475-477) how expressive poverty of syllogistic impeded the rigorization of calculus. Since it was the only established formal logic flipping conditionals "blindly" would not have been kosher. And in the natural reasoning the difference between proof by contraposition and proof by contradiction is highly artificial, in both the conclusion is negated and the negation of something in the premise is derived. So discerning the use of "contraposition" before Leibniz is a matter of one's willingness to read between the lines. This said, according to Wirth, Fermat was particularly self-conscious:

"Fermat was the first who — instead of just proving a theorem — analyzed the method of proof search. Moreover, in his letter for Huygens and in [Diophantus, 1670], Fermat was also the first to provide a correct verbalization of proofs by Descente Infinie and to overcome the presentation of induction proofs as “generalizable examples”".

"For instance, in Euclid’s Elements, Proposition VIII.7 is just the contrapositive of Proposition VIII.6, and this is just one of several cases that we find a proposition with a proof in the Elements, where today we just see a corollary. Moreover, even Fermat reported in his letter for Huygens that he had had problems to apply the Method of Descente Infinie to positive mathematical statements... Because of the work of Frege and Peano, these logical differences may be considered trivial today. Nevertheless, they were not trivial before, and to understand the history of mathematics and the fine structure in which mathematicians reasoned, the distinction between affirmative and negative theorems and between direct and apagogic methods of demonstration is important".

P.S. Despite the common reading of Hilbert into Euclid, Euclid was not interested in building a deductive system from axioms and logic, and his "deviations" from this "task" are not oversights. He was interested in systematizing geometry, which he saw as an idealized representation of the "sensibles", a kind of "theoretical physics", and explicating common assumptions and types of reasoning used by geometers. These included reasoning from construction of diagrams, which was considered legitimate as long as they were used "indeterminately", see Acerbi's Euclid's Pseudaria (4.1). When contraposition remains valid in such reasoning is not a priori obvious, in general it fails in constructivism.

Answer 2

I don't have enough reputation to comment. Are you reading Euclid from the original Ancient Greek text or are you reading it from a translation? And can you give an example of two (not necessarily consecutive) propositions where you observed this? I also noticed that you observed that an equivalence is proved in four successive propositions in some cases. Can you give an example of this?

In many instances, Euclid proves and states one conditional and immediately proves the converse, not the contrapositive. But this might be difficult to catch because of the word order. I tried to translate from Ancient Greek earlier and I was surprised myself. But as an example you can see the guide for Proposition 1.18 and 1.19 by David E. Joyce.

Answer 3

A translation attributed to John Wells (see http://darshanapress.com/The%20Vaisheshika%20Darshana.pdf), of कारणाभावात्कार्याभावः। न तु कार्याभावात्कारणाभावः reads thus: "1.10 Absence of effect is known by the absence of a cause, 1.11 but absence of cause is not (necessarily) known by the absence of an effect." (Wells, 2009, p. 4)

Wells' translation invoked above is listed as the translation of the critical edition of the वैशेषिक सूत्र (Vaiśeṣika Sūtra) [see footnote 17 in https://en.wikipedia.org/wiki/Vai%C5%9Be%E1%B9%A3ika_S%C5%ABtra#cite_note-FOOTNOTEBimal_Krishna_Matilal197755%E2%80%9356-20] attributed to कणाद (Kaṇāda).

Citing Fowler (2002, pp. 98-99, Perspectives of Reality: An Introduction to the Philosophy of Hinduism) and Margenau (2012, pp. xxx-xxxi, Physics and Philosophy: Selected Essays) the link invoked immediately above includes the following about when the Vaiśeṣika Sūtra was likely compiled: "...the Vaiśeṣika Sūtra was likely compiled sometime between 6th and 2nd century BCE,..."

In view of i) all of the above, and ii) in the context of the question — When did mathematicians first use the contrapositive form to prove a conditional statement? — the following points seem noteworthy:

a) 1.10 above — कारणाभावात्कार्याभावः ("Absence of effect is known by the absence of a cause") — is, it can be reasonably posited, very very close to "If not B, then not A" (given "If A then B"), basically what is referred to as "Proof by Contrapositive."

b) Interestingly, 1.11 above — न तु कार्याभावात्कारणाभावः ("but absence of cause is not (necessarily) known by the absence of an effect") does not stop at the equivalent of "If not B, then not A" (basically 1.10 above), but goes on to add the equivalent of the point that "If A then B," does not necessarily mean "If not A then not B."

In my view, any history of the idea of what is today referred to as "Proof by Contrapositive" https://en.wikipedia.org/wiki/Proof_by_contrapositive#:~:text=In%20mathematics%2C%20proof%20by%20contrapositive,%2C%20then%20not%20A%22%20instead. that aspires to be truly global and inclusive, will need to, at the very least, include a mention of the वैशेषिक सूत्र (Vaiśeṣika Sūtra) attributed to कणाद (Kaṇāda), if not presenting "कारणाभावात्कार्याभावः। न तु कार्याभावात्कारणाभावः" from the वैशेषिक सूत्र (Vaiśeṣika Sūtra) attributed to कणाद (Kaṇāda) as amongst the earliest, if not the earliest, extant statement related to "Proof by Contrapositive".