Necessary ICs

A formula G is a necessary IC for f if

f(x,t) _ f(y,tí) _ x=y _ G(x,y,t,tí)

Ö provided that:

• it is not equivalent to universal identity:

  ¨_xyttí G(x,y,t,tí) _ x=y
  

• it is not trivially true of all fs:

  ¨_xyttí f(x,t) _ f(y,tí) _ G(x,y,t,tí)
  

Previous slide

Next slide

Back to first slide

View graphic version