How to reconcile the fact that mathematical proofs are logical implications with the lack of a formal calculus equivalent to the logical implication? [closed]

Question

Theorems follow from axioms. That is, theorems are the logical consequence of axioms. Thus, mathematical proofs are essentially deductive. Proofs are all essentially logical implications. There is not one proof in mathematics which is not a logical implication.

Yet, mathematicians make nonsensical or contradictory claims on the subject.

First, mathematicians seem to all insist that theorems are proved using the material implication, not the logical implication, even though this is patently false since most theorems are not even proved formally, since mathematicians still today prove their theorems essentially in the same way as they did before mathematical logic and the introduction of the material implication.

Mathematicians keep using the label "material implication" even though the material implication is not an implication. It is essentially and obviously a simple logical operation.

Some mathematicians say, without proof, that the material implication is equivalent to the logical implication. How can prove using the logical implication that the material implication is equivalent to the logical implication and this even though you do not understand the logical implication?

Others mathematicians say, again without proof, that the material implication "improves" on the logical implication understood in the Aristotelian or "colloquial" sense. How can you claim to improve on something you do not understand?

Some mathematicians also claim that mathematics is a sort of meaningless formal "game", based on the mindless application of arbitrary rules of derivation. Yet, you cannot apply a rule without relying not only on the rule itself, but on your own logical capacity. Mindless is not an option. The application of a rule is itself a logical implication, something which is made explicit in the use of the expression "rule of inference". For example, the material implication itself can be used through the application of a rule of inference, a sort of bogus modus ponens called... "modus ponens", written in two different ways:

p ⊃ q
p
———
∴ q

Or:

p ⊃ q, p
————
q

So, how do you personally reconcile the fact that mathematical proofs are essentially deductive, and therefore necessarily involves logical implications, with the fact that there is still today in mathematics no formal calculus logically equivalent to the logical implication?

Answer 1

There is some need for clarification here. Nobody claims that material implication is the same as logical implication. Material implication, or the material conditional, is an object-language propositional connective. It is the same kind of thing as ⋀ and ⋁ - its job is simply to take two truth values as arguments and return a truth value as a result. It can be defined syntactically using natural deduction rules, such as the classical rules of modus ponens and conditional proof. It can also be defined semantically using a truth table. The two definitions are provably equivalent.

Logical implication, or logical consequence, is a meta-level relationship between sentences; it holds when one sentence is logically entailed by others. Again, it can be divided into syntactic and semantic components. We use the turnstile Γ ⊢ α to indicate that α is the syntactic consequence of Γ, which can also be read as Γ proves α, or α is a theorem on Γ. We use the double turnstile Γ ⊨ α to indicate that α is the semantic consequence of Γ, which is usually cashed out using model theory as every model of Γ is a model of α. For first order predicate logic, syntactic and semantic consequence are provably coextensive.

Having distinguished material and logical implication, there is now an important relationship between them. For any argument, there is a corresponding conditional sentence. For example, if we have an argument A, B, C; therefore D, we can formulate a sentence "if A and B and C then D". Naively speaking, the argument is valid if and only if the corresponding conditional sentence is necessarily true. We can then give more concrete form to the naive 'necessarily' by representing it syntactically as 'provably', or semantically as 'under all interpretations'. Now here is the big pay-off... If we are using classical logic, the 'if/then' that appears in the corresponding conditional sentence is material implication. In other words, an argument such as A, B, C; therefore D is classically valid if and only if the sentence "(A ⋀ B ⋀ C) → D" is provable, where → is material implication.

This is fundamentally why material implication is useful in logic. It is not because all conditionals are material implications - they are not. It is because material implication is the object-language connective that corresponds to the classical relationship of entailment. Material implication is useful just because classical logic is useful.

As to what mathematicians do: they are in the business of providing proofs of theorems, which can be represented as Γ ⊢ α. There are many formal systems of calculus that characterize the logical implication relation ⊢. There are Hilbert-style axiom systems, natural deduction systems, Gentzen-style sequent calculus. Many of these include material implication because it is convenient and useful. For example, the axioms of modal logic are expressed using material implication. When mathematicians publish their work, they typically do not put in all the formal logical apparatus because it is a lot of extra work and they can usually be sure that their audience will be familiar with the logic.

Answer 2

Long comment

You can take a look at a simple piece of "real mathematics" and consider how much "formal logic" is implicit in that three lines theorem.

A lot of "classical" propositional logic is implicit in it, without strictly formal propositional calculus at all.

See David Hilbert's The Foundations of Geometry (1899), English translation, Th.1, page 3:

Theorem 1. Two straight lines of a plane have either one point or no point in common [...]

The theorem asserts that two distinct straight lines can have at most one point in common, and can be stated more at length with: let l and m two distinct straight lines; if they have one point P in common, then P is unique.

The proof is by contradiction, using

Ax.I,1: Two distinct points A and B always completely determine a straight line a. We write AB = a.

Answer 3

(This could be better suited as a comment, but my reputation score is too low to add comments)

It might help if you make clearer what you mean by "logical implication": do you refer to another formalization of some rules of logic, or to the inner activity of the mathematician?

Although when you say

most theorems are not even proved formally, since mathematicians still today prove their theorems essentially in the same way as they did before mathematical logic and the introduction of the material implication

one can convene with you, it is true on the other side that most working mathematicians nowadays believe that proofs can be formalized in a calculus, typically one involving material implication.

If your intent is criticizing the stance by which one says "Mathematics is a game of formal objects within the formal rules of logic", then you might be interested in Intuitionism (see e.g. https://plato.stanford.edu/entries/intuitionism)