I am looking into the practicalities of doing Math in FOL + PA with the FOL extended with equality and functions.


For a predicate you can easily extend the language such that a predicate is defined as a logical expression, which then can be comprehended or expanded in the proofs and theorems that follow.


However, if you want to do the same for a function, then it should be proven that the function is deterministic (giving only one result for a certain set of parameters) and total. If you define the function with other functions, then it that is obvious. However, if the function is defined using logical expressions then it is not obvious.


If I look in the literature I see often a function popping up (such as Gödel's β function) without this explicit proof. I assume that it has informally proven, but since I want to write a piece of text about this, my question is if there are any conventions how to deal with this and how you normally incorporate this in a logic language that can checked by a theorem checker?


This is not very theoretical, since you can get rid of function and rewrite the expressions as predicates.


Thanks in advance,


Lucas



Defining functions in FOL + PA
You might avoid the issue in first-order arithmetic by assuming that a function always selects the least option, or zero if there is no option. So a definition like
$$R(x,y,z)=z<y \wedge \exists v:x = vy+z$$
would actually be transformed into
$$R'(x,y,z)=(R(x,y,z) \wedge \forall w:R(x,y,w)\implies z\le w) \vee (z=0 \wedge \forall z: \neg R(x,y,z))$$


Alternatively, you might follow Solomon Feferman in using logical frameworks flexible enough to include symbols for partial functions and for [definedness](https://virtualmath1.stanford.edu/%7Efeferman/papers/definedness.pdf).


