I am confused a bit, is the following formul a syntactically valid formula of first order logic?
is_VAT_taxable_good(milk) ->
price_with_VAT(good)=price(good)+apply_highest_VAT_rate(price(good))
where
is_VAT_taxable_good(...) - predicate
pricate_with_VAT, price, apply_highest_VAT_rate, ...+... - functions
good - constant
(the language of first order logic, of course, allows to use funnctions inside terms). So – is my initial implication a syntactically valid first order formula (wrt the language with the mentioned functions, variables and constants). If it is not syntactically valid formula, then what is wrong with it and how differently and in right manner I can express the same implication?
Or maybe I should make distinction between logical equality of first order logic and my own custom equality that I can define on two terms as custom 2-ary function e.g. =(..., ...). If that is the case the in which situations should I define such custom equality function and in which situations I can use the build in FOL equality? Is there theory of such custom equality in FOL?
Best Answer
Your formula looks fine, as your implication, as @Derek Elkins said, combines validly built atomic formulas together, while these are in turn formed using the equality relation and a function applied to good, whatever this represents in your underlying language.
In think the second concern/question about equality or the equality symbol $=$ is a little more engaging. First, you should note that on a syntactical level, that is on the formal language level of first order logic, $=$ is just a symbol, initially with no attached meaning. The meaning is supplied via semantics. In first order logic, one often differentiates between first order logic with equality and first order logic without equality.
FO with equality incorporates $=$ as a prime symbol into the signature/language and forces its interpretation in a model $\mathfrak{M}=\langle M,\dots\rangle$ to be an object equality, i.e. (without getting into too much formalism) the syntactical structure $a=b$ with variables(or constants, terms) $a,b$ is true under an interpretation if the objects of $M$ assigned to $a$ and $b$ are the same, i.e. are equal on the meta-level.
FO without equality essentially omits this concept as a primitve. The reasons for distinction is largely historic and I omit any further details now.
What I think is more important, is that of course you can add a relation symbol to the signature/language as a custom equality symbol and enforce some kind of behaviour by restricting the desired models to those having the corresponding properties, e.g. through a corresponding axiomatization of a desired model class, that is you may specify the class of models you want to consider as the models of some set of first order sentences:
Say you might want to create another type of equality in some context, written syntactically in the formal language as $\equiv$ for which you may ask different properties from, e.g. transitive behaviour
$$\forall x\forall y\forall z:x\equiv y\rightarrow(y\equiv z\rightarrow x\equiv z)$$
Classical equality as perceived e.g. in mathematics of course has other properties as well like symmetry etc., which you may omit or add depending on whatever you try to model(where model is a great descriptor, as you restrict the class of models to those already satisfying your required properties).
Since it seems that your question comes from a more applied background, let me end with that it depends largely on what you try to model and how you want to model it, but you may always, and this is the great strength and diversity of FO compared to e.g. (in a drastic way) classical propositional logic, specify a signature of symbols representing functions and relations for some scenario for which you then can specify semantic properties syntactically through corresponding formulas.
EDIT: I'm sorry if I drove off a little bit, concerning your question I was not sure if you asked for soft discussion, elaboration of a concept or a more formal treatment of these questions.