# Second Order Instantiation

This problem is from the same reference as last time’s but is a bit harder.

The problem: Second Order Instantiation.  This is problem LO19 from the appendix.

The description: Given two second order logic expressions E1 and E2.  E1 can have variables, E2 can’t.  Can we make a substitution of the variables in E1 to get an expression identical to E2?

Example: In second order predicate logic, functions can be variables.  So we could have E1 be P(X) ∧ P(Y), where P is a function variable, and X and Y are “regular” boolean variables.

If E2 was f(a) ∧ f(b) (where all of f, a, and b are not variables), then the substitution {P/f, X/a, Y/b} would work.  But if E2 was f(a) ∧ g(b), then no substitution would work.

Reduction: We again use the Baxter thesis that we used in the last problem to help us here.  We start with a SAT formula S (though really, there’s no reason why we couldn’t just use 3SAT) with n clauses C1 through Cn and m variables P1 through Pm.  E1 will contain one variable for each variable Pi in S, and one variable for each literal xi,j (clause i, position j in the clause).

We also create second-0rder variables gi, one for each clause in S.  Each function gi has degree equal to the number of literals in clause i.

E2 will be built out of the constant symbols T and F, and constant functions Gi, each Gi has degree equal to the number of literals in clause i.

We will also have an additional function H of degree 2, and K of degree 2n.

From each clause i, we build an expression ei‘ = H(gi(T,..T), gi(F,…F))

(Each gi has as many parameters as there are literals in clause i that are all either T or F)

We also build an expression Ei‘ = H(T,F)

For each clause i, literal j, define the expression ei,j”’ = gi(xi,j, …, pi,j, …, xi,j)

(All of the parameters are xi,j except for the jth one, which is the variable for pi,j)

We build the expression ei” = Gi(ei,j”’, …)

(Each Gi has as many parameters as there are literals in clause i)

We also build an expression Ei” = Gi(…)

Each parameter j is T if literal j if clause i is a positive occurrence of a variable, or it’s F if literal j of clause i is a negated occurrence of a variable.

We build E1 = K(e1‘, …, en‘, e1”, …, en”)

E2 = K(E1‘, …, En‘, E1”, …, En”)

Baxter was again good enough to give us an example.

Suppose S was: P ∧ (~P∨Q) ∧ ~R ∧ (~Q∨R∨~P). We have 3 variables and 4 clauses.  So

E1 = K(H(g1(T), g1(F)),

H(g2(T,T), g2(F,F)),

H(g3(T), g3(F)),

H(g4(T,T,T), g4(F,F,F)),

G1(g1(p)),

G2(g2(p, x2,1), g2(x2,2, q)),

G3(g3(r)),

G4(g4(q, x4,1, x4,1), g4(x4,2, r, x4,2), g4(x4,3, x4,3, p)))

E2 = K(H(T,F), H(T,F), H(T,F), H(T,F),

G1(T), G2(F,T), G3(F), G4(F,T,F))

Let’s look at G1 to see how the substitution works.  We need G1(g1(p)) in E1 to map to G1(T) in E2.  So we need g1(p) to map to T.  From the first H function in E1, we also need g1(T) to map to T.  The only way to make both substitutions true is if the variable p is mapped to (or assigned to, in our SAT instance) to T.

Now let’s look at G4. We need the following three mappings to exist:

• g4(q, x4,1, x4,1) -> F
• g4(x4,2, r, x4,2) -> T
• g4(x4,3, x4,3, p) ->F

..we already know from the H function that g4(T,T,T) maps to T and g4(F,F,F) maps to F.  We already know from our G1 discussion that p has to map to T.  For g4(x4,3, x4,3, p) to map to F, we’ll need x4,3 to map to F (and then we have g4(F,F,T) map to F.  Notice that because we move the “variable” parameter around g4, none of the other g4 clauses will be able to generate (F,F,T) parameters since they all have 2 copies of the same x variable in different places).

The actual proof of this reduction goes on for a couple of pages of the Baxter thesis, but hopefully this explains the basic idea.

Difficulty: 8.  This is harder to follow than last week’s, but the general idea of “binding variables and literals to functions that test for satisfiability” is a pattern we’ve seen several times.