Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


543 users

+1 vote

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.

in * TF "Emb. Sys. and Rob." by (430 points)
Please don't address Prof. and team, also students may give you good answers!

2 Answers

+1 vote
Best answer

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.

by (166k points)
selected by
+2 votes
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
by (810 points)
Thanks Soeren ! :)
Imprint | Privacy Policy