What are those "things that cannot be proved using only ordinary rules of inference"?

Question

The online edition of the book Introduction to Logic by Michael Genesereth and Eric Kao, has a detail that left me confused.

CHAPTER 4

[...]

4.2 Linear Proofs

[...]

The interesting thing about the Mendelson axiom schemas is that, together with Implication Elimination, they alone are sufficient to prove all logical consequences from any set of premises.

[...]

4.3 Structured Proofs

[...]

The main benefit of structured proofs is that they allow us to prove things that cannot be proved using only ordinary rules of inference.

[...]

My confused thinking:

• Mendelson proof system has no structured rule of inference, so it is for linear proofs,
• so by 1st quoted sentence it is an example of a system by which linear proofs can "prove all logical consequences from any set of premises",
• but then how come that according to the 2nd quoted sentence there are "things that cannot be proved using only ordinary rules of inference",
• where ordinary rules of inference suggest linear proofs since structured rules of inference are for structured proofs.

What are those "things that cannot be proved using only ordinary rules of inference"? Could you give examples?

Answer 1

I am not sure what the writer means by: "The main benefit of structured proofs is that they allow us to prove things that cannot be proved using only ordinary rules of inference."

His earlier remark: "The interesting thing about the Mendelson axiom schemas is that, together with Implication Elimination, they alone are sufficient to prove all logical consequences from any set of premises." is correct.

More technical (what is wrong with the statements) Skip this when you find the above enough .

It does look like the writer is mixing formulas and rules, he even goes so far as: "Rules with no premises are sometimes called axiom schemas. Axiom schemas are usually written without the horizontal line used in displaying ordinary rules of inference."

There are two problems with this statement:

1) Axiom schemes are 'recipes' for formulas (every formula that can be created by replacing the meta variables ϕ , ψ and χ by any well formed formula is an axiom. (see http://en.wikipedia.org/wiki/Hilbert_system )

You can always go from an implicational formula to an inference rule. (An implicational formula is a formula where the main connective is an implication)

But the converse (from inference rule to implicational formula) is not always a given (it just depends, if the deduction theorem is true in that logic , in most familiar (non-modal) logics it is, here it can get rather messy and complicated)

2) What are that "rules with no premises" ?? Inference rules (rules for short) always have premisses, inference rules allow you to go from one or more premisses to one conclusion, so that there is at least one premmisse is allready implied in the definition. (see http://en.wikipedia.org/wiki/Inference_rules )

It is true that there are different uses of premisses, (premmisses of an argument vs premmisses of an inference rule), but it is not clear what the writer means with premisses in " rules with no premisses".

Maybe he means that when you treat axiom schemes as rules only, then you cannot prove every theorem. (For example try to prove $ P \to P $, without any formula to start with, how can you start? where can you apply your inference rule to?)

Maybe that is what the writer means, but I am not sure about it, maybe best is to ask the writer / your lecturer about this. Let me know what they said, maybe I can learn from it as well.

Hope this helps.

Answer 2

If you have a recursively-defined sequence $f$, then it might not be able to prove a property for $f_n$ for all values of $n$.

More specifically, if $f$ is the Fibonacci sequence ($f_0=0$, $f_1=1$, $f_n=f_{n-1}+f_{n-2}$), then you cannot prove $$(\forall n)(f_{n+1} f_{n-1} - {f_n}^2 = (-1)^n)$$ using the rules of inference. You need something like mathematical induction.

Answer 3

Your confusion lies in the interpretation of sentenses.

The original text says:

" The main benefit of structured proofs is that they allow us to prove things that cannot be proved using only ordinary rules of inference. "

What author means is that since the structured proofs allows us to introduce assumptions, we can now get rid of those Mendelson's 3 axiom schema and using only ordinary rules of inference (i.e. Premises {A, A=>B} yields B)to proof things. Whereas with linear proof, only using rules of inference is hard to proof anything, thus we have to use Mendelson's 3 axiom.