How Do We Distinguish between (Logical) Axioms and Other Assumptions of a Proof?

Question

While I was studying Propositional Calculus from Elliott Mendelson's book of Introduction to Mathematical Logic, in the section of Formal Theory I came across a notation $\Gamma$ that represents a set of well-formed formulas (wfs) in a statement that is phrased as follows:

A well-formed formula (wf) $\mathscr{C}$ is said to be a consequence of a set $\Gamma$ of wfs if and only if there is a sequence $\mathscr{B_1,...,B_k}$ of wfs such that $\mathscr{C}$ is $\mathscr{B_k}$ and, for each $i$;

• either $\mathscr{B_i}$ is an axiom,
• $\mathscr{B_i}$ is in $\Gamma$,
• $\mathscr{B_i}$ is a direct consequence of some of the preceding wfs in the sequence by some rule of inference.

Question (1): What separates axioms from the elements of set $\Gamma$? In other words, why can we not say axioms are elements of $\Gamma$? In that case axioms are not wfs? (P.S. I need an example that illustrates this fact in which an axiom that is not an element of $\Gamma$.)

Answer 1

This is just because we prefer to say that

"$n$ is composite" is a consequence of "$n$ is even" and "$n>2$"

than to say that

"$n$ is composite" is a consequence of "$n$ is even" and "$n>2$" and the Peano axioms and the axioms of Zermelo-Frenkel set theory and the Hilbert axioms of propositional logic.

Answer 2

As far as this concrete definition of "consequence" goes, logical axioms and members of $\Gamma$ indeed play the same role.

The reason for distinguishing between them is that there are other contexts where we're only interested in $\Gamma$ and where the logical axioms are considered to be an "internal detail" in the definition of "consequence".

As one important example, one can show that your definition is equivalent to this "semantic" definition of consequence:

$\mathscr C$ is a consequence of $\Gamma$ if and only if every truth assignment that makes every element of $\Gamma$ true, also makes $\mathscr C$ true.

This correspondence would not work if we required all of the necessary logical axioms to be part of $\Gamma$.

And even if we just look at "syntactic" definitions there are different proof systems for the propositional calculus that happen to produce the same consequence relation as the Hilbert system that Mendelson is presenting. These proof systems have their own logical axioms (or none at all), so again the different systems only give the same correspondence if we don't insist of having the logical axioms in $\Gamma$.

---

An important case of this is when $\Gamma$ is the empty set. Then you only have the logical axioms to work with, but you can still prove that some formulas are consequences of the empty set, such as $$(A\to B)\lor(A\to C)\to (A\to (B\lor C))$$ You will need several axioms to prove this, and neither of them will be elements of $\Gamma$ in this case.

On the other hand, we can also let $\Gamma_2$ consist of $A$ and $D$ and $(A\to B)\lor(A\to C)$, and show that $B\lor C$ is a consequence of $\Gamma_2$. The proof will need to use both some logical axioms and some of the assumptions in $\Gamma_2$, but those assumptions are certainly not axioms.

---

When we distinguish between logical axioms and other assumptions, the idea is that the logical axioms are something that are part of the logic -- that is, they're really there to fix what the logical symbols like $\land$ and $\lor$ and $\to$ mean -- whereas the other assumptions are things you select from case to case when you apply the logic to a particular reasoning. Then you can assume you already know how the logical symbols work, and the additional assumptions can just use them to speak about how the non-logical symbols (which at this level are just the propositional letters) relate to each other.

Somewhat confusingly, the "other assumptions" are often also called "axioms" when we view things from a different level of abstraction. One can avoid some of the confusion by calling them "non-logical axioms".

If you select a particular $\Gamma$ containing non-logical axioms, these ought to have the same logical consequences no matter which proof system for (classical) propositional calculus your select. From a birds-eye perspective you can then ignore the details of the proof system.

Answer 3

"What separates axioms from the elements of set Γ?"

Nothing. In fact, some axioms must exist in Γ for a proof to exist.

"In other words, why can we not say axioms are elements of Γ?"

There's no reason not to say that axioms are elements of Γ.

"In that case axioms are not wfs? "

No, axioms ARE wfs. In fact, they must be wfs by Mendelson's definition of a proof. Also, all axioms satisfy the formation rules.

That also indicates why there is not a single formal proof in Mendelson's book. The text is littered with a constant confusion of the notion of a formal and an informal proof actually. Mendleson never actually even writes the wfs, let alone the axioms that he would logically use. But I guess he wasn't able to do that or no one bothered to inform him that he didn't follow his own definition of formal proof.