If I understand correctly, the first formula expresses a contradiction, since F will always satisfy the existential. I get that you're trying to rule out F's existence by saying it doesn't satisfy the tautologous (∀x)(Fx → Fx), but as far as I can tell the result is just a sentence that can't ever be true.

Same holds for the second.

It's tricky what you mean by a property not existing: you can of course say that no individual bears the property, but that can be done in first-order. The fact that you are using the symbol F at all already commits your ontology to the property denoted by F to 'existing' in the minimal sense that it's in the domain of quantification of property-variables. If you wanted to say it didn't exist while quantifying over it, you'd have to have some alternate notion of existence, maybe expressed by an existence predicate on properties (that might return true just in case the property holds of no individual, or cannot hold of any individual).

It's the same puzzle about how to express that a certain individual doesn't exist in first-order logic. Suppose you write something like:

~(∃x)(x = a)

But that requires the individual denoted by 'a' to be in your domain, and so in the domain of quantification of individual variables. Even to say that whatever 'a' denotes doesn't exist, then, is to commit yourself to its 'existence' in this minimal (Meinongian) sense.

Thanks for the answer.