Studeny says in the abstract of his 1992 paper that:
However, under the assumption that CIRs [conditional-independence relations] are grasped the existence of a countable characterization of CIRs is shown.
Since Studeny seems to be calling a "complete finite axiomatization" a "finite characterization", this seems to suggest that Studeny is even claiming/asserting that he has shown a complete countable axiomatization of conditional independence.
Question: Is this correct? Has Studeny or anyone else shown the existence of a complete countable axiomatization of conditional independence? (Soundness is not in dispute.)
Studený has, for discrete random variables. What has been called "CIRs" or "stochastic/probabilistic CI models" at that time was a CI relation (a set of formal triplets $\langle A,B|C\rangle$ representing conditional independence statements) realized by a discrete probability distribution. Afterwards, more specific (binary) or simply different (regular Gaussian) probabilistic realizations of CIRs have been considered as well. You already mentioned Sullivant's paper. Or around the same time, Šimeček.
What Studený claimed to have constructed is a countable axiomatization of the collection of all CIRs which are realizable by discrete probability distributions, using only Horn clauses (which he calls "$\square$ (inference) rules").
I work more on the Gaussian side, so for my peace of mind I will allow myself to emphasize "discrete [realizable] CIR" where applicable below. But for consistency with the article, I will continue to use the symbol $\mathsf{CIR}(N)$ to stand for discrete realizable CIRs.
Later in the introduction, Studeny seems to possibly demur, saying only:
The main result is proved in the fourth section. It is supplied by the construction of a countable characterization of CIRs by $\square$ properties (however applicable only in the case that all CIRs are grasped). The fifth description is devoted to a syntactical description of CI [conditional independence]. We show how a formal axiomatization for CI can look and show that no simple complete deductive system for CI exists.
In particular, I don't understand the condition "all conditional independence relations are grasped", nor whether the mentioned formal axiomatization is complete, or just sound, nor what is meant by a "simple complete deductive system" (as opposed to more general complete deductive systems).
Neither Studený nor I are native speakers, but I believe he meant by "only in the case that all CIRs are grasped" that he provides a procedure which converts a complete list of all discrete realizable CIRs (evidently a countable set up to relabeling of the ground sets) into a countable sound and complete axiomatization using Horn clauses. Given that the conjecture being refuted in this paper was that the semigraphoid properties are sound and complete, which would yield the holy grail of knowing all discrete CIRs, it seems sensible to me that he would stress that this countable axiomatization suffers from a chicken and egg problem: if you know all the discrete CIRs, you can derive an axiomatization, but the axiomatization was sought originally to know all the discrete CIRs.
In computational terms, the problem of writing down a complete axiomatization of discrete CIRs Turing-reduces to the problem of deciding when a CIR is realizable by a discrete distribution. The converse is easy to prove, so the two problems are Turing-equivalent. With respect to Spohn's hope of a recursive axiomatization that you quoted, I should note that, to my knowledge, this question is still open. Realizability and the implication problem are equivalent, but neither is known to be decidable.
I am not aware of any alternative reference for the claimed Turing reduction and I think the primary one is alright, so I will explain the proof in different words here.
The case of a fixed ground set
Construction of the axioms. The critical result is Proposition 2 in the aforementioned paper. Given the list $\mathsf{CIR}(N)$ of discrete realizable CIRs on a fixed ground set $N$, we can iterate through all CIRs $J$ on $N$ which are not discrete realizable. Because discrete CIRs are closed under intersection (Lemma 1), there is a unique smallest $\overline J \in \mathsf{CIR}(N)$ which extends $J$. For each CI statement $c \in \overline J \setminus J$ we add one axiom $\bigwedge_{a \in J} a \rightarrow c$ to our list. This axiom is sound because all discrete CIRs on $N$ containing $J$ contain $c$ by the choice of $\overline J$. The axioms for $J$ we just added force $J$ to be closed to $\overline J$, effectively forbidding $J$. If we do this for all non-discrete CIRs on the given ground set, our list of axioms will surely be complete for the finite set $\mathsf{CIR}(N)$. Moreover, it consists only of Horn clauses.
Context preservation. Let's call this set of inference rules $\mathsf{Ax}(N)$. Due to the structure of discrete CIRs, it has a subtle property that will be important in the final step of the proof. Namely, when $\bigwedge_i \langle A_i,B_i|C_i\rangle \rightarrow \langle X,Y|Z\rangle \;\in \mathsf{Ax}(N)$, then this axiom "respects context", in that $X\cup Y\cup Z \subseteq \bigcup_i A_i\cup B_i\cup C_i$. Because if that were not the case, Lemma 4 contains a construction of a discrete CIR on $N$ which contains the antecedents but not the consequent, contradicting, by intersection-closedness, our choice of minimal $\overline J$ in the construction of the axiom.
Locality of consequents. This property means that when we consider a set of antecedents $\langle A_i,B_i|C_i\rangle$, we will find all the consequents of them appearing in any $\mathsf{Ax}(N)$ already just by studying discrete CIRs on the "smallest possible" ground set $N' = \bigcup_i A_i\cup B_i\cup C_i$. This is because on the one hand discrete CIRs are closed under restrictions of their ground sets (by the operation of marginalization on their realizing distributions), so making the ground set smaller does not make more consequents available for a fixed set of antecedents. On the other hand we do not lose any consequents either because if that were the case, i.e. $\bigwedge \langle A_i,B_i|C_i\rangle \rightarrow \langle X,Y|Z\rangle \; \in \mathsf{Ax}(N)$ and $\overline{J'} \in \mathsf{CIR}(\bigcup_i A_i\cup B_i\cup C_i)$ contained all the antecedents but not the consequent, then Lemma 3 (a) allows us to lift $\overline{J'}$ to a discrete CIR on $N$ which still contains the antecedents but not the consequent, contradicting, again by intersection-closedness, the existence of the axiom in $\mathsf{Ax}(N)$.
The case of all discrete CIRs
About ground sets. This was the story for a fixed finite set $N$, but the objective is the collection of all discrete CIRs irrespective of their ground set. Because discrete CIRs don't care how we name and order their ground sets (they are closed under permutations), let us restrict ground sets to all finite subsets of the natural numbers. Then we can consider CIRs uniformly as finite sets of triplets $\langle A,B|C\rangle$ where $A$, $B$ and $C$ are finite, disjoint subsets of $\mathbb{N}$. Notice that there are only countably many of those. Studený accounts for this trouble of choosing ground sets in his definition of $\square$ rule on page 3.
The proof. For each of these countably many finite subsets $N$ of the natural numbers, we simply concatenate the "locally sound and complete" axioms $\mathsf{Ax}(N)$. I claim that this yields the desired axiomatization. Certainly it is a countable set of axioms all of which are Horn clauses. Completeness follows because every CIR that is not discrete realizable lives on a finite ground set $N$ and $\mathsf{Ax}(N)$ includes axioms which forbid this CIR by forcing it to close to the smallest discrete realizable CIR above it. To prove soundness, let any axiom $\bigwedge_i \langle A_i,B_i|C_i\rangle \rightarrow \langle X,Y|Z\rangle$ be given, let $N$ be an arbitrary ground set and $I \in \mathsf{CIR}(N)$ which contains all of the antecedents $\langle A_i,B_i|C_i\rangle$. We argued above that the existence of this axiom implies that on the ground set $N' = \bigcup_i A_i\cup B_i\cup C_i$ there is a non-discrete CIR $J' = \{ \langle A_i,B_i|C_i\rangle : i \}$ whose smallest discrete CIR extension $\overline{J'}$ contains $\langle X,Y|Z\rangle$. By restricting $I$ to $N'$ we obtain a discrete CIR $I'$ which contains the antecedents, so $\langle X,Y|Z\rangle \in \overline{J'} \subseteq I'$ by minimality, and hence $I$ must have also contained the consequent. So the axiom is valid.
Summary
- Because CIRs on a fixed ground set are finitely many structures, you find a finite complete axiomatization of the property of being discrete (in the form of a general Boolean formula in CNF, the clauses of which are written as implications).
- By intersection-closedness, Horn clauses suffice.
- When all these axioms are thrown into one bowl forgetting ground sets, closedness under intersections and restrictions guarantee soundness. Completeness is clear.
- In particular the context preserving nature of the axioms is crucial as it allows us to reconstruct the smallest ground set over which this axiom was obtained.
Spohn seems to go on to say that he hopes that at least it can be shown that this axiom family can be written recursively. But Spohn does not seem to mention whether the typical conditional independence axioms (see below) become complete when one replaces the fourth axiom (which corresponds, I think, to the case that $n=4$ in the family given by Studeny above) with Studeny's countable family of axioms. (Which is the only thing I am interested in.)
No, sometime later Studený and Matúš (later Matúš alone) compiled the list of discrete realizable CIRs on four random variables, in a very compressed form (I, II, III, for a summary see Šimeček's Short note). The semigraphoid axioms plus this infinite familiy (of which only the $n=4$ instance applies to this situation) are not sufficient to cut out the CIRs on four discrete random variables.
If you take the semigraphoid closure of the following set of triplets, it will satisfy the semigraphoid axioms (by construction) and all instances of Studený's property (vacuously), but it is not discrete realizable:
$$
\{
\langle 1,2|\emptyset \rangle,
\langle 1,2|3 \rangle,
\langle 2,4|3 \rangle,
\langle 3,4|1 \rangle,
\langle 3,4|1,2 \rangle
\}.
$$
This is not obvious, but you could start by recognizing that the above structure is a local semigraphoid in the sense of Matúš (1997) and that Studený's is a property which actually takes place in the local world. There is no way to order the ground set $\{1,2,3,4\}$ such that the antecedents of Studený's property are contained in this semigraphoid, so the the property is vacuously fulfilled. As for why this local semigraphoid is not discrete realizable, I cannot give you a more profound reason than: it is not an intersection of any subset of the 91 basic discrete CIRs whose 13 orbits modulo the symmetric group on the ground set are displayed in Šimeček's Short note, reference given above.
Instead, in all of the references discussing the conditional independence axioms I have seen so far, only the typical, sound but not complete, axioms are mentioned.
As a followup to the paper you cited, Pearl and Paz revised their conjecture to state that if the semigraphoid axioms are not complete for discrete CIRs, maybe they at least generate all sound CI inference rules with at most two antecedents, which in turn was proved by Studený. To me this is a satisfactory answer for why the semigraphoid axioms prevail. They are "complete for all the smallest valid axioms". You can read more about it in Studený (1994).
