4
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ But structured proofs are complex derivations "grouped into subproofs nested within outer superproofs", like natural deduction or Fitch-style proofs ? $\endgroup$ – Mauro ALLEGRANZA Mar 31 '14 at 10:14
  • $\begingroup$ I think that the refernce are to Ch.3.2 and 3.3 ... $\endgroup$ – Mauro ALLEGRANZA Mar 31 '14 at 10:16
  • $\begingroup$ I think that the statement extracted from 3.3 about Structured Proofs is a little bit misleading. With "structured proofs" you have a set of tools much more flexible, but if we consider "classical logic" the Natural Deduction set of rules (e.g.for proposiational logic) is sound and complete in respect to tautologies, exactly as Mendelson's 3-axioms/1-rule axiom system. So your perplexity is sound : in what sense structural method allows are to "prove more" ? I think not ... They allows us to prove "better" (i.e.faster, more easily, more intuitively), but thet cannot licence ... 1/2 $\endgroup$ – Mauro ALLEGRANZA Mar 31 '14 at 10:22
  • $\begingroup$ ... "more" than the logical consequences of the premises. 2/2 $\endgroup$ – Mauro ALLEGRANZA Mar 31 '14 at 10:23
  • $\begingroup$ See end Ch.3, with another "strange" statement: "A proof system is complete if and only if every logical conclusion is provable. Mendelson is sound and complete for all sentences that can be written in terms of $\lnot$ and $\rightarrow$. Fitch is sound and complete for the full language." But in M's system, $\lor$ and $\land$ are defined in term of $\lnot$ and $\rightarrow$ (in the "usual" truth-functional way), and M's system derives also all tautologies with $\lor$ (like : $p \lor q \rightarrow q \lor p$). Thus, my modest feeling is that the above textbook is not so reliable. $\endgroup$ – Mauro ALLEGRANZA Mar 31 '14 at 10:29
0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ See Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 42 : if you want to "formally" avoid axioms, you may "reformat" the three Mendelson's axioms as rules with no premises and all works (of course, with modus ponens). Negri & von Plato use as example exactly the derivation of $A \rightarrow A$ from Mendelson (A1) and (A2). $\endgroup$ – Mauro ALLEGRANZA Mar 31 '14 at 15:57
  • $\begingroup$ @MauroALLEGRANZA What are that " rules with no premises" , but then I noticed I even used it in my post without even commenting on it (will do that later), inference rules always have premisses ( see en.wikipedia.org/wiki/Inference_rules ) otherwise what can you interfere / conclude with them? not sure about your remark about Negri & von Plato do they use axioms (formulas) or inference rules? formula's are a bit stronger than inference rules. (will come back to this later, most be off) $\endgroup$ – Willemien Mar 31 '14 at 16:09
  • $\begingroup$ @Willemien: your second paragrph helps, the rest does not $\endgroup$ – user139472 Apr 1 '14 at 10:21
  • $\begingroup$ @nlognafan: I highly recommend you to register your account, and then follow the instructions here to reclaim ownership of the account that you used to ask this question. $\endgroup$ – Willie Wong Apr 1 '14 at 10:25
0
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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.

$\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.