Still not getting difference bettwen Implies and Entails and the role of "interpretation" Background
I am trying to understand the answers to the question Implies ($\Rightarrow$) vs. Entails ($\models$) vs. Provable ($\vdash$).
In his answer, ryang wrote:


*

*material conditional $\left(\to\right)$

*implication$\left(\Rightarrow\right):$$\quad\to$ is true (perhaps in
an axiom system) in the current interpretation

*logical implication / (semantic) logical entailment
$\left(\models\right):$$\quad\to$ is true regardless of interpretation

*derivability / syntactic entailment $\left(\vdash\right):$$\quad\to$
can be proven true regardless of interpretation

For example, these two claims are simultaneously plausible: \begin{align}&\forall x\;\; x=x &\Rightarrow &&\forall x\,\forall y\;\;\;  x^2 -y^2 = (x+y)(x-y),\\&\forall x\;\; x=x &\not\models &&\forall x\,\forall y\;\;\;  x^2 -y^2 = (x+y)(x-y) .\end{align}

He said that the example is mathematically true, hence the $⇒;$ however, that it is not true in every interpretation, hence the $\not\models$.
He also agreed that if a claim that uses $⊨$ is correct then the same claim using $⇒$ instead is also correct, and that I can use  $⊨$ (not only $⇒$) while using non-logical symbols like $+:$ for example, 1=1 ⇒ 0+0=0+0 and 1=1 ⊨ 0+0=0+0 are both correct.
I think I have a rough understanding what "interpretation" means. I understand that $⇒$ is a meta-proposition about a "$→$"-statement, basically saying "$(p(x)→q(x))$=True".
Questions
Is $⊭$ even more meta than $⇒?\,$
In the answers, what are

*

*the "context" (by Hibou57);

*the "in all states of the world" by Rahul Madhavan;

*the "in every structure" by Michael Hardy ?

I think, "context" means a set of sentences that we can infer from, so something like a set of axioms? While "in all states of the world" and "in every structure" mean "for all interpretations"?
Also, specifically: why is \begin{align}&\forall x\;\; x=x &\not\models &&\forall x\,\forall y\;\;\;  x^2 -y^2 = (x+y)(x-y)\quad?\end{align} ryang wrote:

², +, −, ()() are not logical operators; if I define $x^2:=x$ and $x+y:=x$ and $(x)(y):=x$ and $x-y:=y,$ then that ⊨ statement has a true antecedent and false consequent.

But I understand that whether a symbol is logical or non-logical depends on the definition of my formal language, so if I include "$+$" into the set of logical symbols and give it a fixed meaning (make it a constant), then I could use $⊨$ in the example. But ryang wrote:

+ is not a logical connective, and "regardless of interpretation" does not mean "in the absence of non-logical symbols".

What did I get wrong here?
Final Note
I feel like this might be more than one question, but since everything seems entangled and I lack too much understanding, I do not even know how to untangle this mess.

Edit: I just noticed, that a logical symbol seems to be something different than a constant, so I mixed those into one thing. I should have said (and did mean) "if I include "$+$" into the set of constant symbols".
 A: In standard approaches I'm familiar with, you cannot just insert an arbitrary symbol like "+" as a logical symbol. The set of logical symbols not subject to interpretation is fixed by the overall framework (e.g., in first-order logic). One of the main goals of mathematical logic is to study what happens when interpretations of symbols vary, so inserting additional symbols as logical symbols defeats that purpose. If you don't allow interpretations of symbols to vary, then you are just studying one particular structure rather than a whole family of structures. Then you aren't really doing logic at all - you are just studying that structure.
A: 
Is $⊭$ even more meta than $⇒?\,$

$\nvDash$ is "as meta as" $\vDash$ is; they are both concepts of the meta language (mathematical English) and $\implies$ belongs to the formal object lanugage (first-order logic).

I think, "context" means a set of sentences that we can infer from, so something like a set of axioms? While "in all states of the world" and "in every structure" mean "for all interpretations"?

Yes, your thinking is correct.

Also, specifically: why is $$∀x(x=x)⊭∀x∀y(x^2−y^2=(x+y)(x−y))\,?$$ ryang wrote:


², +, −, ()() are not logical operators; if I define $x^2:=x$ and $x+y:=x$ and $(x)(y):=x$ and $x-y:=y,$ then that ⊨ statement has a true antecedent and false consequent.


if I include "$+$" into the set of logical symbols and give it a fixed meaning (make it a constant), then I could use $⊨$ in the example

Sure, you could define a formal language like that, but then you would have a non-standard logic that is not what is commonly meant when talking about first-order logic and the symbol $⊨$. First-order languages are defined by differing sets of non-logical symbols, but the set of logical symbols is fixed. (Apart from different character choices to mean the same thing, e.g. some texts write $\sim$ while others write $\neg$ for negation, and different choices of functionally complete sets of operators, e.g. $\lor$ can be expressed in terms of $\neg$ and $\land$ and so is sometimes treated as syntactic sugar for the latter rather than an official member of the formal language, but this will have no influence on the meaning).
