Is formal truth in mathematical logic a generalization of everyday, intuitive truth?

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.

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)$?

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.