The intuitive meaning of "or" and "implies" in axiom schemes of a logical theory

Question

In a Hilbert-style system, the axiom schemes can be written as (From Bourbaki, Book I):

S1. If $A$ is a relation in $\mathscr C$, the relation $(A\text{ or }A) \Rightarrow A$ is an axiom of $\mathscr C$ (*).

S2. If $A$ and $B$ are relations in $\mathscr C$, the relation $A \Rightarrow (A\text{ or }B)$ is an axiom of $\mathscr C$.

S3. If $A$ and $B$ are relations in $\mathscr C$, the relation $(A\text{ or }B) \Rightarrow (B\text{ or }A)$ is an axiom of $\mathscr C$.

S4. If $A$, $B$, and $C$ are relations in $\mathscr C$, the relation $$(A\Rightarrow B) \Rightarrow ((C\text{ or }A)\Rightarrow (C\text{ or }B))$$ is an axiom of $\mathscr C$.

Later, they mention that:

Intuitively, the rules S1 through S4 merely express the meaning which is attached to the words "or" and "implies" in the usual language of mathematics.

My questions are:
* What exactly is this "meaning" they are talking about?
* For example, why do we need $(A\text{ or } A) \implies A$ in this particular form? What would happen if it was $(A\implies A)\text{ or } A$ instead. Would this form not convey the "meaning" they are talking about and why?
I would appreciate some examples for one of these schemes that can shed light on how these represent the "or" and "implies" in the usual language of mathematics.

Answer 1

I think Graham's answered your question well, but wanted to add something about the second part. First, we don't need any particular axiom... there are many different possible axiomatizations of propositional logic. The only hard requirement is that the axioms are true, and that there's enough of them to prove everything we want to prove. However, there are good reasons to prefer certain axiomatizations over others.

For instance, taking $(A\to A)\operatorname{or} A$ as an axiom would be a little strange. It does happen to be true, since $A\to A$ is true$.^*$ In fact, $(A\to A)\operatorname{or} B$ is true on the same account and says more. The feature of "or" this captures (provided we can already prove $A\to A$ is true) is that if $C$ is true, then $C\operatorname{or}D$ is true regardless of what $D$ is. While this is a decent property to capture in an axiom, it is probably more elegantly captured by axiom S2 on your list.

So the scheme $(A\to A)\operatorname{or} A$ partially captures this idea in a rather roundabout way, while S2 fully captures it in a direct way.

$^*$ By the way, oftentimes $A\to A$ is taken as an axiom. It is true and captures an important facet of "implies". However in your axiomatization it is not necessary since it can be proven from S2 and S1, as you can show as an exercise.

Answer 2

• What exactly is this "meaning" they are talking about?

"Or" is a connective between two relations indicating "at least one from the two is true".   "Implies" is a connective between two relations indicating a promise that "when the former is true, then the later is true."

• For example, why do we need $(A \mathop{or} A)⟹A$ in this particular form?

It is the statement that "If $A$ is true or $A$ is true, then $A$ is true," which should be rather self-evident.   It is useful though, in that having accepted it once as an axiom allows the proof system to remove redundancy from certain expressions "by axiom S1 and modus ponens" rather than saying "look because this is just what 'or' means" every time.