Equality and the EPL Theorem's Assumptions

In the preceding article I addressed a concern about requirements R2 and R3 used in the EPL Theorem: that if our propositional symbols have internal structure, are in fact FOL ground atoms, then

• this internal structure could implicitly introduce some logical dependency between these symbols above and beyond what is stated in the premise 𝑋 of a plausibility expression (𝐴 | 𝑋) ; and

• that therefore R2 and R3 become questionable.

I showed that there is in fact no such logical dependency introduced in the case of FOL without equality. In this article I address the case of FOL with equality.

FOL with equality

One approach to dealing with equality in FOL is to treat ‘=’ as a special, logical symbol, having a fixed meaning just like ¬ , ∧ , ∨ , etc. have fixed meanings. In this approach, which we’ll abbreviate as FOL=, one defines the semantics of equality via

\(\mathscr{I}[[ (t_{1}=t_{2})]] =\begin{cases} \mathsf{T} & \mbox{if }\mathscr{I}[[ t_{1}]] =\mathscr{I}[[ t_{2}]] \\ \mathsf{F} & \mbox{if }\mathscr{I}[[ t_{1}]] \neq\mathscr{I}[[ t_{2}]] \end{cases} \)

given a FOL interpretation ℐ.

Let’s write ⊨₀ for the entailment relation of propositional logic and ⊨ₑ for the entailment relation of FOL=, based on the truth assignment induced by an interpretation ℐ. The existence of additional logical dependencies introduced by equality manifests as the fact that it is possible for 𝑋 ⊨ₑ 𝐴 to be true even though 𝑋 ⊨₀ A is false; for example, if 𝑡, 𝑡₁, 𝑡₂ are ground terms and 𝑇 is a tautology, then

\(\begin{gather*} T\models_{\mathrm{e}}\left(t=t\right)\quad\mbox{but not}\quad T\models_{0}\left(t=t\right)\\ \left(t_{1}=t_{2}\right)\models_{\mathrm{e}}\left(t_{2}=t_{1}\right)\quad\mbox{but not}\quad\left(t_{1}=t_{2}\right)\models_{0}\left(t_{2}=t_{1}\right) \end{gather*}\)

and this occurs because propositional logic is blind to any internal structure of propositional symbols. (Recall that ground atomic formulas such as (𝑡₁ = 𝑡₂) are, in the context of propositional logic, just propositional symbols.)

Axiomatizing equality

With FOL= there’s some implicit information regarding atomic formulas involving ‘=’ that isn’t spelled out in one’s premises, and if you’ve read my previous articles you know what comes next: such implicit information must be made explicit in the premise 𝑋 of a plausibility expression (𝐴 | 𝑋) .

This brings us to the other way of dealing with equality in FOL: include explicit axioms for equality. One such standard axiomatization is the following:

• ER: Equality is reflexive (every value is equal to itself).

  \(\forall x.\,(x=x)\)

• ES: Equality is symmetric (order of arguments doesn’t matter).

  \(\forall x.\forall y.\,\left(x=y\right)\rightarrow\left(y=x\right)\)

• ET: Equality is transitive.

  \(\forall x.\forall y.\forall z.\,\left(x=y\right)\rightarrow\left(y=z\right)\rightarrow\left(x=z\right)\)

• EF(𝑓): Equals are substitutable in function application. For every 𝑛 > 0 and every 𝑛 -ary function symbol 𝑓, we have the axiom

  \(\begin{multline*} \forall x_{1}\cdots\forall x_{n}.\forall y_{1}.\cdots\forall y_{n}.\\ \left(x_{1}=y_{1}\right)\wedge\cdots\land\left(x_{n}=y_{n}\right)\rightarrow\\ \quad\left(f\left(x_{1},\ldots,x_{n}\right)=f\left(y_{1},\ldots,y_{n}\right)\right) \end{multline*}\)

• EP(𝑝): Equals are substitutable in predicate application. For every 𝑛 > 0 and every 𝑛-ary predicate symbol 𝑝, we have the axiom

  \(\begin{multline*} \forall x_{1}\cdots\forall x_{n}.\forall y_{1}.\cdots\forall y_{n}.\\ \left(x_{1}=y_{1}\right)\wedge\cdots\land\left(x_{n}=y_{n}\right)\rightarrow\\ \quad\left(p\left(x_{1},\ldots,x_{n}\right)\leftrightarrow p\left(y_{1},\ldots,y_{n}\right)\right) \end{multline*}\)

Let’s write ⊨₁ for the entailment relation of FOL (without equality), and let 𝛤 be the set of equality axioms given above. Then propositional entailment ⊨₀, FOL entailment ⊨₁, and FOL= entailment ⊨ₑ for ground formulas 𝑋 and 𝐴 are related as follows:

\(\begin{gather*} X\models_{0}A\quad\mbox{iff}\quad X\models_{1}A\\ X\models_{\mathrm{e}}A\quad\mbox{iff}\quad\Gamma,X\models_{1}A \end{gather*}\)

We essentially proved the first equivalence above in the preceding article. The second equivalence says that, from the standpoint of entailment, it doesn’t matter whether we use FOL=, or use FOL plus an axiomatization of equality.

Finite ground axiomatization

There is one snag, though: we need to incorporate an axiomatization of equality into the premise 𝑋 itself, and in general we will not be able to do so with a finite set of ground axioms. Equality is finitely axiomatizable in FOL if we restrict the set of non-nullary¹ function symbols and predicate symbols to be finite (we require a separate axiom for each of these); but to obtain ground axioms we have to replace each universal quantification ∀𝑥. 𝜑 with an infinite number of instances obtained by replacing 𝑥 with every possible ground term. For example, the axiom

\(\forall v_{1}.\forall v_{2}.\left(\left(v_{1}=v_{2}\right)\leftrightarrow\left(v_{2}=v_{1}\right)\right)\)

must be replaced by an axiom (𝑡₁ = 𝑡₂) ↔ (𝑡₂ = 𝑡₁) for every one of the infinitely many possible choices of ground terms for 𝑡₁ and 𝑡₂.

Luckily, we only need a ground axiomatization of equality that suffices for those instances of equality occurring in the premise 𝑋, or which we may wish to use in constructing the query 𝐴, of a plausibility expression (𝐴 ∣ 𝑋) . Let 𝐺 be this set of ground equality atoms, and let’s call a ground formula 𝐺-limited if the only ground atoms containing ‘=’ occurring in it are members of 𝐺. Then we need a 𝐺-limited ground formula 𝜑, which will be the conjunction of a finite set of ground equality axioms, such that

\(X\wedge\varphi\models_{0}Y\quad\mbox{iff}\quad X\models_{\mathrm{e}}Y\)

whenever 𝑋 and 𝑌 are 𝐺-limited.

One approach: limit term depth

One way of creating such an axiomatization is by limiting the depth of terms. The depth of a term is the deepest nesting of function applications within it. Specifically, a term 𝑐( ) has depth 0, and a term 𝑓(𝑡₁, … , 𝑡ₙ) has depth 1 + maxᵢ δᵢ, where δᵢ is the depth of term 𝑡ᵢ. Thus

• 𝑥() has depth 0;

• 1 + 𝑥() has depth 1;

• sqrt(1 + 𝑥()) has depth 2;

• etc.

So letting 𝑁 be some integer such that no term in 𝑋 has depth greater than 𝑁, take the FOL axiomatization of equality given above and instantiate the universally quantified variables using terms of depth at most 𝑁, except for the EF(𝑓) axioms; in this case instantiate the quantified variables with terms of depth at most 𝑁 - 1 (as the resulting ground axiom will then contain a term of depth 𝑁).

If you find this finite limit troublesome, remember Jaynes’s finite sets policy: start with the finite case and then take the limit as 𝑁 goes to infinity.

Another approach: finite domain of discourse

An alternative approach is to note that if

• the domain of discourse (the set of values a quantified variable can have) is finite, and

• our formulas are in ground normal form (defined below),

then a finite ground axiomatization of equality is possible. We do this as follows.

Choose a set of distinct domain constant symbols 𝓓 = { 𝑑₁, … , 𝑑ₖ } intended to represent the 𝑘 values in the domain of discourse. We restrict our attention to formulas in ground normal form:

Definition. A FOL formula is in ground normal form (GNF) if it is a ground formula (no quantifiers, no variables) and every atomic subformula has form 𝑝(𝑐₁, … , 𝑐ₘ) or 𝑓(𝑐₁, … , 𝑐ₙ) = 𝑐₀, where each 𝑐ᵢ is a domain constant (𝑐ᵢ ∈ 𝒟), 𝑚 is the arity of predicate symbol 𝑝, and 𝑛 is the arity of function symbol 𝑓.

We then proceed as follows:

1. Construct a finite set of ground axioms that suffice to characterize equality for GNF formulas. It suffices to assert

   1. that each domain constant is equal to itself and unequal to any other domain constant, and

   2. that any term created by applying a function symbol to arguments that are all domain constants is equal to exactly one of the domain constants.

2. Show how to convert any ground formula into an equivalent GNF formula.

This strategy is a modification of the approach outlined in Wittocx, Mariën, and Denecker (2010)². Details follow.

If your desired domain of discourse is infinite, then once again, start with the finite case and take the limit as 𝑘 goes to infinity.

Axiomatizing equality for GNF formulas

Let 𝛷 be the finite set of function symbols we’ll support. It includes 𝒟, the set of domain constants.

Define the term equality axiom for a ground term t to be:

\(\begin{align*} \mathrm{TEA}\left(t\right) & \triangleq\begin{cases} \mathrm{TEA}_{i} & \mbox{if }t\mbox{ is }d_{i},\;1\leq i\leq k\\ \mathrm{TEA}_{0}\left(t\right) & \mbox{otherwise} \end{cases}\\ \mathrm{TEA}_{0}\left(t\right) & \triangleq\left(\bigvee_{i=1}^{k}(t=d_{i})\right)\wedge \\ &\quad\left(\bigwedge_{1\leq i<j\leq k}\neg\left((t=d_{i})\land (t=d_{j})\right) \right)\\ \mathrm{TEA}_{i} & \triangleq\left(d_{i}=d_{i}\right)\wedge\bigwedge_{j\neq i} \neg\left(d_{i}=d_{j}\right) \end{align*}\)

If 𝑡 is anything other than a domain constant symbol, TEA(𝑡) is a ground formula expressing that 𝑡 is equal to exactly one of the domain constants 𝑑ᵢ. For a domain constant 𝑑ᵢ, TEA(𝑑ᵢ) expresses that 𝑑ᵢ is equal to itself and unequal to any other domain constant.

Define the function equality axiom for any function symbol 𝑓 ∈ 𝛷 of some arity 𝑛 ≥ 0 to be:

\(\mathrm{FEA}\left(f\right)\triangleq\bigwedge_{c_{1}\in\mathcal{D}}\cdots\bigwedge_{c_{n}\in\mathcal{D}}\mathrm{TEA}\left(f\left(c_{1},\ldots,c_{n}\right)\right)\)

This is the conjunction of the term equality axioms for function symbol 𝑓 applied to all possible combinations of domain constants.

Finally, define the ground equality axiom to be

\(\mathrm{GEA}\triangleq\bigwedge_{f\in\Phi}\mathrm{FEA}\left(f\right)\)

This is the conjunction of the function equality axioms for each function symbol. Note that GEA is itself a GNF formula.

A straightforward induction proof yields the following:

Theorem. For any ground term 𝑡 constructed from the function symbols in 𝛷, GEA ⊨₁ TEA(𝑡) .

So GEA entails (in FOL) that every possible ground term is equal to exactly one of the domain constants. This suffices as an axiomatization of equality for GNF formulas. Furthermore, it is straightforward to show that for any two GNF formulas 𝑋 and 𝑌,

\(X\wedge\mathrm{GEA}\models_{0}Y\quad\mbox{iff}\quad X\models_{\mathrm{e}}Y,\)

thus ensuring that GEA makes explicit any implicit logical dependencies between the atoms of 𝑋 and 𝑌.

Reduction to GNF

We can use the following algorithm to transform any ground formula into an equivalent (under FOL=) GNF formula. If 𝜑 is a ground formula then 𝜏(𝜑) is recursively defined as follows:

(Recurse through logical operators.)

\(\begin{align*} \tau(\varphi\land\psi) & =\tau(\varphi)\land\tau(\psi)\\ \tau(\varphi\lor\psi) & =\tau(\varphi)\lor\tau(\psi)\\ \tau(\varphi\rightarrow\psi) & =\tau(\varphi)\rightarrow\tau(\psi)\\ \tau(\varphi\leftrightarrow\psi) & =\tau(\varphi)\leftrightarrow\tau(\psi)\\ \tau(\neg\varphi) & =\neg\tau(\varphi) \end{align*}\)

(In equality comparisons between a domain constant and a term that is not a domain constant, put the domain constant on the right.)

\(\tau\left(t_{1}=t_{2}\right) = \tau\left(t_{2}=t_{1}\right)\quad \mbox{ if }t_{1}\in\mathcal{D},\,t_{2}\notin\mathcal{D} \)

(Replace an equality comparisons between two terms, neither of which is a domain constant, by a formula saying that both terms are equal to the same domain constant.)

\(\begin{multline*} \tau\left(t_{1}=t_{2}\right) =\tau\left(\bigvee_{j=1}^{k}\left(t_{2}=d_{j}\wedge t_{1}=d_{j}\right)\right)\\ \mbox{ if }t_{1},t_{2}\notin\mathcal{D} \end{multline*}\)

(When a function application is compared to a domain constant, reduce its arguments to domain constants using the fact that any argument that is not a domain constant must be equal to some domain constant.)

\(\begin{multline*} \tau\left(f\left(t_{1},\ldots,t_{i},\ldots t_{n}\right)=t_{0}\right) = \\ \tau\left(\bigvee_{j=1}^{k}\left(t_{i}=d_{j}\land f\left(t_{1},\ldots,d_{j},\ldots,t_{n}\right)=t_{0}\right)\right) \\ \mbox{ if }t_{0}\in\mathcal{D},t_{i}\notin\mathcal{D} \end{multline*}\)

(Reduce the arguments of a predicate to domain constants using the fact that any argument that is not a domain constant must be equal to some domain constant.)

\(\begin{multline*} \tau\left(p\left(t_{1},\ldots,t_{i},\ldots,t_{n}\right)\right) = \\ \tau\left(\bigvee_{j=1}^{k}\left(t_{i}=d_{j}\land p\left(t_{1},\ldots,d_{j},\ldots,t_{n}\right)\right)\right) \\ \mbox{ if }t_{i}\notin\mathcal{D} \end{multline*}\)

(Leave GNF atoms unchanged.)

\(\tau\left(\varphi\right) =\varphi\quad\mbox{ if }\varphi\mbox{ is a GNF atom}.\)

Another straightforward induction proof yields the following:

Theorem. For any ground formula 𝜑,

• 𝜏(𝜑) is well defined;

• 𝜏(𝜑) is a GNF formula; and

• GEA ⊨ₑ 𝜑 ↔ 𝜏(𝜑) : that is, 𝜑 and 𝜏(𝜑) are equivalent under FOL=, assuming GEA.

This justifies reducing

\(\left(A\mid X\wedge\mathrm{GEA}\right)\)

to

\(\left(\tau\left(A\right)\mid\tau\left(X\right)\wedge\mathrm{GEA}\right).\)

A note on computational complexity

These approaches to creating a finite ground axiomatization of equality can result in some very large formulas, which may appear computationally impractical; but keep in mind that although the EPL Theorem defines what our probabilities should be, this does not obligate us to carry out the actual computations (or approximate computations) by actually creating these very large formulas and naïvely counting satisfying truth assignments. Furthermore, as previously discussed, although the finite case may often be difficult to compute exactly, things often simplify considerably when we take the limit as 𝑁 or 𝑘 goes to infinity.

1. Having nonzero arity.

2. Wittocx, J., Mariën, M., and M. Denecker, 2010, “Grounding FO and FO(ID) with Bounds,” J. of Artificial Intelligence Research 38, pp. 223—269. https://www.jair.org/index.php/jair/article/view/10653/25467