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

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.

• – Mauro ALLEGRANZA Jun 18 '18 at 6:15
• @ZacharySelk My bad. I've edited the tags. Thanks for letting me know. – Ali Jun 18 '18 at 6:31
• We can say "meaning as use": the meaning of connectives is the way we use it and this is defined by the rules of the calculus. – Mauro ALLEGRANZA Jun 18 '18 at 9:21

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.

• Thanks for your answer. So far, I've just been going forward *syntactically and am not comfortable with the concept of true/false. Would you think reading more about semantics would help me make a bridge with intuition or is it unrelated? – Ali Jun 19 '18 at 18:15
• @Ali well your headline question was basically “what is this ‘meaning’ they’re talking about?” And that is exactly what semantics is, so I’d say it’s very much related. Yes, semantics are very important for intuition and you should learn about them. – spaceisdarkgreen Jun 19 '18 at 18:35
• 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.