When Propositional Symbols Have FOL Structure

The issue

Before continuing on to discuss other topics, I want to address a possible objection to requirements R2 and R3 of the EPL Theorem. A correspondent wrote the following:

I’m not sure I’m comfortable with the idea of (ir)relevance operationalized in R2 and R3 as lack of appearance of particular symbols. In the first-order case where the propositional variables may represent statements that have constants or predicates in common, it feels to me like logically independent propositional variables may nevertheless contain information that is relevant to each other.

Recall that R2 is the requirement of invariance under definition of new propositional symbols, and R3 is invariance under addition of irrelevant information, where 𝑌 is considered irrelevant to (𝐴 ∣ 𝑋) if it is satisfiable and contains no propositional symbol used in either 𝐴 or 𝑋 .

The concern here is that if our propositional symbols have internal structure, are in fact the variable-free atomic formulas in some FOL language, then this internal structure may implicitly introduce some logical dependency between them above and beyond what is stated in the premise 𝑋 of the plausibility expression (𝐴 ∣ 𝑋) . To address this concern we first need to discuss first-order predicate logic (FOL) in more detail.

The language of FOL: symbols

Instead of constructing formulas from propositional symbols, in FOL we build them up from variables, function symbols, and predicate symbols. Function symbols and predicate symbols each have an associated arity, the number of arguments to which they should be applied. Binary (arity 2) function symbols and relation symbols are sometimes used in infix form, e.g. 𝜀 > 0 instead of >(𝜀, 0) and 𝑥 − 𝑦 instead of −(𝑥 , 𝑦) . Constants are just arity-0 function symbols, and the parentheses are often dropped, e.g. 0 instead of 0 ( ) .

Recall the example FOL formula from the preceding post, corresponding to the English language statement that 𝑥 is the limit of 𝑎ₙ as 𝑛 goes to infinity:

\(\begin{flalign*} & \forall\varepsilon.\,\varepsilon\in\mathbb{R}\wedge\varepsilon>0\rightarrow\\ & \quad\exists N.\,N\in\mathbb{Z}\wedge N>0\,\wedge\\ & \quad\quad\forall n.\,n\in\mathbb{Z}\wedge n\geq N\rightarrow\\ & \quad\quad\quad\mathrm{abs}\left(x-\mathrm{elt}\left(a,n\right)\right)<\varepsilon. \end{flalign*}\)

In this example,

• 𝑥, 𝜀, 𝑁, and 𝑛 are variables;

• 0, ℝ, and ℤ are constants (function symbols of arity 0);

• 𝚊𝚋𝚜 is a function symbol of arity 1;

• 𝚎𝚕𝚝 and − are function symbols of arity 2; and

• ∈ , > , < , and ≥ are predicate symbols of arity 2.

The variables in a FOL formula refer to values from some domain of discourse. In our example the intended domain of discourse includes all the real numbers individually as well as two sets considered as objects in their own right: the set of all real numbers and the set of all integers.

The language of FOL: terms and formulas

In FOL, atomic formulas take the place of propositional symbols. An atomic formula has the form 𝑝(𝑡₁, … , 𝑡ₙ) where 𝑝 is a predicate symbol of arity 𝑛 and 𝑡₁, … , 𝑡ₙ are terms. An atomic formula is intended to mean that the relation represented by 𝑝 holds between the 𝑛 arguments.

A term represents a value from the domain of discourse. A term is either a variable 𝑣 or an expression of the form 𝑓(𝑡₁, … , 𝑡ₙ) where 𝑓 is a function symbol of arity 𝑛 and 𝑡₁, … , 𝑡ₙ are terms. This latter form is intended to represent a function applied to 𝑛 arguments. The base cases for this recursive definition are the variables 𝑣 and constants 𝑐( ) (which are arity-0 function applications).

A FOL formula is then one of the following:

• an atomic formula;

• (¬𝜑), (𝜑 ∧ 𝜓) , (𝜑 ∨ 𝜓) , (𝜑 → 𝜓) , or (𝜑 ↔ 𝜓) , where 𝜑 and 𝜓 are FOL formulas; or

• (∀𝑣. 𝜑) or (∃𝑣. 𝜑), where 𝑣 is a variable and 𝜑 is a FOL formula.

As usual, when written for human consumption we may drop parentheses when this results in no ambiguity; also, for some arity-2 function symbols or predicate symbols we may use infix notation as previously mentioned.

Thus a FOL formula is much like a propositional formula, except that atomic formulas take the place of propositional symbols, and we allow the quantifiers ∀𝑣 (for all 𝑣) and ∃𝑣 (there exists 𝑣) as additional logical operations.

Propositionalization

A variable 𝑣 in a FOL formula is free if it occurs outside of the scope of any quantifier ∀𝑣 or ∃𝑣. In our example formula the variable 𝑥 is free and the variables 𝜀, 𝑛, and 𝑁 are not. A FOL formula is closed iff it has no free variables.

A ground term is a term that contains no variables. A ground atom is an atomic formula containing only ground terms. A ground formula is a FOL formula that contains neither variables nor quantifiers. Any ground formula may be constructed from ground atoms using the logical operators ¬ , ⋀ , ⋁ , → , and ↔ ; thus we may consider it to be a propositional formula if we treat the atomic formulas as propositional symbols. (The terminology “ground” is intended to suggest concreteness over abstraction.)

Suppose that we intend the domain of discourse to be limited to 𝑛 values, indicated by the constant symbols 𝑐₁, … , 𝑐ₙ. If a closed FOL formula 𝜑 contains one or more quantifiers ∀𝑣 or ∃𝑣, we can create an equivalent ground formula 𝜑' by repeating the following transformation until there are no quantifiers left:

• If 𝜑 contains a subexpression of the form ∀𝑣. 𝜓 or ∃𝑣. 𝜓, replace it by (𝜓₁ ∧ ⋯ ∧ ψₙ) or (𝜓₁ ∨ ⋯ ∨ ψₙ) respectively, where 𝜓ᵢ is obtained from 𝜓 by replacing all free occurrences of 𝑣 in 𝜓 by 𝑐ᵢ.

This process is called propositionalization, because the result may be treated as a propositional formula.

As an example, propositionalization with a domain of discourse { 0 , 1 } and corresponding constant symbols 0 and 1 turns

\(\forall v.\,\exists w.\,\mathtt{P}\left(v,w\right)\)

into

\(\left(\left(\mathtt{P}\left(\mathtt{0},\mathtt{0}\right)\lor\mathtt{P}\left(\mathtt{0},\mathtt{1}\right)\right)\land\left(\mathtt{P}\left(\mathtt{1},\mathtt {0}\right)\lor\mathtt{P}\left(\mathtt{1},\mathtt{1}\right)\right)\right).\)

FOL interpretations

Recall that an interpretation for a propositional language is just a truth assignment on its propositional symbols. This yields a truth value for a propositional formula 𝐴 by replacing each propositional symbol with its assigned truth value and evaluating the resulting expression. An interpretation for a FOL language likewise yields a truth value for any closed FOL formula, but it does so by assigning meanings to the function symbols and predicate symbols.

Specifically, for FOL an interpretation is a tuple ℐ = (𝐷, 𝑅, 𝐹), where

• 𝐷 is some nonempty set, the domain of discourse;

• 𝐹 is a function that assigns to each function symbol of arity 𝑛 an 𝑛-ary function on 𝐷; and

• 𝑅 is a function that assigns to each predicate symbol of arity 𝑛 an 𝑛-ary relation on 𝐷.

An 𝑛-ary function on 𝐷 is a function that takes 𝑛 arguments from 𝐷 and returns a value from 𝐷. For example, sin is a 1-ary function on ℝ (the real numbers), and + is a 2-ary (binary) function on ℝ. A 0-ary function on 𝐷 is effectively just a constant value from 𝐷.

An 𝑛-ary relation on 𝐷 is a subset of 𝐷ⁿ, the set of 𝑛-tuples (𝑥₁, … , 𝑥ₙ) where 𝑥ᵢ ∈ 𝐷 for all 𝑖. A 0-ary relation on 𝐷 is one of ∅ or 𝐷⁰ ( = { ( ) } ), effectively just a truth value 𝖥 or 𝖳. A 1-ary relation on 𝐷 is effectively a subset of 𝐷. Examples:

• The odd integers are a 1-ary relation (predicate) on ℤ, the set of integers.

• “Less than,” as a binary relation on ℝ, is the set of all ordered pairs (𝑥, 𝑦) where 𝑥 < 𝑦.

Apologies, but Chrome on MacOS, and perhaps other browsers, displays the character ℐ that I use for interpretations in two different ways, seemingly at random. Furthermore, neither of these looks a whole lot like the way this character is shown in displayed formulas such as

\(\mathscr{I}[[\varphi]]\)

I hope this isn’t too confusing.

Semantics of ground formulas

We write ℐ⟦𝜑⟧ for the truth value that interpretation ℐ = (𝐷, 𝑅, 𝐹) yields when applied to closed FOL formula 𝜑. For current purposes we restrict our attention to the case where 𝜑 is a ground formula.

To evaluate a ground term, look up the function assigned to the function symbol, evaluate each of the arguments, and apply the function to the evaluated arguments:

\(\begin{align*} \mathscr{I}[[ f\left(t_{1},\ldots,t_{n}\right) ]] & =F(f)\left(x_{1},\ldots,x_{n}\right)\\ \mbox{where }x_{i} & =\mathscr{I}[[ t_{i} ]],\quad1\leq i\leq n. \end{align*}\)

To evaluate a ground atom, look up the relation assigned to the predicate symbol, evaluate each of the arguments, and decide if the relation holds between the evaluated arguments:

\(\begin{align*} \mathscr{I}[[ p\left(t_{1},\ldots,t_{n}\right) ]] & =\begin{cases} \mathsf{T} & \mbox{if }\left(x_{1},\ldots,x_{n}\right)\in R(p)\\ \mathsf{F} & \mbox{otherwise} \end{cases}\\ \mbox{where }x_{i} & =\mathscr{I}[[ t_{i} ]],\quad1\leq i\leq n. \end{align*}\)

Evaluate the logical operators in the usual way:

\(\begin{align*} \mathscr{I}[[ \neg\varphi ]] & =\neg\mathscr{I}[[ \varphi ]] \\ \mathscr{I}[[ \varphi\wedge\psi ]] & =\mathscr{I}[[ \varphi ]] \wedge\mathscr{I}[[ \psi ]] \\ \cdots \end{align*}\)

(I’ve abused notation above: ¬ and ∧ within the Oxford brackets ⟦⋅⟧ are textual entities—symbols—whereas on the right-hand side of the equality they refer to the actual logical operations.)

Truth assignment induced by an interpretation

We now have two alternatives for evaluating a truth value for a ground formula 𝜑:

• Use a FOL interpretation ℐ and evaluate ℐ⟦𝜑⟧.

• Use a truth assignment 𝛼 on the ground atoms of 𝜑 and evaluate 𝛼⟦𝜑⟧.

In the latter case we have treated ground atoms as propositional symbols and ground formula 𝜑 as a propositional formula.

We can relate these alternatives by noting that ℐ induces the following truth assignment 𝛼 on any set 𝐺 of ground atoms:

\(\alpha(\gamma)\triangleq\mathscr{I}[[ \gamma ]] \quad\mbox{for all }\gamma\in G.\)

We call this the truth assignment induced by ℐ on 𝐺, written TA(ℐ, 𝐺). If 𝐺 contains all the ground atoms occurring in ground formula 𝜑 then

\(\mathscr{I}[[ \varphi ]] =\alpha[[ \varphi ]] \quad\mbox{where}\quad\alpha=\mathrm{TA}\left(\mathscr{I},G\right).\)

Restating the issue

Now let us return to the concern raised at the beginning of this article:

In the first-order case where the propositional variables may represent statements that have constants or predicates in common, can logically independent propositional variables nevertheless contain information that is relevant to each other?

What does it mean for a set of ground atoms 𝐺 to “contain information that is relevant to each other”? It means that there is some combination of truth values for the members of 𝐺 that is not attainable via any interpretation ℐ; in other words, that there exists some truth assignment 𝛼 on 𝐺 that is not equal to TA(ℐ, 𝐺) for any FOL interpretation ℐ.

We can therefore dispense with this concern by showing that the opposite is true: for every truth assignment 𝛼 on 𝐺 there exists some interpretation ℐ for which 𝛼 = TA(ℐ, 𝐺).

Constructing the required interpretation

One way of constructing such an interpretation is via the idea of a Herbrand interpretation, in which every term is interpreted as itself. Specifically, a Herbrand interpretation ℐ = (𝐷, 𝐹, 𝑅) has the properties that

• The domain of discourse 𝐷 is the set of ground terms themselves.

• The mapping 𝐹 is defined by

  \(F\left(f\right)\left(x_{1},\ldots,x_{n}\right)\triangleq f\left(x_{1},\ldots,x_{n}\right)\)

  for every function symbol 𝑓 of arity 𝑛, where we understand the RHS of the equation to mean the ground term that consists of function symbol 𝑓 applied to ground terms 𝑥₁, … , 𝑥ₙ.

Distinct Herbrand interpretations differ only in the mapping 𝑅 that assigns relations on 𝐷 to the predicate symbols.

As an example, if our function symbols are 𝚌 (arity 0) and 𝚏 (arity 1), then for a Herbrand interpretation the domain of discourse is

\(D=\left\{ \mathtt{c},\mathtt{f}\left(\mathtt{c}\right),\mathtt{f}\left(\mathtt{f}\left(\mathtt{c}\right)\right),\ldots\right\} \)

and the mapping 𝐹 is given by

\(\begin{align*} F\left(\mathtt{c}\right)() & =\mathtt{c}\\ F\left(\mathtt{f}\right)\left(\mathtt{c}\right) & =\mathtt{f}(\mathtt{c})\\ F\left(\mathtt{f}\right)\left(\mathtt{f}(\mathtt{c})\right) & =\mathtt{f}(\mathtt{f}(\mathtt{c})\\ \ldots \end{align*}\)

So given a truth assignment 𝛼 on some set of ground atoms 𝐺, let ℐ be the Herbrand interpretation ℐ = (𝐷, 𝐹, 𝑅) where for every predicate symbol 𝑝 of arity 𝑛,

\(R(p)=\left\{ \left(x_{1},\ldots,x_{n}\right)\in D^{n}\colon\alpha\left(p\left(x_{1},\ldots,x_{n}\right)\right)\mbox{ is true}\right\} .\)

Now let 𝛼' = TA(ℐ, 𝐺). The truth assignment 𝛼' has the same domain, 𝐺, as the truth assignment 𝛼. Furthermore, for every 𝛾 ∈ 𝐺 there exists some predicate symbol 𝑝 of some arity 𝑛, and ground terms 𝑥₁, … , 𝑥ₙ ∈ 𝐷, such that 𝛾 is the ground atom 𝑝(𝑥₁, … , 𝑥ₙ). Then

\(\begin{align*} \alpha'\left(\gamma\right) & =\alpha'\left(p\left(x_{1},\ldots,x_{n}\right)\right)\\ & =\mathscr{I}[[ p\left(x_{1},\ldots,x_{n}\right) ]] \\ & =\left(\mathscr{I}[[ x_{1} ]], \ldots, \mathscr{I}[[ x_{n} ]] \right)\in R(p)\\ & =\left(x_{1},\ldots,x_{n}\right)\in R(p)\\ & =\alpha\left(p\left(x_{1},\ldots,x_{n}\right)\right)\\ & =\alpha(\gamma). \end{align*} \)

Since this equality holds for all 𝛾 ∈ 𝐺 we then have 𝛼 = 𝛼' = TA(ℐ, 𝐺). Thus ℐ is the required interpretation.

One last thing

The alert reader will have noticed that I have not mentioned equality in the above discussion. This introduces some complications that I will address in the next article.