 Turning to the last two lines,  we already know that AFA is equivalent to the assertion that  (V, id)  is a final coalgebra of ℘; also, even without  AFA, we have a final coalgebra whose carrier set is the pointed graphs modulo bisimulation.   The logic in this case is infinitary modal logic, actually, it is a fragment of this logic.   It turns out that two points in a given coalgebra have the same infinitary modal theory iff they are bisimilar.  