There are no assignment functions in formal mathematics. – Dan Christensen
Given the comments on this post, let's get into the philosophy of language. The TLDR is assignment is a form of definition, the stipulative definition, and all theories employ it, though philosophy, mathematics, and computer science go about it in their own, overlapping dialects. Assignment is a speech act that imputes truth to a proposition.
There certainly are assignment functions in all theories, and even though are usually not referred to as such, we call them definitions. In mathematics, the magical 'let' is a speech act which transforms a conjecture or intuition into a true proposition. "Let x be 5" is a mathematical assignment insofar as it assigns a value to a variable. Why is it true? Because the author says so! This is what stipulate means. Logicians of course have formalized this sort of practice a bit, but the actual act itself nonetheless has the function of assignment, even if it isn't often recognized as such.
There's a certain interconnection between logic, mathematics, and computer science (as recognized by Curry-Howard and also by intuitionist mathematical philosophers (such as Per Martin-Löf and others). Therefore it should be no surprise that assignment occurs in all three, albeit in different ways.
- In logic, assignment is usually done with the syntax and semantics of existential and universal quantification explicitly. (∃x∀y)
- In mathematics, assignment is usually done with the syntax and semantics of existential and universal quantification implicitly often with arithmetic and set-theoretic operators (x=5:x∈ℕ)
- In computer assignment, assignment is usually done with the assignment operator and other peculiar syntactical conventions (x:=6.2f;)
The only place that 'assignment' is dealt with in any kind of formal context is in formal logic
Computer science takes assignment very seriously because computer scientists who write compilers have to create a syntax (usually expressed in BNF) and manufacture an adequate semantics for it (write a functional compiler). Therefore, there are formalisms related to compiler design that persist because assignment is a first-class operation (in fact, one simply can't write a programming language without them). Furthermore, formalisms of machines are usually written in set-theoretic (read mathematical) terms, where assignment is conveyed by the notion of functional mappings. Turing machine definitions include the concept of initial state, and assignment operation can be seen as taking inputs and associating them with initial state. Thus, a compiler may create a variable in a table and assign it an initial state of 0, but then given additional syntax, may then set that value to what the programmer wants after the act of creating the variable. In Dartmouth's original form of BASIC, the syntax actually used "LET" reflecting the mathematical origins of computer science.
Now, the act of definition does have some wrinkles in it, for example the advocates of early truth-conditional semantics (Frege, Russell, et al.) consider definitions imperatives and incapable of truth values, but a more relaxed interpretation of definition (there are three schools of thinking on the nature of definition in the literature) differentiates the act of definition or assignment from that of the proposition it contains much in the way propositional attitude and the propositions themselves are distinct entity. Thus, the imperative "assign 5 to x" can be read as "Let it be true S" where S is "x=5". To me, it's unintentional equivocation to confuse the speech act of definition with the actual definition itself much in the way that an assertion is more than a proposition.
Some of the comments indicate some scrapping over the phrase "assignment function", so what is fair to infer is that "assignment function" means different things to different people, however, part of the methodology of analytic philosophy is to examine the language, and try to make sense of defintions and their use. Thus, it's plain to an analytical philosopher that "assignment function" can be interpreted in several ways:
- Formal mathematical function language where mappings are constructed using canonical notation such as f:AxB where assignment is done by calculation.
- Computer science language where assign() can be used invoking imperative and declarative statements using something like := for assignment.
- The logical notions are explicated on by lemontree
But in the end, all assignment reduces to notions of definition which is to be understood as a philosophical topic in the philosophy of language. The best resource I own on definitions (and by extension the philosophical underpinnings of assignments) is Robinson's Definition which has a copyright of 1954 and is from Oxford Press. No preview is possible for Google Books. Looks like there are a few contemporaneous attempts also.
To what extent can we evaluate the idea of 'truth' in a variable assignment, is there a concept of a formula being 'true' under an assignment?
So, there to review and answer your question explicitly, there is a concept of a formula (form, statement, utterance, proposition, etc.) being true under an assignment, and is known as a definition which enjoys its own taxonomy. In mathematics, logic, and computer science, such assignments are generally species of stipulative definition. From Robinson, p. 61:
'Let us mean by a "pencil" a right cylinder whose cross-section is a regular polygon... This type of nominal definition was called 'sipulation' by James Mackaye in his The Logic of Language.