Is it 1+1 or “1+1” that is a formula of addition? To my intuition, it is the former, and the latter seems to be a name of the formula. The reason why I ask this question is that provided my intuition is correct, 1+1 is not equal to 2 by Leibniz’s law, because if we take P to be a predicate for “is a formula of addition,” P(2) is false while P(1+1) is true. I’m not trying to deny that they are somehow in equivalence relation, but questioning if Leibniz’s law is enough to capture the relation. I guess my intuition is wrong in the first place but I don’t get why it is.
1+1=2 is a formula (an expression of mathematical language that express a statement) and "1+1=2" is the way to refer to the expression: correct.
1+1 is a term, i.e. an expression that denotes a number.
Thus, it is not a formula.
The principle of the Indiscernibility of Identicals (the converse of the Identity of Indiscernibles) in its predicate logic formulation states :
x=y → ∀F(Fx ↔ Fy).
If we apply it to "objects", like numbers, we have to use the predicate variable F to express properties of numbers, like e.g. "to be Even".
In this case, what we get is correct :
1+1=2 → (Even(1+1) ↔ Even(2)).
But the same applies if we "move at the meta-", i.e. considering the mention context: "1+1" is a term and "2" is a term, while "1+1=2" is a formula.
My understanding of the use-mention distinction is that the former refers to a disposition (behavior) or proposition (meaning bearer) while the latter is merely a reference (syntactical expression such as a string). In this way, dispositions correspond to correspondent truths (combining two individual cookies in results in a state of affairs that a box has a pair of cookies), propositions correspond to coherent truths (1+1=2 -> 2=2 since it is an example of the axiom that any number is equal to itself), and the metalinguistic string "1+1=2" is just a label that works pragmatically and could be "one and one is two" or "eins und eins macht zwei" and so on. As far as formulas are concerned, I believe "1+1=2" would be a fact, not a formula since it is a literal or particular instance of the abstraction "a+a=b" which is universal in nature. Note, I've used the expression "1+1=2" because strictly speaking logical conjunctions aren't predicates, but require a relationship in this case essentially expressed by a copula which is a grammatical form in this expression which expresses identity, equivalence.
Brighter minds might have a better answer.