Order in substituting values for the variables - Predecessors and Successors

Question

Dear Prof. and Team,

Is there any order to be maintained while substituting for the variables here for 1 or 0. In this case it is a,q1 and q2. Can i take any random order here ?

In this eg. a is first substituted for 0 and 1. Instead of that, can i substitute q1 for 0 and 1 in the beginning and so on ?

P.S : I understand the complexity of the formula increases if i don't substitute for a here first. But my question is in general. Should we substitute for a variable thoughtfully so that the formula gets reduced to its simplest form.
https://drive.google.com/open?id=1xhFCjrY_DFaWNW_vw4gjlnqDvHaATziA

Comments

Please don't address Prof. and team, also students may give you good answers!

Answer 1

You can perform the universal quantification of variables in any order since it is commutative. Recall that the definition of universal quantification is ∀x.φ := φ[x:=0] ⋀ φ[x:=1]. Thus, we have 

• ∀x.∀y.φ = (∀y.φ)[x:=0] ⋀ (∀y.φ)[x:=1] = φ[x:=0][y:=0] ⋀ φ[x:=0][y:=1] ⋀ φ[x:=1][y:=0] ⋀ φ[x:=1][y:=1] 
• ∀y.∀x.φ = (∀x.φ)[y:=0] ⋀ (∀x.φ)[y:=1] = φ[x:=0][y:=0] ⋀ φ[x:=1][y:=0] ⋀ φ[x:=0][y:=1] ⋀ φ[x:=1][y:=1] 

which are the same (note that φ[x:=0][y:=1] and φ[y:=1][x:=0] are the same: what we do is replacing occurrences of x and y by 0 and since occurrences of x are not occurrences of y, the two are not in conflict).

Hence, we have ∀x.∀y.φ = ∀y.∀x.φ, and by negation, we also see that ∃x.∃y.φ = ∃y.∃x.φ holds. However, you cannot change the order of alternating quantifiers like ∀x.∃y.φ or ∃x.∀y.φ.

And you are right with your observation that you can often significantly save work when you choose that variable first that will reduce the formula as much as possible since one part φ[x:=0] or φ[x:=1] may be just true or a small formula.

Answer 2

The order with which variable you start quantify ( with substituted for [\phi]_x^0 and [\phi]_x^1) doesn't yield other results.

it can be sehen as \forall x,y \phi & 1= [[\phi]_x^0 & [\phi]_x^1]_y^0  & [[\phi]_x^0 & [\phi]_x^1]_y^1= [[\phi]_y^0 & [\phi]_y^1]_x^0  & [[\phi]_y^0 & [\phi]_y^1]_x^1

Comments

Thanks Soeren ! :)