Armstrong's axioms more precisely 'inference rules': what's the distinction?

"more precisely 'inference rules'" is what wikipedia says twice.

Other references I've looked at (the Alice book, Ullman lecture notes cited, Maier textbook) name them as Armstrong's Axioms, use them for inference. talk about axiomatisation and decidability, etc.

Wikipedia's links to axiom vs inference rule isn't helping me. "a rule of inference's action is purely syntactic, and does not need to preserve any semantic property:" Ok I can see that for (for example) modus ponens: it wants a premise like $p \supset q$ and a premise looking like $p$.

Hmm take the Armstrong Axiom of reflexivity

If $X$ is a set of attributes and $Y$ is a subset of $X$, then $X$ holds $Y$.

If $Y \subseteq X$ then $X \rightarrow Y$.

How to determine syntactically that $Y \subseteq X$?

So what is wikipedia trying to say? What distinguishes an axiom (which might be of the form $p \supset q$) vs an inference rule?

• – D.W. Mar 27 '18 at 15:21
• Please state the question in the title. – reinierpost Mar 27 '18 at 22:24

First, terminologically, "axiom" and "inference rule" are often used as roughly interchangeable as they tend to serve similar purposes. There are technical distinctions, which themselves can vary slightly, but outside the study of formal logic or related systems, these distinctions aren't that important.

In the context of formal logic, an axiom is a formula of the logic that is a theorem by definition. A rule of inference is a way of deducing new theorems from old theorems. Rules are always part of the logic, while axioms are separated into logical axioms, which are viewed as part of the logic, and non-logical axioms, which are viewed as part of the particular theory you are studying within the logic. Many logical axioms can be presented as rules and vice versa. For example, the axiom $P\supset(Q\supset P)$ roughly corresponds to the rule of weakening $\cfrac{\Gamma\vdash P}{\Gamma,Q\vdash P}$.

From a meta-logical perspective, rules of inference can be viewed as (definitional) axioms about the logic being studied (not to be confused with the "formal" axioms within the logic. Philosophically, "believing" in the conclusions of a logical theory requires "believing" the rules of inference just as much as "believing" the axioms.

So are Armstrong's "Axioms" axioms or rules of inference? It depends on how you formalize them. The "axioms" strongly suggest a deductive system, i.e. a system of rules, and that deductive system is quite useful in actually calculating functional dependencies. But, we could just as well take $\to$ and $\subseteq$ as relation symbols in a first-order theory and then the "axioms" really would be non-logical axioms of that theory. This could be viewed as meta-logical axioms about the deductive system, but it can just as reasonably be viewed as axiomatizing what "functional dependency" means without any deductive system in mind.

As for how to determine if $Y\subseteq X$ if we do indeed take a deductive system view of Armstrong's Axioms, in this context $X$ and $Y$ are meta-variables that stand for sets of attributes. They would be instantiated with expressions like $\{\mathsf{name},\mathsf{address}\}$. So for the rule you referenced, you'd simply be able to calculate that $\{\mathsf{name}\}\subseteq\{\mathsf{name},\mathsf{address}\}$ and $\{\mathsf{age}\}\not\subseteq\{\mathsf{name},\mathsf{address}\}$. An algorithm to calculate this could be formalized as a collection of inference rules itself, but there is no reason to do this. We can just assume that it can, in fact, be calculated. Obviously it can be in the intended use-case where the "sets" are explicitly presented, finite sets of elements with decidable equality.

Even for modus ponens, we have $P$ and $Q\supset R$ and we can apply modus ponens if $P=Q$, but checking the (syntactic) equality of two formulas while not hard is not completely trivial. Indeed, weakening is often presented with a rule like $\cfrac{\Gamma\vdash P\qquad \Gamma\subseteq\Delta}{\Delta\vdash P}$ and it is just understood that you can, in fact, calculate whether one set of formulas is a subset of another. It may also be presented as $\cfrac{\Gamma\vdash P}{\Gamma\cup\Delta\vdash P}$ where, again, it is just assumed that you have some way of calculating $\Gamma\cup\Delta$.

• Thank you @Derek, that makes perfect sense. So the reason for calling them 'inference rules' might be that X, Y are strictly speaking meta-variables. – AntC Mar 28 '18 at 1:19
• This explains neither what an axiom is nor what a rule of inference is so it's not clear why you think it is going to clarify things. – philipxy Mar 28 '18 at 13:25
• @philipxy I explicitly disclaim doing so in the first paragraph. Whether you call Armstrong's Axioms "axioms" or "rules" doesn't really matter as long as you understand what they are saying and how to calculate with them. In the context of database theory, the distinction between "axioms" and "rules" is rarely, if ever, going to matter. Nevertheless, you are right, it is a major focus of the question that I just brushed aside, so I will add some more text about that. – Derek Elkins Mar 28 '18 at 18:43
• Thank you again for the additions. I came at this from considering the FOL corresponding to A's axioms given some relation predicate P(a, b, c, d) and a FOL expression for the FD {a, b} → {c, d}. Then A's axioms are just logical consequences of the FD. Interpreting the meta-variables into FOL got me stumped. – AntC Mar 28 '18 at 23:29
• @AntC A's axioms are consequences of FDs holding, but only trivially, because they are true regardless of any FD holding or not holding. Because each of A's axioms states that certain things follow from FDs that are things that follow from them. You don't need to assume A's axioms, because you can prove A's axioms from nothing (like A did) & because assuming them plus given FDs doesn't entail any more than what the FDs already entail. But A's axioms have been chosen so that certain repeated plugging in of given & derived FDs gives all & only the derivable FDs that hold when the given ones do. – philipxy Mar 29 '18 at 3:58