Provable formulas in everyday Mathematics

Question

Basically all statements ( lemmas, theoremas, corollaries ) in Mathematics can be expressed as a conditional statement in first-order language, or existential statement ( existence proofs ). Here i'm interested in the conditional statements case.

Every theorem mostly has assumptions $A_1, A_2,.., A_n$ and a conclusion $C$ ( even if it involves a bi-conditional, we can split into two cases ) . We can join all assumptions into one single formula $A = A_1 \land A_2 \land ... \land A_n$, and simply consider a theorem as a conditional statement $A \rightarrow C$.

To have a proof of the theorem represented by $A \rightarrow C$ is to be able to deduce $C$ from $A$, that is, obtain a finite list whose elements are either $A_1, A_2,.., A_n$, a tautology in first order language ( an axiom ) or some formula obtained by applying some rule of inference from two preceding formulas in the list ; the last element in the finite list is $C$.

Now, we learn that first order logic is sound and semantically complete, so we can conclude that every provable formula ( theorem ) is a tautology in first order language, and at the same time we learn ( by Deduction Theorem ) that if $C$ was deduced from $A$, then $A \rightarrow C$ is provable ( we were proving $A \rightarrow C$ is a tautology in first place).

While i understand that $A \rightarrow C$ must be a tautology, when we say every theorem ( from any branch of mathematics, number theory, abstract algebra, real analysis,etc ) we prove is simply a conditional formula $A \rightarrow C$ that is provable, are we saying it's provable from which set of axioms ?

Since the idea of a formula being provable, requires some set of axioms which the formula can be proved from, how do we understand that every tautology in first order logic is provable ?

Thanks in advance

Answer 1

I think that you have made a little mistake; we need some precise definitions.

Consider first-order logic and a "standard" proof system for it; i.e.logical axioms + inference rules (a so-called Hilbert-style proof system; see Elliott Mendelson, Introduction to mathematical logic (4ed - 1997) or Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001); for natural deduction, thinghs are a little bit different [more rules, no logical axioms], but the basic concepts are the same; see Dirk van Dalen, Logic and Structure (5th ed - 2013) or Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007)).

Note. Mendelson uses two inference rules : modus ponens and geenralization, while Enderton uses only modus ponens.

We have to start from the definition of deduction form assumptions [see Enderton, page 111] :

A deduction of $\varphi$ from $\Gamma$ is a finite sequence $(\alpha_0, ... \alpha_n)$ of formulas such that $\alpha_n$ is $\varphi$ and for each $k \le n$, either

($a_1$) $\alpha_k$ is in $\Gamma$, or

($a_2$) $\alpha_k$ is in the set $\Lambda$ of logical axioms, or

($b$) $\alpha_k$ is obtained by modus ponens from two earlier formulas in the sequence; that is, for some $i$ and $j$ less than $k$, $\alpha_j$ is $\alpha_i \rightarrow \alpha_k$.

If such a deduction exists, we say that $\varphi$ is deducible from $\Gamma$, or that $\varphi$ is a theorem of $\Gamma$, and we write $\Gamma \vdash \varphi$.

Consider now, your example : "a proof of the theorem represented by $A \rightarrow C$ is to be able to deduce $C$ from $A$".

In this way, we obtain a deduction of $C$ from the assumption $A$ :

$A \vdash C$.

Of course, in the above deduction, we have used also the set $\Lambda$ of (logical) axioms.

Then we apply Deduction Theorem to get :

that if $C$ was deduced from $A$, then $A \rightarrow C$ is provable, i.e. $\vdash A \rightarrow C$.

By soundness, we conclude that $A \rightarrow C$ is a (first-order) valid.

See this post for more details.

Consider now a finite set of sentences $\Gamma = \{ \gamma_1,... , \gamma_n \}$. Then, as you said :

we can join all assumptions into one single formula $G = \gamma_1 \land \gamma_2 \land ... \land \gamma_n$, and simply consider a theorem as a conditional statement $G \rightarrow \varphi$.

For example, consider Group theory [see Mendelson, page 71].

$G$ is the conjunction of the (finite) list of first-order axiom of group theory.

Now, let $\varphi$ be a theorem whatever of group theory; from the consideartions above, we have :

$G \vdash \varphi$,

from which we conclude :

$\vdash G \rightarrow \varphi$.

The last one is a valid formula of first-order logic; that is it is true in every interpretation. This is consistent with mathematical practice: if we consider a structure that is a group, this will obviously satisfy group axioms, i.e. $G$.

Being $\varphi$ a tehorem of group theory, by soundness it will be a logical consequence of $G$, i.e. it will be true in every interpretation that satisfy $G$. In conclusion, $G \rightarrow \varphi$ will be true in every interpreattion, i.e.valid.

But this does not imply that $\varphi$ is valid, because it is not a theorem of first-order logic.

In conclusion,

$G \rightarrow \varphi$ is a logical theorem (of f-o logic) and thus it is valid.

Instead :

$\varphi$ is a theorem of group theory but not necessarily a logical one; thus, it is not valid.

Added - April,23

Consider Enderton's system (I use it for simplicity, because it has modus ponens as single rule of inference).

The axiom system for f-o logic [see page 112] is :

The logical axioms are then all generalizations of wffs of the following forms, where $x$ and $у$ are variables and $\alpha$ and $\beta$ are wffs:

1. Tautologies;

2. $\forall x \alpha \rightarrow \alpha(t/x)$, where $t$ is substitutable for $x$ in $\alpha$;

3. $\forall x (\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$;

4. $\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$.

In addition, the equality axioms.

Consider the f-o language for number theory [see Enderton, page 70] : an individual constant : $0$, the successor (unary) function : $S$, the two (binary) functions "sum" : $*$ and "product" : $\times$.

With this language we build the following instance of axiom 2 :

$\forall x \lnot (S(x) = 0) \rightarrow \lnot (1 = 0)$;

where we have used as $\alpha$ the formula : $\lnot (S(x) = 0)$ and as $t$ the term : $S(0)$, i.e.$1$.

Being an instance of a first-order axiom, the formula is provable :

$\vdash \forall x \lnot (S(x) = 0) \rightarrow \lnot (1 = 0)$,

i.e.it is a theorem of f-o logic, because we have proved it using (only) f-o logical axioms.

Thus, by soundness is valid (i.e.true in every interpretation).

Consider now the f-o axiom system for number theory [see Enderton, page 203] ; the first one is :

$\forall x \lnot (S(x) = 0)$.

Thus, from the above instance of f-o axiom 2, we have :

$\forall x \lnot (S(x) = 0) \vdash \lnot (1 = 0)$.

In conclusion, $\lnot (1 = 0)$ is a theorem of number theory, because we have proved it (in f-o logic) from the (mathematical) axioms of f-o number theory.

This theorem is not valid; it is a logical consequence of the mathematical axioms of number theory; thus, it will be true in every structure which satisfy f-o number-theory axioms.