# Why do axiomatic systems for propositional calculus include IFF axioms?

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.

• If your goal is to minimize the number of axioms and operators, you should stick to the Sheffer stroke with its single axiom and single inference rule. Who needs wasteful luxuries like $\land$, $\lor$, $\neg$, or $\implies$? May 3, 2021 at 0:53
• usually redundant axioms are listed, for example in zfc some of the axioms can be derived from the others May 3, 2021 at 0:56
• The game is not always to minimize the number of axioms and operators. Sometimes (a lot of times?) the game is to maximize human comprehension. This might lead to extra symbols, such as the $\iff$ symbol, which I find quite useful in understanding mathematics. May 3, 2021 at 1:02

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.

• "A second crucial point, is that, as far as modus ponens is the only rule of inference, substitutions of parts of a formula with other formulas, are not allowed in a completely formal proof." In Lukasiewicz's systems and some other authors, substitutions are allowed. Furthermore, they come as required to produce formal proofs of many theorems/theses. May 3, 2021 at 15:58
• "But, in a strictly formal proof, every formula is either an axiom schema, a hypothesis, a repetition of a previews formula or follows from two previews formulas by application of modus ponens. " If you have axiom schema, then you need to instantiate the schema into axioms in order to prove certain theorems. May 3, 2021 at 16:03
• @DougSpoonwood I am talking of substitutions of parts of a formula that are formulas themself. Not of substitutions of the propositional variables with other propositional variables or formulas. I will edit this point to make it more clear. If that is allowed, then modus ponens is not the only rule of inference. For the second comment, I am talking about proofs in propositional calculus, not logic in general. May 3, 2021 at 16:47
• Also, one could note here that p→(q→p) is not an axiom of Jan Lukasiewicz, nor are 2. and 3. as listed above. More importantly they are also NOT a translation from Polish notation to an infix notation with his rules of inference. His rules of inference include a rule of substitution. But, let's substitute p→(r→p) for in p→(q→p). We get p→(r→p)→(q→p→(r→p)) which is an ambiguous mess. Why? Because p→(q→p) isn't a meaningful expression, unlike Lukasiewicz's CpCqp, CCpCqrCCpqCpr, and CCNpNqCqp. May 6, 2021 at 20:52
• @DougSpoonwood Lukasiewicz created more than one system. The one in my answer is in D. Hilbert and W. Ackermann, "Principles of Mathematical Logic", Chelsea Publishing Company, New York 1950. See Ch.1, sec. 10, p. 29. The first two axiom schemata is from Frege's system. Lukasiewicz showed that Frege's system can be replaced by the above. You can also find it in wikipedia. May 6, 2021 at 21:56

"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.

• This is just wrong. Certain ways of defining connectives in terms of others that are commonly used in classical logic are not valid in intuitionistic logic, but others are. In particular, this one is. May 6, 2021 at 20:14
• @EricWofsey Thank you. I forgot the 'not' and have now edited it. May 6, 2021 at 20:28
• @EricWofsey Also, the wiki explicitly says: "As a result, none of the basic connectives can be dispensed with, and the above axioms are all necessary" The above axioms could include an axiomatization of equivalence instead of defining it by other connectives. So, there definitely can exist an intuitionistic logic where no definability of connectives is allowed. You want to talk about an intuitionistic logic where definability of connectives is allowed, well that's just one intuitonistic system. May 6, 2021 at 20:35