Practice for the exam: formalize this sentence about Twitter

[Ian W.]

Today Twitter got in trouble because they changed how the site worked.
They then tried to fix it by making another change. Here's how they
described the second change:

"[Any] updates beginning with @username (that are not explicitly
created by clicking on the reply icon) will be seen by everyone
following that account."

This confused the hell out of everybody on the internet. So here's a
challenge: formalize this sentence in first-order logic. You can make
up whatever predicates you like, for example Update(x) meaning x is an
update, BeginsWith(x,user) meaning the update starts with the string
corresponding to user, IsReplyTo(x,y) means x is a reply y, Sees
(user,x) means user sees messages x, and Follows(user1,user2) means
user1 follows user2. I'm probably missing a few. Anyway, post your
answers here and in the meantime see if you can figure out how Twitter
actually works!

Ian

[Anar Seyf]

[ forall follower in Users :
forall x,y in Updates :
( !(isReplyTo(x,y))
& (BeginsWith(x,atUsername(user)))
& (user in Users)
& (Follows(follower, user) )
--> Sees(follower, x) ],

where
- atUsername returns a string concatenation of "@" and username,
- Users = { set of all users },
- Updates = { x : Update(x) },
- user is a free variable throughout the formula.

Close?

Anar

[Ian W.]

I think so. My only nitpick is that you probably also want to quantify
over "user" as well. In my translation, which I believe is equivalent,
I moved the quantifier over followers of the user into the conclusion
of the implication. But, again, I believe that to be an equivalent
formulation.

Nice job!

Ian