[<< wikibooks] Logic for Computer Scientists/Predicate Logic/Equivalence and Normal Forms
== Equivalence and Normal Forms ==
Equivalence of formulae is defined as in the propositional case:


== Definition 6 ==
The formulae 
  
    
      
        F
      
    
    {\displaystyle F}
   and 
  
    
      
        G
      
    
    {\displaystyle G}
   are called (semantically)
equivalent, if for all interpretations 
  
    
      
        
          
            I
          
        
      
    
    {\displaystyle {\mathcal {I}}}
   for 
  
    
      
        F
      
    
    {\displaystyle F}
   and 
  
    
      
        G
      
    
    {\displaystyle G}
  ,

  
    
      
        
          
            I
          
        
        (
        F
        )
        =
        
          
            I
          
        
        (
        G
        )
      
    
    {\displaystyle {\mathcal {I}}(F)={\mathcal {I}}(G)}
  . We write 
  
    
      
        F
        ≡
        G
      
    
    {\displaystyle F\equiv G}
  .
The equivalences from  the propositional case in theorem 4
equivalences hold and in addition we have the following
cases for quantifiers.


== Theorem 1 ==
The following equivalences hold:

  
    
      
        ¬
        ∀
        x
        F
      
    
    {\displaystyle \lnot \forall xF}
    
  
    
      
        ≡
      
    
    {\displaystyle \equiv }
    
  
    
      
        ∃
        x
        ¬
        F
      
    
    {\displaystyle \exists x\lnot F}
  

  
    
      
        ¬
        ∃
        x
        F
      
    
    {\displaystyle \lnot \exists xF}
   
  
    
      
        ≡
      
    
    {\displaystyle \equiv }
    
  
    
      
        ∀
        x
        ¬
        F
      
    
    {\displaystyle \forall x\lnot F}
  
If 
  
    
      
        x
      
    
    {\displaystyle x}
   does not occur free in 
  
    
      
        G
      
    
    {\displaystyle G}
  :

  
    
      
        ∀
        x
        F
        ∧
        G
      
    
    {\displaystyle \forall xF\land G}
   
  
    
      
        ≡
      
    
    {\displaystyle \equiv }
    
  
    
      
        ∀
        x
        (
        F
        ∧
        G
        )
      
    
    {\displaystyle \forall x(F\land G)}
  

  
    
      
        ∀
        x
        F
        ∨
        G
      
    
    {\displaystyle \forall xF\lor G}
    
  
    
      
        ≡
      
    
    {\displaystyle \equiv }
    
  
    
      
        ∀
        x
        (
        F
        ∨
        G
        )
      
    
    {\displaystyle \forall x(F\lor G)}
  

  
    
      
        ∃
        x
        F
        ∧
        G
      
    
    {\displaystyle \exists xF\land G}
   
  
    
      
        ≡
      
    
    {\displaystyle \equiv }
    
  
    
      
        ∃
        x
        (
        F
        ∧
        G
        )
      
    
    {\displaystyle \exists x(F\land G)}
  

  
    
      
        ∃
        x
        F
        ∨
        G
      
    
    {\displaystyle \exists xF\lor G}
   
  
    
      
        ≡
      
    
    {\displaystyle \equiv }
    
  
    
      
        ∃
        x
        (
        F
        ∨
        G
        )
      
    
    {\displaystyle \exists x(F\lor G)}
  

  
    
      
        ∀
        x
        F
        ∧
        ∀
        x
        G
      
    
    {\displaystyle \forall xF\land \forall xG}
   
  
    
      
        ≡
      
    
    {\displaystyle \equiv }
   
  
    
      
        ∀
        x
        (
        F
        ∧
        G
        )
      
    
    {\displaystyle \forall x(F\land G)}
  

  
    
      
        ∃
        x
        F
        ∨
        ∃
        x
        G
      
    
    {\displaystyle \exists xF\lor \exists xG}
   
  
    
      
        ≡
      
    
    {\displaystyle \equiv }
    
  
    
      
        ∃
        x
        (
        F
        ∨
        G
        )
      
    
    {\displaystyle \exists x(F\lor G)}
  

  
    
      
        ∀
        x
        ∀
        y
        
        F
      
    
    {\displaystyle \forall x\forall y\;F}
    
  
    
      
        ≡
      
    
    {\displaystyle \equiv }
   
  
    
      
        ∀
        y
        ∀
        x
        F
      
    
    {\displaystyle \forall y\forall xF}
  

  
    
      
        ∃
        x
        ∃
        y
        
        F
      
    
    {\displaystyle \exists x\exists y\;F}
   
  
    
      
        ≡
      
    
    {\displaystyle \equiv }
    
  
    
      
        ∃
        y
        ∃
        x
        F
      
    
    {\displaystyle \exists y\exists xF}
  
Proof: We will prove only  the equivalence

  
    
      
        ∀
        x
        F
        ∧
        G
        ≡
        ∀
        x
        (
        F
        ∧
        G
        )
      
    
    {\displaystyle \forall xF\land G\equiv \forall x(F\land G)}
  
with 
  
    
      
        x
      
    
    {\displaystyle x}
   has no free occurrence in 
  
    
      
        G
      
    
    {\displaystyle G}
  , as an example.
Assume an interpretation 
  
    
      
        
          
            I
          
        
        =
        (
        U
        ,
        
          
            A
          
        
        )
      
    
    {\displaystyle {\mathcal {I}}=(U,{\mathcal {A}})}
   such that

  
    
      
        
          
            I
          
        
        (
        ∀
        x
        F
        ∧
        G
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\mathcal {I}}(\forall xF\land G)=true}
    

  
    
      
        
          iff 
        
        
          
            I
          
        
        (
        ∀
        x
        F
        )
        =
        t
        r
        u
        e
        
           and 
        
        
          
            I
          
        
        (
        G
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\text{iff }}{\mathcal {I}}(\forall xF)=true{\text{ and }}{\mathcal {I}}(G)=true}
  
  
    
      
        
          iff 
        
        
           for all 
        
        d
        ∈
        U
        :
        
          
            
              I
            
          
          
            [
            x
            
              /
            
            d
            ]
          
        
        (
        F
        )
        =
        t
        r
        u
        e
        
           and 
        
        
          
            I
          
        
        (
        G
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}(G)=true}
  
  
    
      
        
          iff 
        
        
           for all 
        
        d
        ∈
        U
        :
        
          
            
              I
            
          
          
            [
            x
            
              /
            
            d
            ]
          
        
        (
        F
        )
        =
        t
        r
        u
        e
        
           and 
        
        
          
            
              I
            
          
          
            [
            x
            
              /
            
            d
            ]
          
        
        (
        G
        )
        =
        t
        r
        u
        e
        
           (x = does not occur free in = G)
        
      
    
    {\displaystyle {\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}_{[x/d]}(G)=true{\text{ (x = does not occur free in = G)}}}
  
  
    
      
        
          iff 
        
        
           for all 
        
        d
        ∈
        U
        :
        
          
            
              I
            
          
          
            [
            x
            
              /
            
            d
            ]
          
        
        (
        (
        F
        ∧
        G
        )
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}((F\land G))=true}
  
  
    
      
        
          iff 
        
        
          
            I
          
        
        (
        ∀
        x
        (
        F
        ∧
        G
        )
        )
        =
        t
        r
        u
        e
        .
      
    
    {\displaystyle {\text{iff }}{\mathcal {I}}(\forall x(F\land G))=true.}
  
Note that the following symmetric cases do not hold:

  
    
      
        ∀
        x
        F
        ∨
        ∀
        x
        G
      
    
    {\displaystyle \forall xF\lor \forall xG}
     is not equivalent to   
  
    
      
        ∀
        x
        (
        F
        ∨
        G
        )
      
    
    {\displaystyle \forall x(F\lor G)}
  

  
    
      
        ∃
        x
        F
        ∧
        ∃
        x
        G
      
    
    {\displaystyle \exists xF\land \exists xG}
    is not equivalent to   
  
    
      
        ∃
        x
        (
        F
        ∧
        G
        )
      
    
    {\displaystyle \exists x(F\land G)}
  
The theorem for substituitivity holds as in the propositional case.
Example: Let us transform the following formulae by means of
substituitivity and the equivalences from theorem 1:

  
    
      
        (
        ¬
        (
        ∃
        x
        P
        (
        x
        ,
        y
        )
        ∨
        ∀
        z
        Q
        (
        z
        )
        )
        ∧
        ∃
        w
        P
        (
        f
        (
        a
        ,
        w
        )
        )
        )
      
    
    {\displaystyle (\lnot (\exists xP(x,y)\lor \forall zQ(z))\land \exists wP(f(a,w)))}
   

  
    
      
        ≡
        (
        (
        ¬
        ∃
        x
        P
        (
        x
        ,
        y
        )
        ∧
        ¬
        ∀
        z
        Q
        (
        z
        )
        )
        ∧
        ∃
        w
        P
        (
        f
        (
        a
        ,
        w
        )
        )
        )
      
    
    {\displaystyle \equiv ((\lnot \exists xP(x,y)\land \lnot \forall zQ(z))\land \exists wP(f(a,w)))}
  

  
    
      
        ≡
        (
        (
        ∀
        x
        ¬
        P
        (
        x
        ,
        y
        )
        ∧
        ∃
        z
        ¬
        Q
        (
        z
        )
        )
        ∧
        ∃
        w
        P
        (
        f
        (
        a
        ,
        w
        )
        )
        )
      
    
    {\displaystyle \equiv ((\forall x\lnot P(x,y)\land \exists z\lnot Q(z))\land \exists wP(f(a,w)))}
  

  
    
      
        ≡
        (
        ∃
        w
        P
        (
        f
        (
        a
        ,
        w
        )
        )
        ∧
        (
        ∀
        x
        ¬
        P
        (
        x
        ,
        y
        )
        ∧
        ∃
        z
        ¬
        Q
        (
        z
        )
        )
        )
      
    
    {\displaystyle \equiv (\exists wP(f(a,w))\land (\forall x\lnot P(x,y)\land \exists z\lnot Q(z)))}
  

  
    
      
        ≡
        ∃
        w
        (
        P
        (
        f
        (
        a
        ,
        w
        )
        )
        ∧
        ∀
        x
        (
        ¬
        P
        (
        x
        ,
        y
        )
        ∧
        ∃
        z
        ¬
        Q
        (
        z
        )
        )
        )
      
    
    {\displaystyle \equiv \exists w(P(f(a,w))\land \forall x(\lnot P(x,y)\land \exists z\lnot Q(z)))}
  

  
    
      
        ≡
        ∃
        w
        (
        ∀
        x
        (
        ∃
        z
        ¬
        Q
        (
        z
        )
        ∧
        ¬
        P
        (
        x
        ,
        y
        )
        )
        ∧
        P
        (
        f
        (
        a
        ,
        w
        )
        )
        )
      
    
    {\displaystyle \equiv \exists w(\forall x(\exists z\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}
  

  
    
      
        ≡
        ∃
        w
        (
        ∀
        x
        ∃
        z
        (
        ¬
        Q
        (
        z
        )
        ∧
        ¬
        P
        (
        x
        ,
        y
        )
        )
        ∧
        P
        (
        f
        (
        a
        ,
        w
        )
        )
        )
      
    
    {\displaystyle \equiv \exists w(\forall x\exists z(\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}
  

  
    
      
        ≡
        ∃
        w
        ∀
        x
        ∃
        z
        (
        (
        ¬
        Q
        (
        z
        )
        ∧
        ¬
        P
        (
        x
        ,
        y
        )
        )
        ∧
        P
        (
        f
        (
        a
        ,
        w
        )
        )
        )
      
    
    {\displaystyle \equiv \exists w\forall x\exists z((\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}
  


== Definition 7 ==
Let 
  
    
      
        F
      
    
    {\displaystyle F}
   be a formula, 
  
    
      
        x
      
    
    {\displaystyle x}
   a variable and 
  
    
      
        t
      
    
    {\displaystyle t}
   a term. 
  
    
      
        F
        [
        x
        
          /
        
        t
        ]
      
    
    {\displaystyle F[x/t]}
   is
obtained from 
  
    
      
        F
      
    
    {\displaystyle F}
   by substituting every free occurrence of 
  
    
      
        x
      
    
    {\displaystyle x}
   by 
  
    
      
        t
      
    
    {\displaystyle t}
  .
Note, that this notion can be iterated: 
  
    
      
        F
        [
        x
        
          /
        
        
          t
          
            1
          
        
        ]
        [
        y
        
          /
        
        
          t
          
            2
          
        
        ]
      
    
    {\displaystyle F[x/t_{1}][y/t_{2}]}
   and that

  
    
      
        
          t
          
            1
          
        
      
    
    {\displaystyle t_{1}}
   may contain free occurrences of 
  
    
      
        y
      
    
    {\displaystyle y}
  .


== Lemma 1 ==
Let 
  
    
      
        F
      
    
    {\displaystyle F}
   be a formula, 
  
    
      
        x
      
    
    {\displaystyle x}
   a variable and 
  
    
      
        t
      
    
    {\displaystyle t}
   a term.

  
    
      
        
          
            I
          
        
        (
        F
        [
        x
        
          /
        
        t
        ]
        )
        =
        
          
            
              I
            
          
          
            [
            x
            
              /
            
            
              
                I
              
            
            (
            t
            )
            ]
          
        
        (
        F
        )
      
    
    {\displaystyle {\mathcal {I}}(F[x/t])={\mathcal {I}}_{[x/{\mathcal {I}}(t)]}(F)}
  


== Lemma 2 (Bounded Renaming) ==
Let 
  
    
      
        F
        =
        Q
        x
        G
      
    
    {\displaystyle F=QxG}
   be a formula, where 
  
    
      
        Q
        ∈
        {
        ∀
        ,
        ∃
        }
      
    
    {\displaystyle Q\in \{\forall ,\exists \}}
   and

  
    
      
        y
      
    
    {\displaystyle y}
   a variable without an occurrence in 
  
    
      
        G
      
    
    {\displaystyle G}
  , then 
  
    
      
        F
        ≡
        Q
        y
        G
        [
        x
        
          /
        
        y
        ]
      
    
    {\displaystyle F\equiv QyG[x/y]}
  


== Definition 8 ==
A formula is called proper if there is no variable which
occurs bound and free and after every quantifier there is a distinct
variable.


== Lemma 3 (Proper Formula) ==
For every formula 
  
    
      
        F
      
    
    {\displaystyle F}
   there is a formula 
  
    
      
        G
      
    
    {\displaystyle G}
   which is proper and
equivalent to 
  
    
      
        F
      
    
    {\displaystyle F}
  .
Proof: Follows immediately by bounded renaming.

Example: 

  
    
      
        F
        =
        ∀
        x
        ∃
        y
        
        p
        (
        x
        ,
        f
        (
        y
        )
        )
        ∧
        ∀
        x
        (
        q
        (
        x
        ,
        y
        )
        ∨
        r
        (
        x
        )
        )
      
    
    {\displaystyle F=\forall x\exists y\;p(x,f(y))\land \forall x(q(x,y)\lor r(x))}
  has the equivalent and proper formula

  
    
      
        G
        =
        ∀
        x
        ∃
        y
        
        (
        p
        (
        x
        ,
        f
        (
        y
        )
        )
        )
        ∧
        ∀
        z
        (
        q
        (
        z
        ,
        u
        )
        ∨
        r
        (
        z
        )
      
    
    {\displaystyle G=\forall x\exists y\;(p(x,f(y)))\land \forall z(q(z,u)\lor r(z)}
  


== Definition 9 ==
A formula is called in prenex form if it has the form 

  
    
      
        
          Q
          
            1
          
        
        ⋯
        
          Q
          
            n
          
        
        F
      
    
    {\displaystyle Q_{1}\cdots Q_{n}F}
  , where 
  
    
      
        
          Q
          
            i
          
        
        ∈
        {
        ∀
        ,
        ∃
        }
      
    
    {\displaystyle Q_{i}\in \{\forall ,\exists \}}
   with no
occurrences of a quantifier in 
  
    
      
        F
      
    
    {\displaystyle F}
  


== Theorem 2 ==
For every formula there is a proper formula in prenex form, which is
equivalent. 

Example:

  
    
      
        ∀
        x
        ∃
        y
        
        (
        p
        (
        x
        ,
        g
        (
        y
        ,
        f
        (
        x
        )
        )
        )
        ∨
        ¬
        q
        (
        z
        )
        )
        ∨
        ¬
        ∀
        x
        
        r
        (
        x
        ,
        z
        )
      
    
    {\displaystyle \forall x\exists y\;(p(x,g(y,f(x)))\lor \lnot q(z))\lor \lnot \forall x\;r(x,z)}
  
  
    
      
        ∀
        x
        ∃
        y
        
        (
        p
        (
        x
        ,
        g
        (
        y
        ,
        f
        (
        x
        )
        )
        ∨
        ¬
        q
        (
        z
        )
        )
        ∨
        ∃
        x
        
        ¬
        r
        (
        x
        ,
        z
        )
      
    
    {\displaystyle \forall x\exists y\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \exists x\;\lnot r(x,z)}
  
  
    
      
        ∀
        x
        ∃
        y
        
        (
        p
        (
        x
        ,
        g
        (
        y
        ,
        f
        (
        x
        )
        )
        ∨
        ¬
        q
        (
        z
        )
        )
        ∨
        ∃
        v
        ¬
        r
        (
        v
        ,
        z
        )
      
    
    {\displaystyle \forall x\exists y\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \exists v\lnot r(v,z)}
  
  
    
      
        ∀
        x
        ∃
        y
        ∃
        v
        
        (
        p
        (
        x
        ,
        g
        (
        y
        ,
        f
        (
        x
        )
        )
        ∨
        ¬
        q
        (
        z
        )
        )
        ∨
        ¬
        r
        (
        v
        ,
        z
        )
      
    
    {\displaystyle \forall x\exists y\exists v\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \lnot r(v,z)}
  

Proof: Induction over the structure of the formula gives us
the theorem for an atomic formula immediately.

  
    
      
        F
        =
        ¬
        
          F
          
            0
          
        
      
    
    {\displaystyle F=\lnot F_{0}}
  : There is a 
  
    
      
        
          G
          
            0
          
        
        =
        
          Q
          
            1
          
        
        
          y
          
            1
          
        
        ⋯
        
          Q
          
            n
          
        
        
          y
          
            n
          
        
        
          G
          ′
        
      
    
    {\displaystyle G_{0}=Q_{1}y_{1}\cdots Q_{n}y_{n}G'}
   with   
  
    
      
        
          Q
          
            i
          
        
        ∈
        {
        ∀
        ,
        ∃
        }
      
    
    {\displaystyle Q_{i}\in \{\forall ,\exists \}}
  , which is equivalent to 
  
    
      
        
          F
          
            0
          
        
      
    
    {\displaystyle F_{0}}
  . Hence we have 
  
    
      
        F
        ≡
        
          
            
              Q
              
                1
              
            
            ¯
          
        
        
          y
          
            1
          
        
        ⋯
        
          
            
              Q
              
                n
              
            
            ¯
          
        
        
          y
          
            n
          
        
        ¬
        
          G
          ′
        
      
    
    {\displaystyle F\equiv {\overline {Q_{1}}}y_{1}\cdots {\overline {Q_{n}}}y_{n}\lnot G'}
  where 
  
    
      
        
          
            
              Q
              
                i
              
            
            ¯
          
        
        =
        
          
            {
            
              
                
                  
                  
                  
                  ∃
                
                
                  i
                  f
                  
                    Q
                    
                      i
                    
                  
                  =
                  ∀
                
              
              
                
                  
                  
                  
                  ∀
                
                
                  i
                  f
                  
                    Q
                    
                      i
                    
                  
                  =
                  ∃
                
              
            
            
          
        
      
    
    {\displaystyle {\overline {Q_{i}}}={\begin{cases}\;\;\,\exists &ifQ_{i}=\forall \\\;\;\,\forall &ifQ_{i}=\exists \end{cases}}}
     

  
    
      
        F
        =
        
          F
          
            1
          
        
        ∘
        
          F
          
            2
          
        
      
    
    {\displaystyle F=F_{1}\circ F_{2}}
   with 
  
    
      
        ∘
        ∈
        {
        ∧
        ,
        ∨
        }
      
    
    {\displaystyle \circ \in \{\land ,\lor \}}
  . There exists 
  
    
      
        
          G
          
            1
          
        
        ,
        
          G
          
            2
          
        
      
    
    {\displaystyle G_{1},G_{2}}
   which are proper and in prenex form and 
  
    
      
        
          G
          
            1
          
        
        ≡
        
          F
          
            1
          
        
      
    
    {\displaystyle G_{1}\equiv F_{1}}
     and 
  
    
      
        
          G
          
            2
          
        
        ≡
        
          F
          
            2
          
        
      
    
    {\displaystyle G_{2}\equiv F_{2}}
  . With bounded renaming we can construct
  
    
      
        
          G
          
            1
          
        
        =
        
          Q
          
            1
          
        
        
          y
          
            1
          
        
        ⋯
        
          Q
          
            k
          
        
        
          y
          
            k
          
        
        
          G
          
            1
          
          ′
        
      
    
    {\displaystyle G_{1}=Q_{1}y_{1}\cdots Q_{k}y_{k}G_{1}'}
  
  
    
      
        
          G
          
            2
          
        
        =
        
          Q
          
            1
          
          ′
        
        
          z
          
            1
          
        
        ⋯
        
          Q
          
            l
          
          ′
        
        
          z
          
            l
          
        
        
          G
          
            2
          
          ′
        
      
    
    {\displaystyle G_{2}=Q_{1}'z_{1}\cdots Q_{l}'z_{l}G_{2}'}
  
where 
  
    
      
        {
        
          y
          
            1
          
        
        ,
        ⋯
        ,
        
          y
          
            n
          
        
        }
        ∩
        {
        
          z
          
            1
          
        
        ,
        ⋯
        ,
        
          z
          
            l
          
        
        }
        =
        ∅
      
    
    {\displaystyle \{y_{1},\cdots ,y_{n}\}\cap \{z_{1},\cdots ,z_{l}\}=\emptyset }
   and hence  
  
    
      
        F
        ≡
        
          Q
          
            1
          
        
        
          y
          
            1
          
        
        ⋯
        
          Q
          
            k
          
        
        
          y
          
            k
          
        
        
          Q
          
            1
          
          ′
        
        
          z
          
            1
          
        
        ⋯
        
          Q
          
            l
          
          ′
        
        
          z
          
            l
          
        
        (
        
          G
          
            1
          
          ′
        
        ∘
        
          G
          
            2
          
          ′
        
        )
      
    
    {\displaystyle F\equiv Q_{1}y_{1}\cdots Q_{k}y_{k}Q_{1}'z_{1}\cdots Q_{l}'z_{l}(G_{1}'\circ G_{2}')}
  

In the following we call proper formulae in prenex form PP-formulae or PPF’s.


== Definition 10 ==
Let 
  
    
      
        F
      
    
    {\displaystyle F}
   be a PPF. While 
  
    
      
        F
      
    
    {\displaystyle F}
   contains a 
  
    
      
        ∃
      
    
    {\displaystyle \exists }
  -Quantifier, do the
following transformation:

  
    
      
        F
      
    
    {\displaystyle F}
   has the form 

  
    
      
        ∀
        
          y
          
            1
          
        
        ,
        ⋯
        ∀
        
          y
          
            n
          
        
        ∃
        z
        
        G
      
    
    {\displaystyle \forall y_{1},\cdots \forall y_{n}\exists z\;G}
  
where 
  
    
      
        G
      
    
    {\displaystyle G}
    is a PPF and 
  
    
      
        f
      
    
    {\displaystyle f}
   is a 
  
    
      
        n
      
    
    {\displaystyle n}
  -ary function symbol, which does
not occur in 
  
    
      
        G
      
    
    {\displaystyle G}
  .
Let 
  
    
      
        F
      
    
    {\displaystyle F}
   be 

  
    
      
        ∀
        
          y
          
            1
          
        
        ,
        ⋯
        ∀
        
          y
          
            n
          
        
        
        G
        [
        z
        
          /
        
        f
        (
        
          y
          
            1
          
        
        ,
        ⋯
        ,
        
          y
          
            n
          
        
        )
        ]
      
    
    {\displaystyle \forall y_{1},\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})]}
  
If there exists no more 
  
    
      
        ∃
      
    
    {\displaystyle \exists }
  -quantifier, 
  
    
      
        F
      
    
    {\displaystyle F}
   is  in
Skolem form.


== Theorem 3 ==
Let 
  
    
      
        F
      
    
    {\displaystyle F}
   be a PPF. 
  
    
      
        F
      
    
    {\displaystyle F}
   is satisfiable iff the Skolem form of 
  
    
      
        F
      
    
    {\displaystyle F}
   is
satisfiable.
Proof: Let 
  
    
      
        F
        =
        ∀
        
          y
          
            1
          
        
        ⋯
        ∀
        
          y
          
            n
          
        
        ∃
        z
        
        G
      
    
    {\displaystyle F=\forall y_{1}\cdots \forall y_{n}\exists z\;G}
  ; after one
transformation according to the while-loop we have 

  
    
      
        
          F
          ′
        
        =
        ∀
        
          y
          
            1
          
        
        ⋯
        ∀
        
          y
          
            n
          
        
        
        G
        [
        z
        
          /
        
        f
        (
        
          y
          
            1
          
        
        ,
        ⋯
        ,
        
          y
          
            n
          
        
        )
      
    
    {\displaystyle F'=\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})}
  where 
  
    
      
        f
      
    
    {\displaystyle f}
   is a new function symbol.
We have to prove that this transformation is satisfiability
preserving:
Assume 
  
    
      
        
          F
          ′
        
      
    
    {\displaystyle F'}
   is satisfiable. than there exists a model 
  
    
      
        
          
            I
          
        
      
    
    {\displaystyle {\mathcal {I}}}
   for

  
    
      
        
          F
          ′
        
      
    
    {\displaystyle F'}
   
  
    
      
        
          
            I
          
        
      
    
    {\displaystyle {\mathcal {I}}}
   is an interpretation for 
  
    
      
        F
      
    
    {\displaystyle F}
  . From the model
property we have for all 
  
    
      
        
          u
          
            1
          
        
        ,
        ⋯
        ,
        
          u
          
            n
          
        
        ∈
        
          U
          
            
              I
            
          
        
      
    
    {\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}}
  

  
    
      
        
          
            
              I
            
          
          
            [
            
              y
              
                1
              
            
            
              /
            
            
              u
              
                1
              
            
            ]
            ⋯
            [
            
              y
              
                n
              
            
            
              /
            
            
              u
              
                n
              
            
            ]
          
        
        (
        G
        [
        z
        
          /
        
        f
        (
        
          y
          
            1
          
        
        ,
        ⋯
        ,
        
          y
          
            n
          
        
        )
        ]
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f(y_{1},\cdots ,y_{n})])=true}
  From Lemma 1 we conclude 

  
    
      
        
          
            
              I
            
          
          
            [
            
              y
              
                1
              
            
            
              /
            
            
              u
              
                1
              
            
            ]
            ⋯
            [
            
              y
              
                n
              
            
            
              /
            
            
              u
              
                n
              
            
            ]
            [
            z
            
              /
            
            v
            ]
          
        
        (
        G
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}
  where 
  
    
      
        v
        =
        
          
            I
          
        
        (
        f
        (
        
          u
          
            1
          
        
        ,
        ⋯
        ,
        
          u
          
            n
          
        
        )
      
    
    {\displaystyle v={\mathcal {I}}(f(u_{1},\cdots ,u_{n})}
  . Hence we have, that for all  
  
    
      
        
          u
          
            1
          
        
        ,
        ⋯
        ,
        
          u
          
            n
          
        
        ∈
        
          U
          
            
              I
            
          
        
      
    
    {\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}}
   there is  a 
  
    
      
        v
        ∈
        
          U
          
            
              I
            
          
        
      
    
    {\displaystyle v\in U_{\mathcal {I}}}
  , where 

  
    
      
        
          
            
              I
            
          
          
            [
            
              y
              
                1
              
            
            
              /
            
            
              u
              
                1
              
            
            ]
            ⋯
            [
            
              y
              
                n
              
            
            
              /
            
            
              u
              
                n
              
            
            ]
            [
            z
            
              /
            
            v
            ]
          
        
        (
        G
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}
  and hence we have, that 
  
    
      
        
          
            I
          
        
        (
        ∀
        
          y
          
            1
          
        
        ⋯
        ∀
        
          y
          
            n
          
        
        ∃
        z
        
        G
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\mathcal {I}}(\forall y_{1}\cdots \forall y_{n}\exists z\;G)=true}
  , which
means, that 
  
    
      
        
          
            I
          
        
      
    
    {\displaystyle {\mathcal {I}}}
   is a model for 
  
    
      
        F
      
    
    {\displaystyle F}
  .
For the opposite direction of the theorem, assume that 
  
    
      
        F
      
    
    {\displaystyle F}
   has a
model 
  
    
      
        
          
            I
          
        
      
    
    {\displaystyle {\mathcal {I}}}
  . Then we have, that for all  
  
    
      
        
          u
          
            1
          
        
        ,
        ⋯
        ,
        
          u
          
            n
          
        
        ∈
        
          U
          
            
              I
            
          
        
      
    
    {\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}}
  ,
there is  a 
  
    
      
        v
        ∈
        
          U
          
            
              I
            
          
        
      
    
    {\displaystyle v\in U_{\mathcal {I}}}
  , where 

  
    
      
        
          
            
              I
            
          
          
            [
            
              y
              
                1
              
            
            
              /
            
            
              u
              
                1
              
            
            ]
            ⋯
            [
            
              y
              
                n
              
            
            
              /
            
            
              u
              
                n
              
            
            ]
            [
            z
            
              /
            
            v
            ]
          
        
        (
        G
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}
  Let 
  
    
      
        
          
            
              I
              ′
            
          
        
      
    
    {\displaystyle {\mathcal {I'}}}
   be an interpretation, which deviates from 
  
    
      
        
          
            I
          
        
      
    
    {\displaystyle {\mathcal {I}}}
   only, by the
fact that it is defined for the function symbol 
  
    
      
        f
      
    
    {\displaystyle f}
  , where 
  
    
      
        
          
            I
          
        
      
    
    {\displaystyle {\mathcal {I}}}
   is
not defined. We assume that 
  
    
      
        
          f
          
            
              
                
                  I
                
              
              ′
            
          
        
        (
        
          u
          
            1
          
        
        ,
        ⋯
        ,
        
          u
          
            n
          
        
        )
        =
        v
      
    
    {\displaystyle f^{{\mathcal {I}}'}(u_{1},\cdots ,u_{n})=v}
  , where 
  
    
      
        v
      
    
    {\displaystyle v}
  
is chosen according to the above equation.
Hence we have that for all  
  
    
      
        
          u
          
            1
          
        
        ,
        ⋯
        ,
        
          u
          
            n
          
        
        ∈
        
          U
          
            
              I
            
          
          ′
        
      
    
    {\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}'}
  

  
    
      
        
          
            
              I
            
          
          
            [
            
              y
              
                1
              
            
            
              /
            
            
              u
              
                1
              
            
            ]
            ⋯
            [
            
              y
              
                n
              
            
            
              /
            
            
              u
              
                n
              
            
            ]
            [
            z
            
              /
            
            
              f
              
                
                  
                    
                      I
                    
                  
                  ′
                
              
            
            (
            
              u
              
                1
              
            
            ,
            ⋯
            ,
            
              u
              
                n
              
            
            )
            ]
          
          ′
        
        (
        G
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/f^{{\mathcal {I}}'}(u_{1},\cdots ,u_{n})]}(G)=true}
  and from Lemma 1 we conclude that for all  
  
    
      
        
          u
          
            1
          
        
        ,
        ⋯
        ,
        
          u
          
            n
          
        
        ∈
        
          U
          
            
              I
            
          
        
      
    
    {\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}}
  

  
    
      
        
          
            
              I
            
          
          
            [
            
              y
              
                1
              
            
            
              /
            
            
              u
              
                1
              
            
            ]
            ⋯
            [
            
              y
              
                n
              
            
            
              /
            
            
              u
              
                n
              
            
            ]
          
          ′
        
        (
        G
        [
        z
        
          /
        
        
          f
          
            (
          
        
        
          y
          
            1
          
        
        ,
        ⋯
        ,
        
          y
          
            n
          
        
        )
        ]
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f^{(}y_{1},\cdots ,y_{n})])=true}
  which means, that  
  
    
      
        
          
            
              I
            
          
          ′
        
        (
        ∀
        
          y
          
            1
          
        
        ⋯
        ∀
        
          y
          
            n
          
        
        
        G
        [
        z
        
          /
        
        f
        (
        
          y
          
            1
          
        
        ,
        ⋯
        ,
        
          y
          
            n
          
        
        )
        ]
        )
        =
        t
        r
        u
        e
      
    
    {\displaystyle {\mathcal {I}}'(\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})])=true}
  , and hence  
  
    
      
        
          
            
              I
            
          
          ′
        
      
    
    {\displaystyle {\mathcal {I}}'}
   is a model for 
  
    
      
        
          F
          ′
        
      
    
    {\displaystyle F'}
  .

The above results can be used to transform a Formula into a set of
clauses, its clause normal form:


== Problems ==


==== Problem 6 (Predicate) ====
Let 
  
    
      
        F
      
    
    {\displaystyle F}
   be  a formula, 
  
    
      
        x
      
    
    {\displaystyle x}
   a variable and 
  
    
      
        t
      
    
    {\displaystyle t}
   a term. Then 
  
    
      
        F
        [
        x
        
          /
        
        t
        ]
      
    
    {\displaystyle F[x/t]}
   denotes the formula which results from 
  
    
      
        F
      
    
    {\displaystyle F}
   by replacing  every free
occurrence of 
  
    
      
        x
      
    
    {\displaystyle x}
    by 
  
    
      
        t
      
    
    {\displaystyle t}
  . Give a formal definition of this three argument function  
  
    
      
        F
        [
        x
        
          /
        
        t
        ]
      
    
    {\displaystyle F[x/t]}
  ,  by induction over  the structure of
the formula 
  
    
      
        F
      
    
    {\displaystyle F}
  . 

  
    
      
        ◻
      
    
    {\displaystyle \Box }
  


==== Problem 7 (Predicate) ====
Show the following semantic equivalences:

  
    
      
        ∀
        x
        (
        p
        (
        x
        )
        →
        (
        q
        (
        x
        )
        ∧
        r
        (
        x
        )
        )
        )
        ≡
        ∀
        x
        (
        p
        (
        x
        )
        →
        q
        (
        x
        )
        )
        ∧
        ∀
        x
        (
        p
        (
        x
        )
        →
        r
        (
        x
        )
        )
      
    
    {\displaystyle \forall x(p(x)\to (q(x)\land r(x)))\equiv \forall x(p(x)\to q(x))\land \forall x(p(x)\to r(x))}
  

  
    
      
        ∀
        x
        (
        p
        (
        x
        )
        →
        (
        q
        (
        x
        )
        ∨
        r
        (
        x
        )
        )
        )
        ≢
        ∀
        x
        (
        p
        (
        x
        )
        →
        q
        (
        x
        )
        )
        ∨
        ∀
        x
        (
        p
        (
        x
        )
        →
        r
        (
        x
        )
        )
      
    
    {\displaystyle \forall x(p(x)\to (q(x)\lor r(x)))\not \equiv \forall x(p(x)\to q(x))\lor \forall x(p(x)\to r(x))}
  
  
    
      
        ◻
      
    
    {\displaystyle \Box }
  


==== Problem 8 (Predicate) ====
Show the following semantic equivalences:

  
    
      
        (
        ∀
        x
        p
        (
        x
        )
        )
        →
        q
        (
        b
        )
        ≡
        ∃
        x
        (
        p
        (
        x
        )
        →
        q
        (
        b
        )
        )
      
    
    {\displaystyle (\forall xp(x))\to q(b)\equiv \exists x(p(x)\to q(b))}
  

  
    
      
        (
        ∀
        x
        r
        (
        x
        )
        )
        ∨
        (
        ∃
        y
        ¬
        r
        (
        y
        )
        )
        ≡
        (
        ∀
        x
        r
        (
        x
        )
        )
        →
        (
        ∃
        y
        r
        (
        y
        )
        )
      
    
    {\displaystyle (\forall xr(x))\lor (\exists y\lnot r(y))\equiv (\forall xr(x))\to (\exists yr(y))}
  
  
    
      
        ◻
      
    
    {\displaystyle \Box }
  


==== Problem 9 (Predicate) ====
Show that for arbitrary formulae  
  
    
      
        F
      
    
    {\displaystyle F}
   and 
  
    
      
        G
      
    
    {\displaystyle G}
  , the following holds:

  
    
      
        ∀
        x
        (
        F
        ∨
        G
        )
        ≢
        ∀
        x
        F
        ∨
        ∀
        x
        G
      
    
    {\displaystyle \forall x(F\lor G)\not \equiv \forall xF\lor \forall xG}
  
If 
  
    
      
        G
        =
        F
        [
        x
        
          /
        
        t
        ]
      
    
    {\displaystyle G=F[x/t]}
  , than  
  
    
      
        G
        ⊨
        ∃
        x
        F
      
    
    {\displaystyle G\models \exists xF}
  .
  
    
      
        ◻
      
    
    {\displaystyle \Box }