The user didn't delete the file, the system did. The user merely removed the file from his own directory. The system deleted the file because its reference count dropped to zero. It's just happenstance that the user removing the file from the directory happened to drop its reference count to zero. (If the file was hard linked to another directory or a handle was opened to the file, it would not have been deleted.)
The system deletes files automatically when their reference counts drops to zero. The owner of the file doesn't matter. There are many ways someone other than the owner of a file can drop the file's reference count to zero.
Removing a file from a directory (called 'unlinking') is an operation on the directory. Unlinking a file reduces its reference count.
Similarly, a user other than the owner could close the last handle to a file that isn't linked to any directories. Closing that handle would delete the file as well, since again the reference count would drop to zero.
@DavidSchwartz that's true, but deleting the file from the directory is about removing the reference in the directory structure. – mc0e – 2017-04-23T11:47:16.420
>
sudo
or other privilege escalation. You probably overlooked something.16@DarkDust A file is an entry in its parent directory. If you have write rights in a directory, you can remove files in it regardless of who owns the files (unless the sticky bit is also set on the directory) – nos – 2011-12-19T13:13:02.300
@nos: Silly me, you're right. – DarkDust – 2011-12-19T13:14:28.420
1An entry in its parent directory is a reference to a file. It is not the file itself. (Otherwise, how could a file be hard linked to more than one directory?) – David Schwartz – 2011-12-19T14:59:12.697