Tell me more ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.
up vote 1 down vote favorite

I have an exam in the course about higher order logic. I was looking for answer of the question "Explain the advantage and disadvantage of using Hilbert system". The disadvantage in the meaning of why it is hard to apply. Thanks.

share|improve this question
Is this a take-home exam you haven't turned in yet? – Qiaochu Yuan Aug 23 '12 at 21:54
2  
Nope, this is not take home exam. I have to attend the exam next week. I am preparing for the exam and looking for some explanation about it. In my lecture sheet, it says hilbert system is easy to understand and hard to use. But why? I am looking for that thing. – sparrow Aug 23 '12 at 22:26
1  
I think there are nicer ways to welcome a new user who has an exam in a week than savagely downvoting him (-3 at the time I read the question but I have upvoted). I would have liked to help but I am unfortunately incompetent: could someone more erudite please help our new friend? – Georges Elencwajg Aug 23 '12 at 22:34
2  
@GeorgesElencwajg That is so kind of you. I was also amazed and thought I may be asked some very stupid question :) – sparrow Aug 23 '12 at 22:54
1  
@KaratugOzanBircan I already read that wiki article and I also learned to use Hilbert proof system. But still I dont have the proficiency to explain its why/where its good or bad or comparing it with some other proof system like natural deduction :) Thanks for your help btw. – sparrow Aug 23 '12 at 22:57
show 1 more comment

1 Answer

up vote 5 down vote accepted

From a practical point of view, the disadvantages of a Hilbert System are

  • It is very cumbersome to use directly for deriving some formula.
  • You need to prove at least some metatheorems before you can use such a system without too much overhead.
  • It doesn't mirror the natural way to do deduction, which can work by proving subtheorems relying on additional assumption, or by doing case-by-case analysis, or by using proof by contradiction.
  • It needs many axioms and axiom schema's to work.

From a theoretical point of view, the advantages of a Hilbert System are

  • It works.
  • It is conceptually very simple.
  • It has very few deduction rules, often only "modus ponens" and "generalization", which makes it easier to prove metatheorems, or to implement the scheme in a computer program (see metamath proof explorer for a practical example)
  • At least in theory, it should allow to explore the consequences of different axiom systems easily.

The relation between a Hilbert system and a natural deduction system is similar to the relation between machine language and a high level programming language. Of course you can build a high level programming language on top of machine language, and similarly you can prove metatheorems about Hilbert systems which allow you to use some of the more convenient proof techniques from natural deduction systems also with Hilbert systems.

share|improve this answer
2  
A sharper comparison would say that proofs in the Hilbert system are like programs in combinatory logic, while proofs in natural deduction are like programs in $\lambda$-calculus. – Zhen Lin Aug 24 '12 at 1:44
Thanks for your nice explanation. also for the natural deduction comparison :) – sparrow Aug 24 '12 at 10:42
@ZhenLin: that is true -- but I think that anyone who knows what combinatory logic is (and how it makes sense to compare it to the lambda calculus) wouldn't need this explanation in the first place. Unless, perhaps, he has never wondered why combinatory logic is called "logic". – Henning Makholm Aug 25 '12 at 12:41
1  
It should be noted at "easier to implement in a computer program" does not weigh as strongly in favor of Hilbert-style systems as it might seem. Pure Hilbert-style proofs can be extremely long, and implementing them on a real resource-constrained computer makes it necessary (unless one is interested in only toy examples) to optimize the implementation by treating some metatheorems such as the deduction theorem as primitives. And then we're effectively talking about natural deduction instead. – Henning Makholm Aug 25 '12 at 12:48

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.