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 interpretationFor 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".