Logic

Is it possible to prove that something cannot be derived (considering only well-formed-formulas) in a natural derivation system? I mean a premise P cannot yield the conclusion Q since there isn't any logical rule that justifies the inference but how can someone prove this?

Comments

One way to show this would be (1) to prove that the derivation system is sound (that is, if Q can be derived from P in the system, then the inference from P to Q is a valid one); and (2) to show that the inference from P to Q is not valid.

We can also sometimes prove non-derivability results by purely "combinatorial" arguments. Here's a well-known toy example, due to Douglas Hofstadter.

Consider a derivation system which uses just the symbols M, I, and U which can be combined to produce strings of symbols in any way you like, e.g. MI, UMIIM, IUUUUU, etc.

The rules of our system are as follows:

If a string ends in I, you can add a U to the end. For example, from MII you can "infer" MIIU.
If a string starts M, you can "double" the rest of the string (i.e. change Mx, to Mxx). For example, from MIUI you can infer MIUIIUI.
You can replace any occurrence of III with a U. For example, from MUIIIU you can infer MUUU.
You can delete any occurrence of UU. For example: from MIUUUM you can infer MIUM.

Question: Can you start with MI as an "axiom" and derive MU, using the rules 1 to 4?

Answer: You can't. I'll leave you to work out why that is so (or to Google the proof!). But here's a hint and a comment. The hint is: think about the possible numbers of 'I's that can occur in any string got by starting from MI and applying the rules. And the comment is that this proof of non-derivability doesn't depend on questions of interpretation or meaning (unlike a non-derivability proof relying on an idea like the soundness of the system relative to some intended interpretation).

Read another response by Alexander George, Peter Smith

Read another response about Logic