Math proof vs Logic Proof.

Question

I am trying to learn math "from scratch" and started by reading an introductory logic textbook (A Concise introduction to logic) that did a great job explaining predicate logic. Among other things, proofs, that is, syntactic string manipulation where from a set of premises P, via a number of inference rules, a new statement, aka conclusion C, can be derived.

I am now profoundly stuck trying to make the leap to mathematical proofs. And here is where. The first introductory proof I saw looks like the following:

Slide 42 from here

But how does this connect to predicate logic? The predicate logic proofs begin with premises and here the theorem to be proven looks like the conclusion but no premises are given. Which I can understand: in propositional logic, a theorem is "a sentence that can be derived without premises" (ctrl + f for "theorem" here).

But where do I go from here?

I can rewrite the theorem in predicate logic like the following

But how can I go about proving it? The techniques in the textbook call for a sequence of conditional derivations and I would guess some universal instantiation or generalizations.

What am I missing to connect these 2 proofs? What is the link between a predicate logic proof and a math proof written in English?

I see that there is a square function involved that can be thought of as a relation (a form of predicate) and Even(x) is also a predicate, but aside from that i see no clues.

The math proof almost feels like a different underlying language and the predicate logic is like its skeleton that can not really be used here. Is that a valid notion?

Proving in math almost feels like using rules of arithmetic to get a matching definition while proving in predicate logic is more about producing a new string from the existing ones.

I see how this is a lot of thoughts pointing in potentially different directions but I am hoping that someone more experienced could notice/relate to the struggle and point me in the right direction.

Thank you everyone!

I believe my question is similar to the mathematical proof vs. first-order logic deductions but I did not find anything to answer my particular example.

Answer 1

Adding to Ethan's answer and specifically addressing your questions:

The predicate logic proofs begin with premises, and here the theorem to be proven looks like the conclusion but no premises are given. Which I can understand: in propositional logic, a theorem is "a sentence that can be derived without premises".

A mathematical theorem is premised ultimately on mathematical axioms and an interpretation of its mathematical symbols. The axiom system and background toolkit (definitions, rules, laws, lemmas, other theorems) is tacit. This is in contrast to pure theorems, which are logical validities/truths; here, the adjective 'logical' is not merely indicating that the statement is logically derivable, but that it is true regardless of interpretation.

Proving in math almost feels like using rules of arithmetic to get a matching definition

Quibble: proofs derive results, not definitions.

$$\forall n.\,(n\in\mathbb N\to(\text{Even}(n)\leftrightarrow\text{Even}(n^2)))\tag0$$

Correction: see $(2)$ below.

What is the link between a predicate logic proof and a math proof written in English?

Proof: Pick an arbitrary even integer $n.$ We need to show that $n²$ is even.

Here, the author means that $$(n\in\mathbb Z \land \text{Even}(n))\to \text{Even}(n^2)\tag1$$ logically implies $$n\in\mathbb Z\to(\text{Even}(n)\to\text{Even}(n^2)),$$ and that invoking universal generalisation then gives the required result $$\forall n\;(n\in\mathbb Z\to(\text{Even}(n)\to\text{Even}(n^2))).\tag2$$ So far, no mathematics has been performed yet.

Since $n$ is even, there is some integer $k$ such that $n = 2k.$

Here, the author is using multiplication, an arithmetical operation, and invoking the definition of "even number", that is, what it means for the predicate Even$(n)$ to be true/false.

This means that $n^2 = (2k)^2= 4k^2 = 2(2k^2).$ From this, we see that there is an integer $m$ (namely, $2k^2$) where $n^2 = 2m.$ Therefore, $n^2$ is even,

Here, the author is also using exponentiation, another arithmetical operation, and informally—which is not to say unrigorously—proving statement $(1).$ Conditional introduction, existential instantiation and generalisation, etc. are all implicit.

which is what we wanted to show. ■

P.S. That period/colon/comma suffixing the quantifier in $(0)$ potentially introduces ambiguity (though not in $(0)$ itself as it is thoroughly parenthesised): $$∀x\, Px\to Q,$$ due to the precedence convention of logical symbols, definitely means $$(∀x\, Px)\to Q,\tag{A}$$ while in $$∀x. Px\to Q,$$ is the '.' merely superfluous or intended as a delimiter like so $$∀x\, (Px\to Q)\;?\tag{B}$$ $(\text A)$ and $(\text B)$ are logically inequivalent.

Answer 2

I think what you call a "math proof" is best described as an argument that will convince another person of the truth of a particular mathematical assertion about numbers or shapes or other structures mathematicians define and think about.

Those arguments are written in ordinary English (or other natural language) augmented by some mathematical symbols as appropriate.

The level of detail required to be convincing depends on the amount of mathematical knowledge the reader and the writer share.

There is no need to translate those arguments into formal statements in predicate logic. In fact, that is usually a bad idea since it can obscure the mathematical meaning you want to convey.

My personal opinion is that focusing on predicate logic in a first course in "how to write proofs" is counterproductive. I tell my students in that course that a good proof is one that convinces me that you have convinced yourself for good reasons.

Answer 3

I like to think of mathematical proofs as convincing the audience that there is a syntactic string manipulation type proof of the statement, and to give guidance as to how to construct that proof. For the example proof you give, you can start with:

$\forall n: even(n) \implies \exists k: n = 2k$, the definition of $even(n)$

and then use that $\forall a: \forall b: a = b \implies a^2 = b^2$ (which maybe you're going to want to prove from even simpler foundations) and then some tricks with the quantifiers to get:

$\forall n: even(n) \implies \exists k: n^2 = (2k)^2$

Depending on the exact syntactic system you're working in, the exact process of unpacking this proof-in-words will be slightly different, but the template will be the same: just follow the steps in the proof-in-words.

If you're interested in purely syntactic proofs, here's a proof of a similar fact at metamath: https://us.metamath.org/mpeuni/mulsucdiv2z.html

Answer 4

Nobody mentioned proof assistants: Coq, Agda, Idris, Isabelle, etc.
https://en.m.wikipedia.org/wiki/Proof_assistant

They show that, yes, it is possible to completely formalize a proof to the point that it can be mechanically checked, and that some mathematicians actually did it for some very complex proofs (in Coq: the four color theorem; the Feit-Thompson theorem).

But they also show that using such perfectly formal languages is greatly unproductive, requires a lot of specific training, and produces proofs that are a lot less readable than plain english proofs. Also, they put forward a lot of differences and subtleties between various logics and type theories, that non-specialists (i.e. mathematicians that are not logic specialists) would rather ignore.

Some mathematicians like Voevodsky have concluded - after some bitter personal experience - that long, complex proofs are too error-prone, and must be checked by computarized means. But Voevodsky was also negative about the usability of predicate logic for computerized proofs, felling that predicate logic was too low-level. That would be like designing complex software in Assembly language. This was the main driver of his researches after 2000.
https://www.ias.edu/ideas/2014/voevodsky-origins

---

As a personal taste, I like epsilon-delta kinds of proofs. Difference between continuity and uniform continuity is much clearer when fully written with quantifiers, than in plain English. But that's somewhat a narrow case.