Is formal truth in mathematical logic a generalization of everyday, intuitive truth? I'm trying to wrap my head around the relationship between truth in formal logic, as the value a formal expression can take on, as opposed to commonplace notions of truth.
Personal background: When I was taking a class in formal logic last semester, I found that the most efficient way to do my homework was to forget my typical notions of truth and falsehood, and simply treat truth and falsehood as formal, abstract values that formal expressions may be assigned. In other words, I treated everything formally, which from the name of the course is presumably what I was supposed to do while solving problems.
On the other hand, I came out of the course more confused than enlightened about what truth refers to in mathematics. For example, on what levels are each of the following two statements "true"?

  
*
  
*There are infinitely many prime numbers.
  
*The empty function $f\colon \emptyset \to \mathbb R $ is injective.
  

For the first one, I can obviously see that there would be a contradiction if there were only finitely many prime numbers. To me, the classic proof by contradiction is not a "formal proof" or anything; it is merely a natural language argument that proves (in the everyday sense of the word "proves") why the statement must be true (in the everyday sense of the word "true").
On the other hand, I run into trouble when I try to think about the second one. The very concept of the "empty function" doesn't even feel like it makes sense, but if I think about it as the relation between $\emptyset$ and $\mathbb R$ containing no elements, and then try to write out the statement formally, I get (if I did it correctly)

$
\forall x \forall y ( ((x\in \emptyset) \land (y\in \emptyset) \land (f (x) = f (y))) \implies (x=y))
$

which I think has to be true in a formal sense (since the antecedent is always false?). But to be honest, I don't really know how to think about "truth" here; the situation feels much more confusing than with the first statement.
So, in conclusion, my questions are:

In what sense is each of the above statements "true"? And, more generally,
Is the notion of truth in (mathematical) logic just a formal value assigned to expressions? Or should I think of it as encompassing, but also generalizing, the intuitive notion of a true statement?

(Any insightful comments or answers are appreciated, even if they don't address all of my questions directly.)
 A: From a philosophical point of view this is really a big question to ask! Actually one would need a good notion of all day truth as well as of mathematical truth, to answer this question. What truth in an all-day sense could possibly mean is discussed virtually all the time throughout the history of philosophy, and I will skip this here.
The question what truth in mathematics could mean was one of the main subjects in the Foundational crisis in the early 20th century and is widly discussed ever since. The second (and highly related) question was (and is): what are the objects of mathematics? Back then there were mainly three points of view: The platonist, who thinks there are some kind of blueprints of mathematical objects and all one does, is discovering some truth (in a rather all day sense of truth) about their properties. The formalist, who does not think, mathematical objects exist at all, they are rather implicitly defined by some axioms and then truth is nothing else then consistency with these axioms. And last the intuitionist, who thinks mathematical objects are creatures of human mind. The starting point for the intuitionist is the ability to count, which amounts into the natural numbers.  Everey other object and every true statement then has to be constructed out of these first objects and some basic logic, wich does not include the law of excluded middle, i.e. no proof by contradiction. Astonishingly enough it is possible to reconstruct a quite rich part of mathematics even in a pure intuinitionist flavour.
Throughout the 20th century there were a lot of mathematical and philosohical writings around these question (see Hilbert, Brower, Whitehead, Putnam, Günther, Turing, Gödel and many others). Luckily this philosophical uncertainity didn't keep mathematicians from doing mathematics. What I think is really interesting is the capability of switching between the different states: Attacking a problem requires often (at least in my field of interest which is differntial geometry) first to get a good intuition about the objects (this is the platonist part), some strong constructive work inside the mind (this is the intuitionist part) and finally putting everything down into a rigorous proof (that is the formalist part). And most often this is not a linear process, rather a continous going forth and back... 
As Reuben Hersh put it: "“The working mathematician is a Platonist on weekdays, a formalist on weekends. On weekdays, when doing mathematics, he’s a Platonist, convinced he’s dealing with an objective reality whose properties he’s trying to determine. On weekends, if challenged to give a philosophical account of this reality, it’s easiest to pretend he doesn’t believe in it. He plays formalist, and pretends mathematics is a meaningless game.... Does it matter? Yes. Truth and meaning aren’t recondite technical terms. They concern anyone who use or teaches mathematics."
If by chance you understand german: There is a really nice book of a sociologist, who did some research on how the mathematical community works and what are the main characteristics of mathematics compared to other scientific fields. It gives a good bases on some philosophical background and quiet interesting insights into the mechanics of mathematical research. Bettina Heintz: Die Innenwelt der Mathematik.
Another good question enters the game: What is the connection between mathematics and "reality"? More precicly: How does mathematics and it's applications to science, social science, engineering and so forth interact? If mathematics was just a technical game, or some construct in human mind, how is it possible, that it has such a rich field of applications? On the other hand: Do all this applications imply, that mathematical objects really live in the physical world, and if so, what does this imply for beeing able to make true statement? See for example papers of Putnam, which include deep thoughts in this direction.
Not much of an answer, more of a loos collection of some thought. Hope it gives some input though!
A: I like to think that mathematical truth is a mathematical model of "real world truth", similar in my mind to the way in which the mathematical real number line $\mathbb{R}$ is a mathematical model of a "real world line", and similarly for many other mathematical models. 
In order to achieve the level of rigor needed to do mathematics, sometimes the description of the mathematical model has formal details that perhaps do not reflect anything in particular that one sees in the real world. Oh well! That's just the way things go. 
So yes, the empty function is injective. It's a formal consequence of how we axiomatize mathematical truth.
And, by the way, yes, there are infinitely many primes. The classical proof by contradiction that you feel is a natural language proof and not really a "formal proof" is actually not very hard to formalize at all. Part of the training of a mathematician is (a) to use our natural intuition, experience, or whatever, in order to come up with natural language proofs and then (b) to turn those natural language proofs into formal proofs.
A: Lee Mosher has already given an excellent general answer, and user21820 has given a nice explanation of vacuous truth. I'd like to expand on their answers by describing how I think about empty functions, which I find just as concrete and intuitive as other functions.

Like many people, I like to think of a set as a type of stuff.^ For example, there's


*

*a set $\mathbf{Fruit}$ which every fruit qualifies as an element of,

*a set $\mathbf{Papayas}$ which every papaya qualifies as an element of,

*a set $\mathbf{Mammals}$ which every mammal qualifies as an element of,

*a set $\mathbf{OwlPellets}$ which every owl pellet qualifies as an element of,

*a set $\{\text{Vectornaut}\}$ which only I qualify as an element of, and

*a set $\varnothing$ so exclusive that nothing qualifies as an element of it.


Observe that $\mathbf{Papayas} \subset \mathbf{Fruit}$, because every papaya is a fruit. Similarly, $\{\text{Vectornaut}\} \subset \mathbf{Mammals}$, because I, the only thing that qualifies as a $\{\text{Vectornaut}\}$, happen to be a mammal.
A function $A \to B$ is like a vending machine: if you drop an $A$ into the slot, the machine will spit out a $B$ for you to enjoy. If you drop in something that's not an $A$, the machine will reject it, because it only accepts $A$s. If you drop a banana into a $\mathbf{Fruit} \to \mathbf{Papayas}$ vending machine, for example, the machine will spit out a papaya. (This is a useful vending machine if you like papayas more than any other fruit.) If you drop a mouse into a $\mathbf{Fruit} \to \mathbf{Papayas}$ vending machine, the mouse will just roll out the coin return, because it's not a fruit. If you drop a mouse into a $\mathbf{Mammals} \to \mathbf{OwlPellets}$ vending machine, on the other hand, the machine will rattle around for a bit and then spit out an owl pellet. (I think I can guess what's hiding in there.)
A $\varnothing \to \mathbf{Fruit}$ vending machine is so selective that it won't accept anything as payment. You can dump in dolphins or owl pellets or gold dubloons, but it all just rolls out the coin return, and you never get any fruit. This is a stupid kind of vending machine, but it's useful to be able to talk about, because vending machines like this really exist—in everyday language, we call them “out of order.”
It's impossible for a $\mathbf{Fruit} \to \varnothing$ vending machine to exist. The reason is that some things really do qualify as fruit—I have one right here on my kitchen counter—and if you dropped one of those things into a $\mathbf{Fruit} \to \varnothing$ vending machine, the machine would have to spit out something that qualifies as a $\varnothing$. Since nothing qualifies as a $\varnothing$, the machine can't function as adversised.
On the other hand, it is possible for a $\varnothing \to \varnothing$ vending machine to exist. Although there's nothing the machine could give you in return for a payment, there's also nothing it will accept as a payment, so it will never fail to work as advertised.

^ The rules of set theory are designed to capture this intuitive picture.
A: The answer is both, due to the quirks of formal language.  Truth is both a label assigned to expressions and also a specific concept related to your intuition.  The reason for this dichotomy is most apparent in the work of Alfred Tarksi and his undefinability theorem.
Tarski's theorem tugs at the corners of the fabric of mathematics.  He showed that, for any theory strong enough to prove all truths in arithmetic (i.e. 1+1=2, 3*5=15, and so on) and had negation, it could not define its own semantics.  The specific statement he proved was that it could not define a function True such that True(encode(s)), where encode(s) was an encoded expression in that language gave the truth value for s.  He used a really twisted little trick known as the diagonalization lemma to basically wedge the system against itself and prove that there must be a case where the True function breaks down.
In many cases, we are not considering such powerful self referential systems.  Usually we're using a powerful system to prove something smaller and specific.  For example, we may use first order logic and ZF set theory to prove a statement about the cardinality of large sets.  In this sense, we are using the idea of "truth" as a label that can be applied within that system.
However, when we start exploring deeper "truths" which start to stretch the limit of our proof system, we start to find that the simple concept of "truth as a label" ceases to be as useful as it was in the simpler cases.  We start relying more on the semantic meaning of "truth" rather than the syntactic one.  Thanks to Tarski's work, we can prove that that semantic meaning must come from elsewhere.  It must have a deeper meaning.
This eventually does push its way into the philosophy of mathematics, where we have to define what mathematics calls "truth."  At this point, we can define "truth" any way we want, it's just a word, but there is an intuitive benefit for "truth" to have a meaning closely related to the intuitive concepts we all use.
A case study in the differences here is the difference between ZF and ZFC axioms for set theory.  The axiom of choice is a remarkably intuitive axiom, but it has profoundly non-intuitive effects.  In ZFC, it is possible to take a sphere, cut it into a finite number of pieces, rotate and translate those pieces, and reassemble them into two perfect spheres, each with the same volume as the original.  These new spheres are not swiss cheese: they are a dense sphere, just like the original one.
In ZFC, the expressions used to describe this slice and dice operaton are deemed "true," because their syntactic description is formed from a series of valid inferences in first order logic with ZFC.  However, the idea that I can double my volume of spheres without decreasing their density in any way runs so afoul of our intuitive sense of "truth" that many mathematicians refuse to accept proofs done in ZFC.
A: To address your two specific questions:


*

*This is true because we can demonstrate it via a proof about natural numbers. It is rather specific, since it applied to a class of very concrete objects (one could say the most concrete objects in math: "God gave us the integers, all else is the work of man." Specifically, the natural numbers probably have the most right to being "out there" in a platonic sense - we can directly observe natural numbers in the world in terms of collections of objects. Only classical geometry comes to mind as more tied to observables.

*This question is much more "formal", since it is about matching an object to a definition. The object $f:\emptyset \to \mathbb{R}$, is both rigorously defined and yet vague as well (what does this function look like, how would I calculate it on a computer?). It is true in the sense that it satisfies the "check boxes" that define an injective function - $f$ need to correspond to anything observable or any of our everyday notions.


In general, formal methods, in fact, most "abstractions", are not inherently about anything. They consist in definitions and their verification. The extent to which they are about things beyond their own definitions is a philosophical/empirical matter. It is up to us to determine whether or not our notions concord with some formal system. If they do, then we can take advantage of the massive, extended analogical thinking that abstract/formal systems allow.
A: Here is a natural language statement you can use to verify that the empty set is injective:

If more than one wireless device is transmitting on the same frequency, then they will interfere with each other.

Or, in other words, given $f:device\mapsto frequency$, if $f$ is not injective then you will get interference.
Naturally, when there are no devices transmitting on any frequency ($device = \emptyset$), none of them will be interfering with any of the others, and thus our empty function must be injective.
Going back to your example of "all cellphones in the room are turned off", this is just an example of implied context, since that statement wouldn't normally serve any purpose if there weren't any cellphones. However, if you add explicit context to it, like "all cellphones must be off or on airplane mode before takeoff", it should be clear that if there are no cell phones, the requirement is satisfied.
This is the reason that many mathematically-true things seem like they don't make sense in the real world: they are victims of implied context. In fact, a lot of what mathematics is for is getting rid of these implied contexts.
A: Your main issue here seems to be that you are wondering how all the following statements:

If the Earth is flat, then the Earth exists.
If the Earth is flat, then the Earth does not exist.
If there is life on Europa, then the Earth exists.

could possibly be meaningfully assigned the same truth value in the real world. These are called vacuous truths, the first two because the falsity of the condition means that the consequent is irrelevant, and the third because the truth of the consequent means that the condition is irrelevant. One could interpret logic as a game of some sort, where the prover tries to convince the refuter of his claim. If the prover makes a claim of the form:

If A then B.

then the refuter must try to refute it. How? She must convince the prover that A is true but yet B is false. Back to our vacuous examples, the refuter must convince the prover that the Earth is flat. Nah... That's not going to happen, which is why the refuter can't refute the prover. In the third case, the refuter must convince the prover that the Earth doesn't exist. Again, no way...
On the other hand, the prover can prove the first two claims by showing that the Earth is not flat! (Come, follow me around the globe in eighty hours.) After doing this he can convince the refuter that he can always keep his promise because it can't be broken; the Earth is not flat, so the condition of his promise will never come to pass. The consequent part of his promise is irrelevant. In the third case, the condition part is immaterial because the prover can convince the refuter that no matter whether she can show that there is life on Europa, he can convince her that the Earth exists.
This is exactly the same as when you talk about an empty function being injective:

Any function with empty domain is injective.

which expands to:
$\def\none{\varnothing}$

Given any function $f$ such that $Dom(f) = \none$, and any $a,b \in Dom(f)$, if $f(a) = f(b)$ then $a = b$.

Well, what does the prover have to do to convince the refuter? He says, give me any function $f$ such that $Dom(f) = \none$, and give me any $a,b \in Dom(f)$! The refuter simply can't! There isn't any object in $Dom(f)$!
But wait, you say, how about the also true statement:

Any function with singleton domain is injective.

which expands to:

Given any function $f$ such that $Dom(f) = \{x\}$ for some $x$, and any $a,b \in Dom(f)$, if $f(a) = f(b)$ then $a = b$.

This time the refuter can continue the game. She gives the prover a function $f$ and provides an $x$ such that $Dom(f) = \{x\}$, and also gives him $a,b \in Dom(f)$. But then the prover now tells her: See? You assured me that every object in $Dom(f)$ is equal to $x$, so you've to accept that $a = x$ and $b = x$, and hence by meaning of equality $a = b$. Now I can convince you that if $f(a) = f(b)$ then $a = b$. (This is exactly the third kind of vacuous statement that we discussed at the beginning.) Indeed, haven't I already convinced you that $a = b$, so you don't need to even bother to show me that $f(a) = f(b)$?
A: Disclaimer: I am a formalist.
In my opinion, the right lesson is to question the everyday, intuitive notion of truth — i.e. I boldly assert that the everyday, intuitive notion of truth is also just a means of assigning a value to informal statements.
We like to think there is some deeper meaning to it, and there might even be such, but in practice, a "truth" is simply a label we put to statements that we arrive at in some sort of 'acceptable' manner, such as


*

*the result of a sufficiently plausible argument with accepted hypotheses

*the result of a scientific study

*the result of our brain processing external stimuli


or even things like


*

*deciding we are unwilling/unable to contemplate the negation

*wishful thinking


(of course, the latter two are rarely done consciously in those terms).
So the everyday, intuitive notion of truth really is similar to the formal mathematical notion of a truth valuation: it's just a means of assigning values to certain informal statements. And just as how mathematical truth valuations must respect (formal) logical deduction, we like the everyday, intuitive notion of truth to respect our various informal means of gaining knowledge.
A: As pointed out in some of the other answers, your question can be reformulated more concretely in terms of the natural numbers: Does $\mathbb{N}$ correspond to the ordinary (or what you call intuitive) counting numbers? The answer is that it depends on whether you accept the Intended Interpretation hypothesis, as many mathematicians do.  There is a detailed discussion of this issue here.
