Some people think that the identity notion is captured by the second proposal above. I think we need two notions of identity. I will not discuss that now.
For all things, for all things, for all predicates, that x and y are strictly identical logically implies that that x has predicate F is logically equivalent with that that y has predicate F.
(∀x)(∀y)(∀F)(x=Sy⇔(Fx⇔Fy)) [with obvious interpretation and =S meaning strict identity]
This is called Liebniz’s law.
“I think Liebniz’s law accommodates personal identity quite comfortably with the addition of a time quantifier: x and y are identical if any property possessed by x at time t is also possessed by y at time t. If you add a world quantifier it can also handle transworld identity rather well.“
For all things, for all things, for all predicates, for all times, that x and y are personally identical logically implies that that x has predicate F at time t is logically equivalent with that that y has predicate F at time t.
(∀x)(∀y)(∀F)(∀t)(x=Py⇔(Fxt⇔Fyt)) [with obvious interpretation and =P meaning personal identity]
This seems to work.
But I don’t understand the part about transworld identity. It seems to me that the above can handle transworld identity fine.