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.
What is the advantage and disadvantage of Hilbert System?
-
2Nope, 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. – 2012-08-23
-
1I 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? – 2012-08-23
-
0http://en.wikipedia.org/wiki/Hilbert_system – 2012-08-23
-
2@GeorgesElencwajg That is so kind of you. I was also amazed and thought I may be asked some very stupid question :) – 2012-08-23
-
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. – 2012-08-23
2 Answers
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.
-
3A 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. – 2012-08-24
-
0Thanks for your nice explanation. also for the natural deduction comparison :) – 2012-08-24
-
0@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". – 2012-08-25
-
1It 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. – 2012-08-25
-
0There exist a few errors here. Hilbert systems can work, in the sense of having the ability to deduce theorems, with a single axiom and modus ponens. Examples of this include the postulate sets: {CCpqCCqrCpr}, {CCCqprCpr}, as well as the sole axiom sets usable for classical propositional logic, {CqCpq}, and {CpCNpq}. The last two have an infinity of theorems derivable with condensed detachment. You can theoretically just validate the rule of condensed detachment in the metatheory, and then use it without knowing what you will derive. Is that too much overhead for computers? – 2013-06-15
-
0Also, proof techniques from natural deduction systems aren't always available in Hilbert Systems, in the sense that conditional introduction isn't available, because the deduction metatheorem can not get shown in the metatheory. – 2013-06-15
-
1@DougSpoonwood While trying to find the answer to a question I recently asked, I also stumbled upon a paper claiming [condensed detachment](http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.ndjfl/1040149359) 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. – 2013-06-15
-
0@ThomasKlimpel Maybe you're right about them still qualifying as schemes, I'm really not so sure. That said, a scheme like Cpp is more general than a scheme like CCppCpp (only one can get derived from the other). Also, if they are axiom schemes, they still consist of *single* axiom schemes, where you can deduce things with just modus ponens. Additionally, condensed detachment as a method doesn't find arbitrary formulas in the sense that it works such that it finds the most general formulas possible. The substitutions, as far as I can tell, are only arbitrary in the names of the variables used. – 2013-06-15
-
0@ThomasKlimpel I guess if you want to say that an axiom schema stands for a countably infinite set of axiom, it still qualifies a single countably infinite set of axioms. You can work with a single countably infinite set of axioms in a Hilbert system. You don't need many of them. – 2013-06-15
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 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.
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.