Mechanization of logic and mechanization of numerical calculation

[9 January 2015]

In their book Mechanization of reasoning in a historical perspective (Amsterdam: Rodopi, 1995), Witold Marciszewski and Roman Murawski write (actually, this chapter is by WM):

Albert Einstein could not do without arithmetical data-processing in his computations, but had no need to resort to rules of formalized deduction in his reasonings …

Point taken. (It should be noted that WM and RM define data-processing broadly, to include things like the mechanical rules for multiplication and long division taught in primary schools.) We use mechanical rules for arithmetic calculation all the time, but very seldom for inference. It would be interesting to have a theory as to why this might be so. Perhaps humans are better at inference than at arithmetic? (Certain kinds of inference will, I guess, have been reinforced and selected for by evolution.) Or perhaps humans are so bad at inference that people seldom or never engage in chains of inferences that would require mechanical aid? As if we never did arithmetic with numbers greater than ten?

Of course, sometimes people make mistaken inferences, which mechanized reasoning aids could in theory prevent.

And compare Leibniz’s suggestion that people would do better in some endeavors if they did resort more often to rules of formalized deduction (in “De logica nova condenda”, in Die Grundlagen des logischen Kalk├╝ls, ed. and tr. Franz Schupp with Stephanie Weber [Hamburg: Meiner,2000], p. 2 [my translation, following Schupp and Weber]):

Est vero in notra potestate, ut in colligendo non erremus, si scilicet quoad argumentandi formam rigide observemus regulas Logicas, quoad materiam vero nullas assumamus propositiones, quarum vel veritas, vel major ex datis probabilitas, non sit jam antea rigorose demonstrata. Quam methodum secuti sunt Mathematici, admirando cum successu.

Est etiam in potestate nostra, ut controversias finiamus, si scilicet argumenta quae afferuntur in formam accurate redigamus, non syllogismos tantum formando atque examinando, set et prosyllogismos, et prosyllogismorum prosyllogismos, donec vel absolvatur probatio, vel constet quid adhuc investigandum probandumve argumentanti supersit, ne scilicet inani circulo priora repetat, et Diogenis dolium volvat.

But it is in our power not to err in logical inference, namely if we rigidly observe the rules of logic, with respect to the form of argument, and if with respect to the subject matter weal assume nothing whose truth, or at least its likelihood, has not been shown on the basis of available data. Which is the method that the mathematicians have followed with admirable success.

It is also in our power to put an end to controversies, namely if we put the arguments brought forward accurately into a form, in which we not only formulate and examine the syllogisms of the argument, but the prosyllogisms, and the prosyllogisms of the prosyllogisms, until finally the proof is completed, or else it is established what parts of the argument must be further investigated in order to avoid falling into an empty circle repeating what has already been said, and rolling the tub of Diogenes.

Is there a contradiction here, or can these two views be reconciled?