1

This is exercise 5 in Van Dalen's "Logic and Structure", and the question is to show:

$\Gamma \vdash \phi \implies \Gamma \cup \Delta \vdash \phi$

$\Gamma \vdash \phi ; \Delta, \phi \vdash \psi \implies \Gamma \cup\Delta\vdash\psi$

I have two questions:

  1. What is this asking...? Can someone help me understand exactly what's going on in the question here?

  2. There is a solution given by Dr. Kevin T. Kelly's Logic and Computation course, in which he writes the following here:

I have a few questions on how this is written. Firstly, what is the set $\text{der}$ exactly? This is not defined in Van Dalen. Secondly, what does he mean when he writes "clamp $\cal{D'}$ onto $\phi$ in $\cal{D}'$"? Is this like the standard clamp function in analysis?

Cheers

Mauro ALLEGRANZA
  • 94,169
Trace444
  • 15

1 Answers1

3

The two results above express the basic property of the derivability relation $\vdash$.

The symbol $\Gamma \vdash \phi$ means that there is a derivation $\mathcal D$ (in the Natural Deduction proof system) of conclusion $\phi$ from the set $\Gamma$ of assumptions (or premises).

In the linked comment, the existence of such a derivation is symbolized with: $\mathcal D \in \text {der}$.

Having said that, the first result says that: having a derivation $\mathcal D$ of formula $\phi$ from the set of assumptions $\Gamma$, we can add further assumption (the new set of formulas $\Delta$) and the derivation still holds.

This property is called Monotonicity of entailment.

The second result expresses the Transitivity of entailment.

About "to clamp"...?

The idea is simply this one: starting from derivation $\mathcal D$ of $\phi$ from $\Gamma$, add to the premises the new set $\Delta$ and copy-paste the derivation $\mathcal D'$ of $\psi$ from $\Delta$ and $\phi$ (that we have already as conclusion of $\mathcal D$).

The result is a new derivation $\mathcal D''$ of $\psi$ with the new set $\Gamma \cup \Delta$ of premises.

This property of the $\vdash$ relation formalizes the usual mathematical practice of proving some preliminary Lemma to be used in the proof of a main Theorem.

Mauro ALLEGRANZA
  • 94,169
  • That helps a lot. I will research this more. Can you address the concerns laid out in the image I have posted, regarding the clamping? – Trace444 Mar 03 '21 at 07:05
  • @Trace444 clamping here means just "attach it to the earlier derivation". A derivation is a sequence of statements, really, and we can concatenate one sequence to another. It's just a "slangy" expression by the one writing that solution. It's what Mauro calls the copy-pasting part. – Henno Brandsma Mar 03 '21 at 08:33
  • @Trace444 It should have said "just take the derivation $\mathcal{D}$ which ends in $\phi$ (its conclusion), then take the derivation $\mathcal{D}'$ which has $\phi$ as one of its hypotheses. We glue together $\mathcal{D}, \mathcal{D}'$ in that order, where we remove $\phi$ from the hypotheses of $\mathcal{D}'$, because it's not needed in the new combined derivation: where $\mathcal{D}'$ used the hypothesis $\phi$, the new one uses the conclusion $\phi$ from $\mathcal{D}$ instead, and this forms the glue between them, as it were. The result is a valid derivation with conclusion $\psi$. – Henno Brandsma Mar 03 '21 at 08:41
  • @Trace444 I think the previous is what "clamp" is meant to convey. – Henno Brandsma Mar 03 '21 at 08:43
  • @Trace444 Van Dalen also has a whole preceding discussion on how to represent derivations as labeled trees etc. It's like grafting a tree onto another one. The leaf $\phi$ in $\mathcal{D}$ is the "clamp" on which we fasten $\mathcal{D}'$. – Henno Brandsma Mar 03 '21 at 08:49
  • Thank you very much, @HennoBrandsma. This has helped a lot. – Trace444 Mar 03 '21 at 09:18