# Is a proof by mathematical induction a semantic proof or a syntactic proof?

In logic, an important distinction is made between semantic proofs ( using for example the truth table method) and syntactic proofs ( using for example the natural deduction method).

Remark. Maybe I should not say " semantic proof" or " syntactic proof" but rather semantic method and syntactic method. What I mean is that there are two ways to consider the concept of logical consequence, and therefore, the concept of validity.

My question (1) does the distinction hold in mathematics and (2) if it holds, is it possible to classify the mathematical induction method as purely semantic or purely syntactic.

My reason to doubt is that mathematical induction seems to be a way to test all the possible values of the variable involved in the formula under consideration ( to test an infinite number of possible values). That is the semantic aspect : testing the values is analogous to considering all the possible "interpretations" in logic.

But at the same time, in the second step of the proof, it uses syntactic devices to prove the conditional: if the formula is true for n, then it is also true for n+1. This is analogous to transforming a formula mechanically as it is the case in the syntactic part of logic.

• If we are working in e.g. first-order arithmetic, where the induction schema is a non-logical axiom of the theory, a proof is a derivation of a formula form the axiom by way of logic rules. Thus, in the derivation we can use the induction axiom and "derivation" is a syntactical concept. – Mauro ALLEGRANZA Mar 29 at 7:15
• If we are producing an induction proof in the meta-theory, like using induction on the complexity of formulas to show e.g. that the nuber of left parentheses equals that of right ones, we are not working "in" the calculus but we are producing a "normal" math proof about the objects : formulas. In this case, the dichotomy syntax-semantics is less meaningful. – Mauro ALLEGRANZA Mar 29 at 7:18

It is a very interesting question and I'll try to answer to it.

Prelude.

In what follows I am going to talk about logics in a technical sense, i.e. a logic will be specified by a language (i.e. a set of formulas, presented in some way), a set of inference rules (i.e. possibly partial operations from formulas to into formulas) and satisfiability relation (defined between elements called interpretations and formulas).

The language and the inference rules provide the proof system of the logic while the interpretations and the satisfiability relation provide the semantics of the logic.

From these data we get two different notion of consequence in a logic:

• the first one is the $$T \models \varphi$$, usually called logical consequence, which basically states that every model of $$T$$ (i.e. every interpretation that satisfies the formulas in $$T$$) is also a model of $$\varphi$$
• the second one is $$T \vdash \varphi$$, usually called derivability, which states that there is a proof (in a proof system considered) of $$\varphi$$ which uses as unique assumptions the formulas in $$T$$.

In every good logical systems we have that if $$T \vdash \varphi$$ holds, i.e. if we have a proof of $$\varphi$$ from $$T$$, then $$T \models \varphi$$ holds as well.

In very good logical systems the converse holds too: i.e. if $$T \models \varphi$$ then $$T \vdash \varphi$$ holds too.

In the first case we say that the logic is sound and in the second case that it is complete.

Classical first-order logic is the most well known example of sound and complete system. Classical second-order logic, with Tarski-semantics, is an example of a sound but not complete system.

Let's answer the question. Generally to prove a given formula $$\varphi$$, assuming a set of axioms $$T$$, one has simply to provide a proof of $$\varphi$$ using assumptions in $$T$$, that is one have to prove $$T \vdash \varphi$$. This is what one means by a syntactic proof of $$\varphi$$.

But if you are working in a sound and complete logic you have another way to prove a formula $$\varphi$$: you could prove $$T \models \varphi$$, and then using the completeness of the system you get that $$T \vdash \varphi$$. Methods of this sorts are called semantics because they do not provide directly a proof of $$\varphi$$, but they provide a proof indirectly via compleness, by proving properties of the interpretations of $$T$$ and $$\varphi$$.

(1) does the distinction hold in mathematics?

Absolutely. The syntactic and semantic methods are different: one work by providing the proof of the statement the other one provide indirectly the proof via a compleness result. Also, semantic methods have a limited application in not complete systems: because in these system you cannot turn logical consequence into derivability, hence you may not get automatically a proof.