Evaluating a proposition that is empty Here is a silly example to illustrate my question:
Definition We call a function zeroed-at-one if $f(1)=0$.
If $1$ is not in the domain of $f$, is the statement "$f$ is zeroed-at-one" true or false? The problem is that $f(1)$ is undefined.
Consider that Wolfram MathWorld states: "Undefined: An expression in mathematics which does not have meaning and so which is not assigned an interpretation."
Let: 
P = "$f(1)=0$"
Q = "$f$ is called "zeroed-at-one". 
If $f(1)$ is undefined, is P true or false, or does it have no meaning/interpretation? 
Can we say that, for this definition, we have P $\Rightarrow$ Q, or P$\Leftrightarrow$ Q? I think we really want an "if and only if" for definitions since if P is false and Q is true, then P$\Rightarrow$Q is true, but P$\Leftrightarrow$ Q is false. If P is meaningless in such a case, then is it the case that we can neither say $f$ satisfies the definition, nor that $f$ does not satisfy the definition?
I feel that we want P here to be false if $f(1)$ is undefined, but how is that justified? Moreover, how is it properly notated in formal logic, and how is the undefined issue dealt with there?
 A: I believe as you have it written, part of the definition of being zeroed-at-one requires that $1$ be in the domain and $0$ be in the codomain. If either of those conditions are not met, you have no chance to be zeroed-at-one, and so you would say that the statement "$f$ is zeroed-at-one" is false. Basically, your definition is not explicit enough, and I think that any reasonable mathematician would assume what I have about the implict requirements.
A: It depends on what logical framework you're working in. If, as your tags suggest, $f$ is a function symbol in a first-order theory with $1$ and $0$ being constants, then $f$ can't not be defined at $1$. Either you're working in a single-sorted FOL, and thus every function symbol is applicable to every term (there is only one "domain"), or you're working in a multi-sorted FOL and either $1$ is of the appropriate sort to be an input to $f$ and so $f$ is defined at $1$, or it's not and your definition itself is just syntactically ill-formed.
If you want to talk about functions that are partially defined, you would typically model them as predicates in FOL. You'd have a predicate $P(x,y)$ that informally corresponded to "$f$ is defined at $x$ and $f(x)=y$". "Zeroed-at-one" would then be the assertion that $P(1,0)$ holds. This is also effectively what happens if you want to consider this as working in set theory. That is, $f(1)=0$ is often viewed as being short-hand for $(1,0)\in f$ in a set theoretic context. Using the set theoretic view, if $1$ is not in the domain of $f$, then $(1,0)\in f$ is certainly false and so $f$ would not be "zeroed-at-one". There is never an "undefined" value.
A: The answer by Derek Elkins explains how this is treated in first-order logic: we use relations instead of functions when the functions may not be total, or we use set theory so that we can ask explicitly whether elements are in the domain of the function. 
There is an alternative: we can change to a different "free logic" in which there can be terms (such as "f(0)") that do not actually denote anything.  These are called "singular terms". 
Free logic is unlike first-order logic where all terms must denote, but more like English where "the 12th king of the United States" is a well formed noun phrase that does not denote any person.  For this reason, free logic is more heavily studied in linguistics and philosophy than in mathematical logic. 
In free logic, there are several ways of defining the truth of formulas when they may have singular terms. Generally, in free logics that require every formula to be true or false in each interpretation, if $f(0)$ is a singular term then $f(0) = 1$ is teated as false provided that the term $1$ does denote something. In other words, a singular term cannot be equal to a denoting term in these logics, and a claim that they are equal evaluates to false. 
There are many more details about free logic in the link above, so I will not try to go much further here, but they do provide an established basis for reasoning in the presence of singular terms. 
A: Consider the definition of continuity of a function for comparison:

The function $f$ is continuous at some point $c$ of its domain if the limit of $f(x)$, as $x$ approaches $c$ through the domain of $f$, exists and is equal to $f(c)$.

As you can see, there's a slight difference with your definition. In this case the definition includes that $c$ must be in the domain. Therefore both continuous and discontinuous are not defined at a point $c$ that is not in the domain of the function.
Since you did not include the domain-condition in your definition, we must assume that not-zeroed-at-one means that either $f(1)$ is undefined, or $f(1)\ne 0$ as JDMan already pointed out.
Edit: There is a certain abuse of definition where discontinuity is concerned when talking about a removable discontinuity.

The term removable discontinuity is an abuse of terminology for cases in which the limits in both directions exist and are equal, while the function is undefined at the point $c$. This use is abusive because continuity and discontinuity of a function are concepts defined only for points in the function's domain. Such a point not in the domain is properly named a removable singularity.

