Is it correct that an interpretation for a first order logic system is defined for the first order language of the logic system, without the axioms and inference rules in the logic system being considered?
When we study whether an interpretation is a model for a given formula in a first order language, how do we know whether the interpretation of the formula is true or false?
Does an interpretation include a function which assigns truth values to all the propositions (i.e. the meanings of all the formulas provided by the interpretation)? How is such a function constructed, if the interpretation doesn't contain counterparts of axioms and of inference rules?
Thanks.
It is not the interpretation which is true or false: We say that a formula is true or false under an interpretation.
Yes. An interpretation for a language of FOL is one which is defined for all the non-logical symbols (individual constants, function symbols, predicate symbols) of the language, independently of the axioms that hold in a language.
I'm not sure I correctly understand your question. The truth value of a formula is already defined relative to interpretations, so checking the truth value of a formula under an interpretation just means recursively applying the definitions of the semantics.
No. Unlike in propositional logic, where interpretations directly assign truth values to propositional letters, in FOL interpretations only assign meanings to the non-logical symbols (that is, the individual constants, function symbols and predicate symbols), and the truth value of propositions is then recursively computed relative to this interpretation.
In principle, as long as it follows the definition of a first-order structure, you can define your interpretation however you want, if you're talking about just in general interpretations of FOL. If you are in a specific theory, you will have a certain language, and want an interpretation relative to that language, and if you want an interpretation that is a model of the theory, i.e. in which all the theorems of the theory are true, you will have to think more closely about what your interpretations must look like so they satisfy all the axioms.
But normally in mathematical practice, it goes the other way round: You have a mathematical structure with an intended interpretation for the symbols in mind, and you try to find a logical system that describes exactly this structure. Semantics first, axioms and inference rules second. This "intended interpretation" will then be the standard model of the theory, though in general there also exist non-standard models which satisfy the axioms of the theory as well. For example, the structure of the natural numbers with the intended definitions of addition, multiplication etc. is the standard model of Peano arithmetic, which is a first-order theory whose axioms describe exactly how addition etc. behaves, and thus the formulas that are true in all interpretations that are models of the theory (such as the standard model) are precisely the facts about natural number arithmetic.
As said, I'm not entirely sure I understood your question correctly because I would assume that if you talk about interpretations and theories of FOL, you already know how the semantics of FOL works, i.e. what an $\mathcal{L}$-structure with domain and interpretation function is, and how the truth value of a formula relative to an interpretation is defined recursively. In that case, I think you will have to rephrase your question to make it clearer what you want to know about.
But if you don't know what an FOL interpretation is, which your second question seems to suggest, I strongly recommend you first grab a good book that teaches the basics of FOL, before going into things such as axioms and first-order theories. It doesn't make much sense here for me to repeat the definitions of the semantics of FOL, which you will find explained in much more detail along with examples. After understanding what an interpretation is, your questions might resolve themselves.