| T.R | Title | User | Personal Name
 | Date | Lines | 
|---|
| 1214.1 |  | AITG::DERAMO | Dan D'Eramo, nice person | Tue Mar 27 1990 17:17 | 17 | 
|  |         Use the equivalences: not for all x not <==> the exists an x
        		      not there exists a y not <==> for all y
        		      not not <==>
        
        So
        
        	for all x, there exists a y such that P(x,y)
        <==>
        	not there exists an x not not for all y not P(x,y)
        <==>
        	not there exists an x for all y not P(x,y)
        
        So the negation of that will be just
        
        	there exists an x such that for all y, not P(x,y)
        
        Dan
 | 
| 1214.2 |  | JARETH::EDP | Always mount a scratch monkey. | Tue Mar 27 1990 17:18 | 13 | 
|  |     Re .0:
    
    I don't think you can simply invert the quantifiers.  Why do you want
    to?  If you just want "there exists" to appear for "for all", you can
    write the statement as:
    
    	- (there exists an x such that (for all y, -P(x,y))).
    
    Note that the first possibility you wrote is actually the negation of
    the original statement; the statement above is equivalent to the
    original.
    
    				-- edp
 | 
| 1214.3 |  | AITG::DERAMO | Dan D'Eramo, nice person | Tue Mar 27 1990 17:25 | 17 | 
|  |         Essentially, a not can trade places with a for_all or a
        there_exists if in doing so it flips the quantifier to
        the other kind.
        
        not		for_all x there_exist y p(x,y)
           not		for_all x there_exist y p(x,y)
              not       for_all x there_exist y p(x,y)
                 not    for_all x there_exist y p(x,y)
                    not for_all x there_exist y p(x,y)
        		B U M P !
        	    there_exists x not there_exist y p(x,y)
        		B U M P !
        	    there_exists x for_all y not P(x,y)
        
        The running start helps but isn't necessary. :-)
        
        Dan
 |