0
$\begingroup$

This is a problem from A Friendly Introduction to Mathematical Logic by Christopher Leary and Lars Kristiansen which is in Page number 65.


Here's my attempt:

Consider a structure $\mathfrak{U}$ and suppose that its universe is $A=\{ 1,2 \}$. Consider $\Sigma$ be the singleton consisting of the formula $\exists x(x=y)$. Then $\Sigma \vdash \exists x(x=y)$ and suppose that we had $\Sigma \vdash x=y$. Then by Soundness Theorem, $\Sigma\models x=y$.

Consider the variable assignment function $s$ into $\mathfrak{U}$ which sends $x$ to $1$ and $y$ to $2$. Then clearly, $\mathfrak{U}$ satisfies $\exists x (x=y)$ with the assignment $s$ as $\mathfrak{U}$ satisfies $x=y$ with the substituition $s[x|2]$. But on the other hand, $\mathfrak{U}$ does not satisfy $x=y$ with the substituition $s$. This would contradict that $\Sigma\models x=y$. Hence, it cannot be that $\Sigma \vdash x=y$.


Is this counterexample correct? Is there a way to do without appealing to the Soundness Theorem?

$\endgroup$
2
$\begingroup$

Yes, your counterexample works.

As to avoiding soundness: it's difficult, although of course not impossible, to avoid the soundness theorem when proving non-instances of $\vdash$. This is because the definition of $\vdash$ is a "positive inductive" one - it's set up to be very easy to prove instances of $\vdash$, but that has a cost. To see the issue, think about proving $\top\not\vdash\perp$; although blindingly obvious, this isn't actually easy (depending on what definition of "$\vdash$" you're using anyways).

Broadly speaking, in order to prove $\Phi\not\vdash\psi$ you need to produce a set of formulas $\Theta$ which is closed under $\vdash$, contains $\Phi$, and does not contain $\psi$ (and verify that of course). The soundness theorem is really just a way of repackaging this task: every structure $\mathfrak{M}$ has its associated theory $Th(\mathfrak{M})$, which is closed under $\vdash$ by soundness, and so we can think about structures instead of theories. However, we can totally "cut out the middleman:" you can produce an entirely syntactic description of $Th(\mathfrak{A})$, and prove the relevant properties of this, without ever actually referring to structures.

And this is in fact a worthwhile problem to tackle:

Can you give a "structure-free" description of $Th(\mathfrak{A})$?

Even the case of quantifier-free formulas is instructive here. (HINT: think about ways of splitting the set of free variables into two possibly empty pieces.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.