# Hilbert system A Hilbert system, also called Hilbert-style deductive system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well. Most variants of Hilbert systems take a characteristic approach to balancing a trade-off between logical axioms and rules of inference. Hilbert systems are characterised by preferring many axiom schemes to a small set of rules of inference. Systems of natural deduction take the opposite approach, including many deduction rules but very few or no axiom schemes. The most commonly studied Hilbert systems have either just one rule of inference, modus ponens for propositional logics, or two, generalisation along with MP in order to handle predicate logics. They also feature several infinite axiom schemes. Hilbert systems for propositional modal logics, sometimes called Hilbert-Lewis systems, are generally axiomatised with two additional rules, the *necessitation rule* and the *uniform substitution rule*. A characteristic feature of the many variants of Hilbert systems is that the context is not changed in any of their rules of inference, while both *natural deduction* and *sequent calculus* contain some context-changing rules. Thus, if one is interested only in the derivability of tautologies, no hypothetical judgments, then one can formalize the Hilbert system in such a way that its rules of inference contain only judgments of a rather simple form. The same cannot be done with the other two deductions systems - since context gets changed in some of their rules of inferences, they cannot be formalized so that hypothetical judgments could be avoided; not even if we want to use them just for proving derivability of tautologies. --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://mandober.gitbook.io/math-debrief/300-logic/terms/hilbert-system.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.