In Model Theory the satisfiability conditions for a quantified formula expressed in First Order Logic are stated according to an assignment function, which mach each variable to each object of the domain well-ordered in sequences. I was wondering: in an infinite non-denumerable domain the Axiom of Choice - or some other version of it - is required to obtain well-ordered sequences to which apply the assignment function?
Sorry for the rough question, I come from a Philosophy department. Hope that the point is clear!
Not really. The axiom of choice does not come into play at all when defining satisfaction and truth.
Since a first-order formula has only finite length, assignments agreeing on those finitely many variables appearing in a given formula must agree on the truth value.
Moreover, the assignment and truth value are given by recursion on complexity of formulas. This is a well-founded relation because formulas are finite in first-order logic, and this has nothing to do with the axiom of choice. Consequently, we can define the recursive process without worrying about a well-ordering at all.
The axiom of choice, however, does play a small role in the study of logic. The compactness theorem for first-order logic, which is equivalent to the completeness theorem, requires a weak fragment of choice in general, because there we do not look only at a single formula at a time, but rather at a large collection of formulas. Regardless of that, if the language itself can be well-ordered, then choice is not needed since we can use that well-order to follow the standard proof easily.