Why do axiomatic systems for propositional calculus include IFF axioms?

Question

I am reading : https://en.wikipedia.org/wiki/Propositional_calculus#Axioms, and the following three axioms seemed unnecessary to me: $$ IFF-1 : ( \phi \iff \chi ) \implies (\phi \implies \chi ) \\ IFF-2 : ( \phi \iff \chi ) \implies (\chi \implies \phi ) \\ IFF-3 : ( \phi \implies \chi ) \implies ( ( \chi \implies \phi ) \implies ( \phi \iff \chi ) ) $$ I understand how they would define an $ \iff $ operator, but wouldn't you always be able to substitute $(\phi \implies \chi) \land (\chi \implies \phi)$ for $ (\phi \iff \chi) $ in any proof? From $(\phi \implies \chi) \land (\chi \implies \phi)$ and the three $\land$ axioms you can recover the three $\iff$ axioms. In this scheme $ (\phi \iff \chi) $ in proofs would be notation for ($\phi \implies \chi) \land (\chi \implies \phi)$. You would end up with an equivalent notion with three fewer axioms and one fewer operator in the system.

Answer 1

Firstly, let us make clear that there are many different but equivalent sets of axiom schemata for propositional calculus, which serve the same purpose: from them, we can prove the same theorems. Some of them include only the least possible number of axiom schemata. Others have redundant axiom schemata, that can be proved from the rest and thus, are not really necessary. However, there is a subtle point here: you have to introduce more axioms, in order to include in a formal language, more primitive symbols, like logical connectives. For example, see the following set of axioms, from Jan Łukasiewicz:

1. $p\rightarrow\left(q\rightarrow p\right)$
2. $\left[p\rightarrow\left(q\rightarrow r\right)\right]\rightarrow\left[\left(p\rightarrow q\right)\rightarrow\left(p\rightarrow r\right)\right]$
3. $\left(\neg p\rightarrow\neg q\right)\rightarrow\left(q\rightarrow p\right)$

From these three schemata and using modus ponens as the only inference rule, one can prove all the tautologies of propositional calculus. There is no redundant axiom schemata here. If any of them is removed, the system will not work. Note that only two logical operations are used in the system: negation "$\neg$" and material implication "$\rightarrow$". The other usual logical operation symbols, could be seen as abbreviations:

• Conjunction "$p\wedge q$" is an abbreviation for "$\neg\left(p\rightarrow\neg q\right)$".
• Disjunction "$p\vee q$" is an abbreviation for "$\neg p\rightarrow q$".
• Biconditional "$p\leftrightarrow q$" is an abbreviation for "$\neg\left[\left(p\rightarrow q\right)\rightarrow\neg\left(q\rightarrow p\right)\right]$".

Etc. A crucial point here, in respect of your question, is that abbreviations do not belong to the formal language. One can use these symbols in order to make an expression or a proof more readable and shorter. However, a strictly formal expression, does not include them.

For another example, lets take J. Barkley Rosser's system:

1. $p\rightarrow p\wedge p$
2. $p\wedge q\rightarrow p$
3. $\left(p\rightarrow q\right)\rightarrow\left[\neg\left(q\wedge r\right)\rightarrow\neg\left(r\wedge p\right)\right]$

Again, modus ponens is the only inference rule and there are not any redundant axiom schemata. We see three logical operations here. However, in Rosser's system, only negation and conjunction are primitive symbols, while material implication is informal:

• "$p\rightarrow q$" is an abbreviation for "$\neg\left(p\wedge\neg q\right)$".
• "$p\vee q$" is an abbreviation for "$\neg\left(\neg p\wedge\neg q\right)$".
• "$p\leftrightarrow q$" is an abbreviation for "$\neg\left(p\wedge\neg q\right)\wedge\neg\left(q\wedge\neg p\right)$".

Rosser's axiom schemes, in the formal language of his system, should look like this:

1. $\neg\left[p\wedge\neg\left(p\wedge p\right)\right]$
2. $\neg\left[\left(p\wedge q\right)\wedge\neg p\right]$
3. $\neg\left[\neg\left(p\wedge\neg q\right)\wedge\neg\neg\left[\neg\left(q\wedge r\right)\wedge\neg\neg\left(r\wedge p\right)\right]\right]$

Also, modus ponens should look like this: $$\dfrac{\begin{array}{c}\neg\left(p\wedge\neg q\right)\\p\end{array}}{q}$$

Now, if you need more primitive logical connectives, you need more axiom schemata also. Stephen Cole Kleene proposes the following 13 axiom schemata for all the usual connectives $\neg$, $\wedge$, $\vee$, $\rightarrow$ and $\leftrightarrow$:

1. $p\rightarrow\left(q\rightarrow p\right)$
2. $(p\rightarrow q)\rightarrow\left(\left[p\rightarrow(q\rightarrow r)\right]\rightarrow(p\rightarrow r)\right)$
3. $(p\rightarrow q)\rightarrow\left[(p\rightarrow\neg q)\rightarrow\neg p\right]$
4. $\neg\neg p\rightarrow p$
5. $p\rightarrow(q\rightarrow p\wedge q)$
6. $p\wedge q\rightarrow p$
7. $p\wedge q\rightarrow q$
8. $p\rightarrow p\vee q$
9. $q\rightarrow p\vee q$
10. $(p\rightarrow r)\rightarrow\left[(q\rightarrow r)\rightarrow(p\vee q\rightarrow r)\right]$
11. $(p\rightarrow q)\rightarrow\left[(q\rightarrow p)\rightarrow(p\leftrightarrow q)\right]$
12. $(p\leftrightarrow q)\rightarrow(p\rightarrow q)$
13. $(p\leftrightarrow q)\rightarrow(q\rightarrow p)$

From this Kleene's system, if you don't need the biconditional as a primitive symbol, you can remove schemata 11-13, which are the 3 IFF schemata that you mention in your question. So, you get a shorter set of 10 axiom schemata, for the connectives $\neg$, $\wedge$, $\vee$ and $\rightarrow$. Then again, if you don't need disjunction as a primitive symbol either, then you can also remove schemata 8 and 9. Now, you have a set of 8 axioms for the connectives $\neg$, $\wedge$ and $\rightarrow$. Further more, if you don't need conjunction as a primitive symbol either, then you can also remove schemata 5-7. Now, you have a set of 4 axioms for the connectives $\neg$ and $\rightarrow$. This is as far as you can go, with this system.

A second crucial point, is that, as far as modus ponens is the only rule of inference, substitutions of composite parts of a formula, which contain logical operations, with other formulas, are not allowed in a completely formal proof. Since abbreviations are informal anyway, most writers feel free at any time to replace a formal expression with the abbreviation, or vice-versa. But, in a strictly formal proof, every formula is either an axiom (or an axiom schema, in propotitional calculus), a hypothesis, a repetition of a previews formula or it follows from two previews formulas by application of modus ponens. Thus, unless you have substitution as an inference rule, you can not use it.

However, in order to make things simpler, one could prove the substitution theorem: Let $p_{1},p_{2},...,p_{n},q,r$ be statements and let $w$ be built up out of some or all of the previews, occurring one or more times, by means of the primitive connectives only. Let $v$ be the result of replacing some or all occurrences of $q$ in $w$ by $r$. Then, substitution theorem states that:

$$\text{If }\vdash w\text{ and} \vdash q\leftrightarrow r\text{, then }\vdash v\text{.}$$

It will take to much space to include the whole analysis here, but the proof of substitution theorem is such that allows you, by following specific rules, to transform a proof which uses the substitution theorem, to a completely strict formal proof, where every formula is either an axiom, a hypothesis, a repetition of a previews formula or follows from two previews formulas by application of modus ponens. Then, one feels confident to write shorter proofs with the help of substitution theorem, knowing that he can get the strict form in any time, with an algorithmic procedure.

Answer 2

"I understand how they would define an ⟺ operator, but wouldn't you always be able to substitute (ϕ⟹χ)∧(χ⟹ϕ) for (ϕ⟺χ) in any proof?"

No. In intuitionistic logic, such substitution is not necessarily allowed, since defining (ϕ⟺χ) in terms of $\land$ and ⟹ is not possible necessarily. Definiability of distinct connectives is not allowed in at least some intuitionistic logical systems.

Also, using definable connectives is sometimes disallowed in proofs. Definition-free proofs would disallow using ((ϕ⟹χ)∧(χ⟹ϕ)) for (ϕ⟺χ) in any proof.