0

The exercise 3.4.4 of Mathematical Logic by Hodges and Chiswell is like that:
"Let $\rho$ and $\sigma$ be signatures with $\rho \subseteq \sigma$
(a) Suppose $D$ is a $\sigma$-derivation, and $D'$ is got from $D$ by writing $\perp$ em place of each symbol in $D$ that is in $\sigma$ but not in $\rho$. Show that $D'$ is a $\rho$-derivation.
(b) Suppose $\Gamma$ is a set of formula de $LP(\rho)$ and $\psi$ is a formula of $LP(\rho)$, such that the sequent $(\Gamma \vdash_\sigma \psi)$ is correct. Show that the sequent $(\Gamma \vdash_\rho \psi)$ is correct."
The solution of part (a) is presented and the solution of part (b) is an application of part (a).
My problem is that I can't imagine in propositional logic an example where this exercise is applicable.
Some help?
Thanks.

lcmpereira
  • 103
  • Induction on the derivation-tree... Unfortunately, many cases to check: try with some significant one. The base case is straightforward: $\Gamma \vdash \varphi$ with only the Assumption rule applied: thus $\varphi \in \Gamma$ and thus $\Gamma [\bot/p] \vdash \varphi [\bot/p]$ – Mauro ALLEGRANZA Jan 31 '22 at 14:47
  • Then try some cases for Induction step: $(\lnot \text I)$ and $(\land \text I)$. – Mauro ALLEGRANZA Jan 31 '22 at 15:10
  • I would like to know if there is only one case where a symbol doesn’t appear in conclusion and undischarged assumptions and appears in the middle of derivation. – lcmpereira Jan 31 '22 at 15:44
  • We have the so-called SUBFORMULA PROPERTY... but it is a "advanced" issue and I'm quite sure that at that point of the book there is no need to consider it for the above exercise. – Mauro ALLEGRANZA Jan 31 '22 at 15:48
  • Maybe the intuition can help... why the above substitution does not cause troubles? Consider the simple derivation without assumption $\vdash \varphi$. By soundness, we know that $\varphi$ is a tautology; thus, it is always TRUE for every assignment of truth values to the prop symbols. If we replace one of them, say $p$, with $\bot$ we do not "produce" a new case in the corresponding truth table, because this case was already present when $p$ was assigned FALSE. This amounts to (prove by Induction) that if $\vDash \varphi$, then $\vDash \varphi [\bot/p]$. – Mauro ALLEGRANZA Jan 31 '22 at 15:51
  • In propositional logic. – lcmpereira Jan 31 '22 at 15:52
  • But then, by Completeness: $\vdash \varphi [\bot/p]$. This "semi-formal" argument can be reframed without Soundness-Completeness but still using Induction. – Mauro ALLEGRANZA Jan 31 '22 at 15:53
  • Thanks, Mauro. But I am not worried about the solution of the problem. The solution of part (a) is presented in the book, and the solution of part (b) is an application of part (a). I wanted a concrete example of these conditions in propositional logic without excessive use of RAA. – lcmpereira Jan 31 '22 at 15:59
  • An example of that kind of derivation? $p[\bot/p] \vdash (p \lor q)[\bot/p]$ – Mauro ALLEGRANZA Feb 01 '22 at 06:56
  • I will give you an useless example, but I can't write here. I will answer my own question. – lcmpereira Feb 01 '22 at 11:40
  • But I think this is the issue. Extra symbols cannot play an important role, otherwise it would not be possible to replace them with $\perp$. – lcmpereira Feb 01 '22 at 13:52

1 Answers1

0

Consider the following derivation:

$ \dfrac{ \dfrac{ \dfrac{\dfrac{p \quad [\neg p]}{\perp}}{q} \quad \dfrac{\dfrac{p \quad [\neg p]}{\perp}}{\neg q} } {\perp} } {p} $

This proves the sequent $\{p\} \vdash p$. The derivation uses $q$ and this symbol doesn't appear in the conclusion or in the undischarged assumption.

Replacing $q$ by $\perp$:

$ \dfrac{ \dfrac{ \dfrac{\dfrac{p \quad [\neg p]}{\perp}}{\perp} \quad \dfrac{\dfrac{p \quad [\neg p]}{\perp}}{\neg \perp} } {\perp} } {p} $

But it is an useless example. I would like to know if there is a more useful derivation with these conditions.

lcmpereira
  • 103
  • You have to replace a prop symbol with $\bot$... Thus, assume that $\phi$ is $p$ and replace it with $\bot$. Can you check the new derivation? – Mauro ALLEGRANZA Feb 01 '22 at 13:54
  • But you can also assume that $\psi$ is $q$ and replace it with 4\bit$. Check it again... – Mauro ALLEGRANZA Feb 01 '22 at 13:55
  • The gist is... not so much the result, but the proof technique: induction on the derivation tree. – Mauro ALLEGRANZA Feb 01 '22 at 13:55
  • Regarding the exercise, I think I have to replace $\psi$ with $\perp$. – lcmpereira Feb 01 '22 at 14:36
  • Yes... the text says: "writing $\bot$ in place of each symbol in D that is in σ but not in ρ.." So we have to use symbols: $p,q,\ldots$ and not schematic (meta-)variables. So my example is: assume you have used $q$ (which is in $\sigma$ but not in signature $\rho$) and replace it with $\bot$. The result is in "rho-language" and - the theorem says - is still a good derivation. – Mauro ALLEGRANZA Feb 01 '22 at 14:41
  • Yes, I used metavariables like symbols of the signatures. Thank you. – lcmpereira Feb 01 '22 at 14:47
  • Answer edited. Thank you. – lcmpereira Feb 07 '22 at 12:46