A gráfok szokásos elsőrendű nyelvén nem formalizálható, hogy út van két pont között. Ezt mutatja az az ultraszorzatos konstrukció, amit néhány hozzászólással ezelőtt írtam. ZFC-ben viszont eddig úgy tűnik, hogy minden kényelmesen formalizálható, még ZFC konzisztenciája is megfogalmazható.