3
$\begingroup$

This question may sound silly, but there is something about the semantics in first order languages which confuses me a bit.

Im using Ebbinghaus,Flum,Thomas:Einführung in die mathematische Logik, as well as Shoenfield:Mathematical Logic for reference

They define (I translated the :gdw to :iff):

$$\vDash \mathfrak{I}(x_1 \equiv x_2) \qquad \mathrm{:iff} \qquad \mathfrak{I}(x_1) = \mathfrak{I}(x_2)$$

and for Shoenfield, he uses no semantical symbol but introduces the term structure and then says for the formula $\mathbf{A} \ which \ denotes \ \mathbf{a} = \mathbf{b}$

$$\mathfrak{S}(\mathbf{A}) = \top \quad \mathrm{iff}\quad \mathfrak{S}(\mathbf{a}) =\mathfrak{S}(\mathbf{b})$$

Which seem very similar (presumably they are actually both describing satisfiability relation and/or validity relation), but for a few things.

my question: I understand how I can use "satisfiable under an interpretation" to eliminate junctors by using the truth function for those, however with these definitions (similar holds for a general relation) I still technically dont see how I would be able to formally be able to say that $a=b$. For while Ebbinghaus states a rule (which actually seems like an axiom to me) that reflexity of the equality can be infered without an antescenden, and Shoenfield has equality axioms, either are syntactical (right?) and thus unrelated to the evaluating the equality under an interpretation. What am I missing, or is it implied that the use of the interpretation is done informally (unless the meta language is formalized as well)?

I will bring an example similar to one Ebbinghaus brings to make it clearer:

Let $S = (+,\cdot,0,1)$ on$\mathbb{N}$ be a structure, and $\beta(v_n) = 2n$, then the formula $$v_2(v_1+v_2) \equiv v_4$$ under this interpretation would become $4 \cdot(2+4) = 8$ (note they use $\equiv$ before interpreting and $=$ after, so I presumed that the evaluation is actually done in the metalanguage, while the equality axiom is stated in the object language etc

$\endgroup$
2
  • $\begingroup$ Well i comment to ask you if i am right. Are you asking, in a first order theory with equality, if axioms for = have to be "specified" before and treating = like a binary symbol of predicate? $\endgroup$ Commented Nov 7 at 15:46
  • $\begingroup$ Have you never considered the possibility that Ebbinghaus is a bad learning resource? A good source would make it very clear what is a string and what is not. You must always remember that every piece of syntax in a formal system is just syntactic strings and has no meaning until you apply an interpretation to it. It's not really about stating in object language or meta language. You want to know whether the string "x = y" is true under an interpretation I. That is I("x = y"), which is defined as ( I("x") = I("y") ). That's all there is. $\endgroup$ Commented Nov 16 at 9:43

2 Answers 2

Reset to default
4
$\begingroup$

An axiom is either a formula of the language or a schema in the metalanguage. In the first case, the "assertion" of the axiom as an axiom is a metalinguistic act.

In general, inference rules are "prescriptions" in the metalanguage. Expressions starting with $\vdash$ and $\vDash$ are metalinguistic expressions, because they states properties of formulas of the language.

An interpretation is a domain with objects and operations on them, that in mathematics is usally called a structure.

A formula $a=b$ is satisfied in an interpretation $I$ iff the "objects" assigned by the interpretation to terms (names) $a$ and $b$ respectively are the same.

Trivial example: formula $1+1=2$ interpreted in the domain of natural numbers.

Variable assignment functions are needed in order to manage formulas in predicate logic. They are functions from terms to elements of the domain of the interpretation and thus $\beta(v)=1$ ia a metalinguistic expression.

As said by the previous answer, Ebbinghaus etc use the $\equiv$ symbol in the formal language of predicate calculus and use in the metalanguage the $=$ symbol to denote the equality between objects of the structure.

Thus, $I \vDash (t \equiv s)$ iff $I(t)=I(s)$.

$\endgroup$
4
$\begingroup$

Assuming you have a first order language $\mathcal{L}$ and a Theory $\mathcal{T}$, if you want a theory with the symbol =, you have to specify its axioms in the meta Language, if you want to encode the fact that = is an equivalence relation compatible with terms and formulas you can construct. You need the following Axioms \begin{aligned} &\text{(U1)} && \dfrac{}{x = x} \\[1em] &\text{(U2)} && \dfrac{x = y}{y = x} \\[1em] &\text{(U3)} && \dfrac{x = y \quad y = z}{x = z} \\[1em] &\text{(U4)} && \dfrac{x_1 = y_1, \dots, x_n = y_n}{t(x_1,\dots,x_n) = t(y_1,\dots,y_n)} \\[1em] &\text{(U5)} && \dfrac{x_1 = y_1, \dots, x_n = y_n \quad \varphi(x_1,\dots,x_n)} {\varphi(y_1,\dots,y_n)} \end{aligned} And with a lot of calculation you will have $$Γ ⊢φ \iff Γ \models φ,$$ where $Γ$ is a set of closed formulas. But if you throw in your language the symbol = without specifiyng, before, what rules do you need, then you cannot really do what is written above. After that, you can "really" interpret this symbol as the standard equality.

Summarizing, it is like have an equality without specifying axioms. We know that $x=x$ because we have an axiom for it...

$\endgroup$
2
  • $\begingroup$ I added an example in the original post, and am still confused as the statement under an interpretation seems to have been stated in the meta language, while the equality axiom is stated as a rule as your U1 just with $\equiv$ instead etc $\endgroup$ Commented Nov 7 at 16:28
  • $\begingroup$ Well it is really tricky. The concept is the diffenrence between the symbol of = and the concept of = when interpret. You can say when a=b in a particular structure, but to treat a=b in a theory and to really derive a=b from something formally you need axioms. The trick here is the diffenrence between Model of a theory and the theory itself. $\endgroup$ Commented Nov 7 at 16:41

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.