Predicate Logic Representation

Question

How do you represent arithmetic operations with predicate logic? For example if I want to represent 2+3 = 5 in predicate logic with plus(x,y) function is the following correct?

plus(2,3) <=> 5

But ideally <=> is equivalent and not equal. So is the above representation wrong?How do you represent something like this with predicate logic?

Answer 1

If you use plus as a function symbol, then you may write plus(2,3)=5; if you wish to formalize as a predicate you need a ternary predicate plus(2,3,5). The latter option is less common, but very fine too.

EDIT, July 2020

Just to be clear, if you use functions (and basic = rules), it is hard coded in the settings itself that, for all a, b, there is a unique c such that plus(a,b)=c (you may prove it!). In the predicate case, you need to state that explicitly (add it as an axiom):

$\forall a,b \exists! c \; plus(a,b,c)$,

where $\exists!c$ is: there is a unique c, i.e.

$\forall a,b ( \exists c \; plus (a,b,c) \wedge ( \forall d,d' ( plus(a,b,d) \wedge plus(a,b,d') \rightarrow d=d' \; )))$,