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.

-
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. – moshfiqur Aug 23 '12 at 22:26
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
@GeorgesElencwajg That is so kind of you. I was also amazed and thought I may be asked some very stupid question :) – moshfiqur Aug 23 '12 at 22:54
@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. – moshfiqur Aug 23 '12 at 22:57

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.

-
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 :) – moshfiqur 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
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
@DougSpoonwood While trying to find the answer to a question I recently asked, I also stumbled upon a paper claiming condensed detachment would allow to do without axiom schemes. I didn't read it in detail. However, the two axioms you propose look like axiom schemes to me. The $p$, $q$ and $r$ in your axioms are intended to be substituted with arbitrary formulas, hence these are two axiom schemes, not two single axioms. But I would be happy if you can explain it to me so I see that I'm wrong. – Thomas Klimpel Jun 15 '13 at 16:55

You can make deductions blindly... at least in several cases of propositional calculi. That is, you can having no idea of what you want to prove in the first place. At least, once you know how to do so. Condensed detachment is such a method.

Every logician seems to say that the make the metatheory easier to do than natural deduction systems (I don't know what logicians say about Hilbert systems compare to semantic tableaux in this respect). I don't understand how this works or why it holds.

They usually rely on the rule of modus ponens, or a more general rule of detachment. There exist very, very few people who debate or will need convincing of these rules. Consequently, if the axioms get accepted, once you can figure out how to deduce things, you can start to deduce things.

With Hilbert systems you can investigate systems of logic where the deduction metatheorem does not hold. This has importance for certain classes of multi-valued logics, as well as investigation of subsystems of classical propositional logic. Perhaps a good example here comes as the equivalential calculus (the rule of detachment here goes Epq, p$\vdash$q. A usual demonstration of the deduction metatheorem relies on the law of simplification CqCpq. The formula EqEpq is simply not valid under {0, 1} semantics (let both p=0 and q=0). So, the deduction metatheorem fails for the equivalential calculus.