Relational Logic and Propositional Logic

One interesting feature of Relational Logic (RL) is that it is expressively equivalent to Propositional Logic (PL). For any RL language, we can produce a pairing between the ground relational sentences in that language and the proposition constants in a PL language. Given this correspondence, for any set of arbitrary sentences in our RL language, there is a corresponding set of sentences in the language of PL such that any RL truth assignment that satisfies our RL sentences agrees with the corresponding PL truth assignment applied to the PL sentences.

The procedure for transforming our RL sentences to PL has multiple steps, but each step is easy. We first convert our sentences to prenex form, then we ground the result, and we rewrite in PL. Let's look at these steps in turn.

A sentence is in prenex form if and only if it is closed and all of the quantifiers are on the outside of all logical operators.

Once we have a set of sentences in prenex form, we compute the grounding. We start with our initial set Δ of sentences and we incrementally build up our grounding Γ. On each step we process a sentence in Δ, using the procedure described below. The procedure terminates when Δ becomes empty. The set Γ at that point is the grounding of the input.

(1) The first rule covers the case when the sentence φ being processed is ground. In this case, we remove the sentence from Delta and add it to Gamma.

(2) If our sentence is of the form ∀ν.φ[ν], we eliminate the sentence from Δ_i and replace it with copies of the scope, one copy for each object constant τ in our language.

(3) If our sentence of the form ∃ν.φ[ν], we eliminate the sentence from Δ_i and replace it with a disjunction, where each disjunct is a copy of the scope in which the quantified variable is replaced by an object constant in our language.

The procedure halts when Δ_i becomes empty. The set Γ_i is the grounding of the input. It is easy to see that Γ_i is logically equivalent to the input set.

Here is an example. Suppose we have a language with just two object constants a and b. And suppose we have the set of sentences shown below. We have one ground sentence, one universally quantified sentence, and one existentially quantified sentence. All are in prenex form.

A trace of the procedure is shown below. The first sentence is ground, so we remove it from Δ add it to Γ. The second sentence is universally quantified, so we replace it with a copy for each of our two object constants. The resulting sentences are ground, and so we move them one by one from Δ to Γ. Finally, we ground the existential sentence and add the result to Δ and then move the ground sentence to Γ. At this point, since Δ is empty, Γ is our grounding.

Once we have a grounding Γ, we replace each ground relational sentence in Γ by a proposition constant. The resulting sentences are all in Propositional Logic; and the set is equivalent to the sentences in Δ in that any RL truth assignment that satisfies our RL sentences agrees with the corresponding Propositional Logic truth assignment applied to the Propositional Logic sentences.

For example, let's represent the RL sentence p(a) with the proposition pa; let's represent p(b) with pb; let's represent q(a) with qa; and let's represent q(b) with qb. With this correspondence, we can represent the sentences in our grounding with the Propositional Logic sentences shown below.

Since the question of unsatisfiability for PL is decidable, then the question of unsatisfiability for RL is also decidable. Since logical entailment and unsatisfiability are correlated, we also know that the question of logical entailment for RL is decidable.

Another consequence of this correspondence between RL and PL is that, like PL, RL is compact - every unsatisfiable set of sentences contains a finite subset that is unsatisfiable. This is important as it assures us that we can demonstrate the unsatisfiability by analyzing just a finite set of sentences; and, as we shall see in the next chapter, logical entailment can be demonstrated with finite proofs.