What is the advantage and disadvantage of Hilbert System? 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.
 A: 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: Some advantages:
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 they 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.
Some disadvantages:
The substitutions needed in formulas hardly seem clear at first to derive anything other than substitution instances of the formulas you already have.  In other words, figuring out how to deduce detached theorems don't seem clear at first.  Fortunately, condensed detachment as a method does have a way to help you see how to do such deductions.  But, how often is that taught?
They generally have only the rule of modus ponens, so you don't have all that many tools with which to derive things.
