Counting quantification

<h2 id="definition-in-terms-of-ordinary-quantifiers">Definition in terms of ordinary quantifiers</h2>
<p>Counting quantifiers can be defined <a href="/facts/Recursive_definition/9RfhFw0R">recursively</a> in terms of ordinary quantifiers.
</p><p>Let 
  
    
      
        
          ∃
          
            =
            k
          
        
      
    
    {\displaystyle \exists _{=k}}
  
 denote "there exist exactly 
  
    
      
        k
      
    
    {\displaystyle k}
  
". Then
</p>

∃
                  
                    =
                    0
                  
                
                x
                P
                x
              
              
                
                ↔
                ¬
                ∃
                x
                P
                x
              
            
            
              
                
                  ∃
                  
                    =
                    k
                    +
                    1
                  
                
                x
                P
                x
              
              
                
                ↔
                ∃
                x
                (
                P
                x
                ∧
                
                  ∃
                  
                    =
                    k
                  
                
                y
                (
                P
                y
                ∧
                y
                ≠
                x
                )
                )
              
            
          
        
      
    
    {\displaystyle {\begin{aligned}\exists _{=0}xPx&\leftrightarrow \neg \exists xPx\\\exists _{=k+1}xPx&\leftrightarrow \exists x(Px\land \exists _{=k}y(Py\land y\neq x))\end{aligned}}}

<p>Let 
  
    
      
        
          ∃
          
            ≥
            k
          
        
      
    
    {\displaystyle \exists _{\geq k}}
  
 denote "there exist at least 
  
    
      
        k
      
    
    {\displaystyle k}
  
". Then
</p>

∃
                  
                    ≥
                    0
                  
                
                x
                P
                x
              
              
                
                ↔
                ⊤
              
            
            
              
                
                  ∃
                  
                    ≥
                    k
                    +
                    1
                  
                
                x
                P
                x
              
              
                
                ↔
                ∃
                x
                (
                P
                x
                ∧
                
                  ∃
                  
                    ≥
                    k
                  
                
                y
                (
                P
                y
                ∧
                y
                ≠
                x
                )
                )
              
            
          
        
      
    
    {\displaystyle {\begin{aligned}\exists _{\geq 0}xPx&\leftrightarrow \top \\\exists _{\geq k+1}xPx&\leftrightarrow \exists x(Px\land \exists _{\geq k}y(Py\land y\neq x))\end{aligned}}}

<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Uniqueness_quantification/qBpdIqel">Uniqueness quantification</a></li>
<li><a href="/facts/Lindstr%C3%B6m_quantifier/8dGIA4Pt">Lindström quantifier</a></li>
<li><a href="/facts/Spectrum_of_a_sentence/RWueT8u6">Spectrum of a sentence</a></li></ul>

<ul><li>Erich Graedel, Martin Otto, and Eric Rosen. "Two-Variable Logic with Counting is Decidable." In <i>Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97</i>, Warschau. 1997. <a href="http://www-mgi.informatik.rwth-aachen.de/Publications/pub/graedel/gorc2.ps">Postscript file</a> <a href="/facts/OCLC_(identifier)/Yqad8waq">OCLC</a> <a href="https://www.worldcat.org/oclc/282402933">282402933</a></li></ul>

Counting quantification open-in-new

Counting quantification