Talk:Hilbert system

Rewrite

This article reads like a cheatsheet for 3, which, I might add, is written in Hungarian. The article doesn't define any of its syntax nor explain much of anything else. I appreciate the translation work that Physis has done here, but it's so much more technical than similar articles that I think it needs a complete rewrite. Vagary 02:02, 4 February 2007 (UTC)

Is there an error?

I'm not sure I understand these entirely, but shouldn't the eight axiom be

• $\mathrm {UnivGen} \ ^{*}\left\{\left(x=y\right)\to \left(\phi [\square :=x]\to \phi [\square :=y]\right)\mid \mathrm {Sbst} \left(\phi ,\square ,x\right)\land \mathrm {Sbst} \left(\phi ,\square ,y\right)\right\}$

instead of

• $\mathrm {UnivGen} \ ^{*}\left\{\left(x=y\right)\to \left(\phi [\square :=x]\to \psi [\square :=y]\right)\mid \mathrm {Sbst} \left(\phi ,\square ,x\right)\land \mathrm {Sbst} \left(\phi ,\square ,y\right)\right\}$

? --SLi 21:52, 28 May 2007 (UTC)

• $\mathrm {UnivGen} \ ^{*}\left\{\left(t_{1}=t_{2}\right)\to \left(\phi [\square :=t_{1}]\to \phi [\square :=t_{2}]\right)\mid \mathrm {Sbst} \left(\phi ,\square ,t_{1}\right)\land \mathrm {Sbst} \left(\phi ,\square ,t_{2}\right)\right\}$

Thank You very much. Besides the corrected typo, I chose also a better notation: x,y for metavariables (on varables); $t_{1}$, $t_{2}$ for metavariables on terms.

Physis 10:55, 24 June 2007 (UTC)

Sorry for the other error. In fact, Axiom 8 can be weakened, while it was too strong in another aspect at the same time. It must be

$\mathrm {UnivGen} \ ^{*}\left\{\left(x_{1}=x_{2}\right)\to \left(\phi [y:=x_{1}]\to \phi [y:=x_{2}]\right)\mid \mathrm {Sbst} _{0}\left(\phi ,y,x_{1}\right)\land \mathrm {Sbst} _{0}\left(\phi ,y,x_{2}\right)\right\}$

where let denote $\mathrm {Sbst} _{0}\subseteq \mathbf {Form} \times \mathbf {Var} \times \mathbf {Var}$ a restriction of allowed substitution $\mathrm {Sbst}$ — the restriction says that the substituted term is a variable, not an arbitrary term: $\mathrm {Sbst} _{0}=\mathrm {Sbst} \!\downharpoonright _{\mathbf {Form} \times \mathbf {Var} \times \mathbf {Var} }$.

Physis 20:33, 28 June 2007 (UTC)

Too complicated. Kleene 1952: Development of a "formal system"

It is depressing to run into something as abstruse and inaccessible as this article. Here is the system as Hilbert and Kleene and Godel defined it, in more or less current symbolism. I'm sure what is in the article is well-done, but is there another way to present it? Here is Kleene's approach:

---

This form of number theory extends for all the real numbers: -∞, 0, +∞. Kleene 1952 starts at chapter IV A FORMAL SYSTEM then skips to Chapter VIII FORMAL NUMBER THEORY.

To develop this theory he immediately defines what he calls three "function symbols" + (plus), * (times), ' (successor). But the development is worth repeating to see what is going on. In summary:

Symbols:

His entire collection of symbols is Logical symbols: ⊃ (implies), & (and), V (or), ￢(not), ∀ (for all), ∃ (there exists). Predicate symbols: = (equals). Function symbols: + (plus), * (times), ' (successor). Individual symbols: 0 (zero). Variables: a, b, c, .... Parentheses: (, ).

Juxtaposition (concatenation):

Term: From these symbols and the notion of juxtaposition (concatenation) of these symbols he defines term.

Formula: From term he defines formula.

Scope of a variable, free variable: He develops the notions of "scope of a variable" and "free variable".

Substitution: Then he introduces the notion of substitution (everywhere there's an occurrence), also replacement (selectively for e.g. one occurrence but not all ... this is confusing).

Transformation rules: in particular the three deductive schema. In the following the symbol ⇒ is being used in place of a long line under the expression, and indicates "yields" in the tautological or derivational sense. The symbols A, B are formulas, A(x), A(t) indicate a formula with a free variable:

Rules of inference: Immediate consequence :

• 2. A, (A ⊃ B) ⇒ B [here A is the first premise and (A ⊃ B) is the second premise, and B is the conclusion
• 9. C ⊃ A(x )⇒ (C ⊃ ∀xA(x) )
• 12. ( A(x) ⊃ C) ⇒ (∃xA(x) ⊃ C)

Postulates: These transformation rules are three of 21 postulates that he divides into three categories:

• GROUP A1: Postulates for the propositional calculus (formulas with no free variables)

• 1a A ⊃ (B ⊃ A). [Hilbert's #1, introduction of an assumption]
• 1b (A ⊃ B) ⊃ ((A ⊃ (B ⊃ C)) ⊃ (A ⊃ C).
• 2. A, A ⊃ B ⇒ B [Modus ponens: which I've always written and worked with as (A & (A ⊃ B)) ⊃ B, cf Kleene 1952:88 ]
• 3. A ⊃ (B ⊃ A & B). [As ⊃ has seniority over &, this is A ⊃ ( (B) ⊃ (A & B) ) ]
• 4a. A & B ⊃ A. [ (A & B) ⊃ A ]
• 4b. A & B ⊃ B. [ (A & B) ⊃ B ]
• 5a. A ⊃ A V B. [ A ⊃ (A V B) ]
• 5b. B ⊃ A V B. [ B ⊃ (A V B) ]
• 6. (A ⊃ C) ⊃ ((B ⊃ C) ⊃ ((A V B) ⊃ C)).
• 7. (A ⊃ B) ⊃ ((A ⊃ ~B) ⊃ ~A). [here ~ instead of the bent bar only because it's easier for me to write]
• 8^o. ~~A ⊃ A. [^o indicates that this "~-elimination" is intuitionistically unacceptable]
• 8^I. ~A ⊃ (A ⊃ B). ["weak ~-elimination" acceptable to intuitionists]

• GROUP A2: (Additional) Postulates for the predicate calculus (incorporating formulas A(x) with a free variable x)

• 9. C ⊃ A(x) ⇒ C ⊃ ∀xA(x)
• 10. ∀xA(x) ⊃ A(t)
• 11. A(t) ⇒ ∃xA(x)
• 12. ( A(x) ⊃ C ) ⇒ ( ∃xA(x) ⊃ C )

• GROUP B: (Additional) Postulates for number theory

It is in the last group B that the predicate symbol " = " and the "function symbols" + and * appear. As these are axioms, they are worth repeating:

• 13. A(0) & ∀x(A(x)⊃A(x') ⊃ A(x). (axiom of induction, cf Peano axioms)
• 14. a'=b' ⊃ a=b. (Peano axiom)
• 15. ￢a' = 0. (Peano axiom)
• 16. a=b ⊃ (a=c ⊃ b=c). (Peano axiom)
• 17. a=b ⊃ a'=b' (Peano axiom)
• 18. a+0=a (additive identity defined)
• 19. a+b'=(a+b)' (addition function-symbol defined in a recursive sense, cf Kleene 1952:186)
• 20. a*0=0 (multiplicative identity defined, an axiom)
• 21. a*b'=a*b+a (multiplication function-symbol defined in a recursive sense, cf Kleene 1952:186)

Finally, he defines the notion of immediate consequence of the premise(s) by the rules.

In his Chapter V Formal Deduction Kleene introduces the metamathematical sign ⊦ ("yields", deducibility relation) as in, for example:

modus ponens: A, A ⊃ B ⊦ B

In the final chapter he introduces the INDUCTION RULE over formulas with variables i.e. A(x). From all of this he deduces (proves) the familiar "arithmetic laws", including "association", "distribution", and "commutation" for + and *, the notions of additive identity and multiplicative identity, and the notions of multiplicative and additive inverses, the order properties (<, ≤, >, ≥), other more unusual properties such as "connexity, irreflexiveness, asymmetry, inequalities under addition and multiplication), but in particular interest the existence and uniqueness of quotient and remainder.

From this follows the notion of formally provable and we have, in a nutshell the same development used by Kurt Gödel in his Incompleteness theorems (1931) (which is fact where Kleene's development stops until he introduces the notion of primitive recursive functions. wvbailey Wvbailey 16:03, 11 November 2007 (UTC)

---

The reference David Hilbert (1927) The Foundations of Mathematics is a famous exerpt from Sahotra Sarkar (ed.) 1996, The Emergence of Logical Empiricism: From 1920 to the Vienna Circle, Garland Publishing Inc. Wherein Hilbert lays out his formal axiomatic system. This can be found at

reference: http://www.marxists.org/reference/subject/philosophy/works/ge/hilbert.htm

Hilbert 1927:

Symbols of the system: { ⊃ , &, V, ~, ∀x, ∃x, =, (, ) }

I. Axioms of implication:

• 1. A ⊃(B ⊃ A) (introduction of an assumption)
• 2. (A ⊃(A ⊃ B)) ⊃ (A ⊃ B) (omission of an assumption)
• 3. (A ⊃(B ⊃ C)) ⊃ (B ⊃ (A ⊃ C)) (interchange of assumptions)
• 4. (B ⊃ C) ⊃ ((A ⊃ B) ⊃ (A ⊃ C)) (elimination of a propostion)

II. Axioms about & and V:

• 5. A & B ⊃ A
• 6. A & B ⊃ B
• 7. A ⊃(B ⊃ A & B)
• 8 A ⊃ A V B
• 9. B ⊃ A V B
• 10. ((A ⊃ C) & (B ⊃ C) ⊃ ((A V B) ⊃ C)

III. Axioms of negation:

• 11. ((A ⊃ B) & ~B) ⊃ ~A (principle of contradiction)
• 12. ~(~A) ⊃ A (principle of double negation)

IV. The logical e-axiom:

• 13. A(a) ⊃ A(e(A)), where e(A) is an object about which the proposition A(a) holds if it holds for any object at all (here ≡ is "logically equivalent" i.e. ←→ )

• 13.1 Definition: ∀(a)A(a) ≡ A(e(~A))
• 13.2 Definition: (∃a)A(a) ≡ A(e(A))

Axioms of equality:

• 14. a = a
• 15. (a = b) ⊃ (A(a) ⊃ A(b))

Axioms of number:

• 16. a' ≠ 0; ( ≠ for "not=")
• 17. ( A(0) & ∀(a)(A(a)⊃ A(a')) ) ⊃ A(b) (principle of mathematical induction)

He also cites the "explicit definitions", which introudce the notions of mathematics and have the character as axioms, as well as certain recursion axioms).

[etc.] Wvbailey 17:59, 15 November 2007 (UTC)

---

Availability of a forked, rewritten version

I tried to reply these concerns with writing a new approach to introduce the topic. I kept this on a subpage. I shall follow Carl's proposal and will not develop this subpage any more, but contribute to the article indirectly. If the subpage contains anything that can be usable in any way, please feel free to use it. Physis 16:18, 15 November 2007 (UTC)

Three approaches I found till now

Till now, I have found the following three approaches:

Relying on Extension by definition I

R1. $\alpha \to \left(\beta \to \alpha \right)$

R2. $\left(\alpha \to \beta \rightarrow \xi \right)\to \left(\left(\alpha \to \beta \right)\to \left(\alpha \to \xi \right)\right)$

R3. $\left(\lnot \alpha \to \lnot \beta \right)\to \left(\beta \to \alpha \right)$ (reductio ad absurdum)

R4. $\forall x\left(\alpha \right)\to \alpha [x:=t]$ where t may be substituted for x in $\alpha$

R5. $\forall x\left(\alpha \to \beta \right)\to \left(\forall x\left(\alpha \right)\to \forall x\left(\beta \right)\right)$

R6. $\alpha \to \forall x\left(\alpha \right)$ where x is not a free variable of $\alpha$.

R7. ${\mathfrak {x}}={\mathfrak {x}}$ for variable ${\mathfrak {x}}$ where the notation ${\mathfrak {x}}$ is not meant as a metavariable, but it is directly part of object language: any fixed variable selected from the object language. Thus, R7 need not be an axiom scheme: it can be a standalone axion instance of its own. Of course, we could use a x metavariable ranging over variables of the object language, but it can be proven that doing so would be superfluous.

R8. $\left(x=y\right)\to \left(\alpha [z:=x]\to \alpha [z:=y]\right)$

Relying on extension by definition II

D1. $\alpha \to \left(\beta \to \alpha \right)$

D2. $\left(\alpha \to \beta \rightarrow \xi \right)\to \left(\left(\alpha \to \beta \right)\to \left(\alpha \to \xi \right)\right)$

D3. $(\lnot \alpha \to \beta )\to (\lnot \alpha \to \lnot \beta )\to \alpha$, mentioning that instead of this (contraposition), also reductio ad absurdum can be used, as at the above approach (R3).

D4. $\forall x(\alpha )\to \alpha [x:=t]$

D5. $\forall x(\alpha \to \beta )\to \forall x(\alpha )\to \forall x(\beta )$

D6. $\alpha _{0}\to \forall x(\alpha _{0})$ where x is not a free variable in $\alpha _{0}$

D7. $t=t$ where t is a metavariable ranging over terms

D8. $(s_{1}=t_{1})\to \dots \to (s_{n}=t_{n})\to f(s_{1},\dots ,s_{n})=f(t_{1},\dots ,t_{n})$ where f is a metavariable ranging over function symbols, and $s_{1},\dots ,s_{n},t_{1},\dots ,t_{n}$ are metavariables ranging over terms.

D9. $(s_{1}=t_{1})\to \dots \to (s_{n}=t_{n})\to P(s_{1},\dots ,s_{n})\to P(t_{1},\dots ,t_{n})$ where P is a metavariable ranging over predicate symbols, and $s_{1},\dots ,s_{n},t_{1},\dots ,t_{n}$ are as above

Conservative extension

The approach I found is not a mere superset of any of the former approaches, because the most interesting axiom for universal quantifier differs: instead of

$\forall x(\alpha \to \beta )\to \forall x(\alpha )\to \forall x(\beta )$

it postulates

$\forall x(\alpha _{0}\to \beta )\to \alpha _{0}\to \forall x(\beta )$ where x is not a free variable in $\alpha _{0}$

In details:

C01. $\alpha \to \left(\beta \to \alpha \right)$

C02. $\left(\alpha \to \beta \rightarrow \xi \right)\to \left(\left(\alpha \to \beta \right)\to \left(\alpha \to \xi \right)\right)$

C03. $(\lnot \alpha \to \beta )\to (\lnot \alpha \to \lnot \beta )\to \alpha$

C04. $\lnot \lnot \alpha \to \alpha$. (In both "extension by definition" former approach, this was lacking.)

Conjunction and disjunction

C05. $\alpha \to \beta \to (\alpha \land \beta )$

C06. $\alpha \land \beta \to \alpha$

C07. $\alpha \land \beta \to \beta$

C08. $(\alpha _{1}\to \beta )\to (\alpha _{2}\to \beta )\to (\alpha _{1}\lor \alpha _{2})\to \beta$

C09. $\alpha \to \alpha \lor \beta$

C10. $\beta \to \alpha \lor \beta$

Universal

C11. $\forall x(\alpha _{0}\to \beta )\to \alpha _{0}\to \forall x(\beta )$ where x is not a free variable in $\alpha _{0}$

C12. $\forall x(\alpha )\to \alpha [x:=t]$ where x is a metavariable ranging over variables of the object language, t is also a metavariable ranging over terms of the object language

C13 $\alpha _{0}\to \forall x(\alpha _{0})$ where x is not a free variable in $\alpha _{0}$

Existential

C14. $\forall x(\alpha \to \beta _{0})\to \exists x(\alpha )\to \beta _{0}$ where x is not a free variable in $\beta _{0}$

C15. $\alpha [x:=t]\to \exists x(\alpha )$

C16. $\exists x(\alpha _{0})\to \alpha _{0}$ where x is not a free variable in $\alpha _{0}$. The reference does not use it, I put it here only becauase I think it fits here, forming a kind of dual pair with C13.

Identity

C17. $t=t$ where t is a metavarable ranging over terms

C18. $(s_{1}=t_{1})\to \dots \to (s_{n}=t_{n})\to f(s_{1},\dots ,s_{n})=f(t_{1},\dots ,t_{n})$ where f is a metavariable ranging over function symbols, and $s_{1},\dots ,s_{n},t_{1},\dots ,t_{n}$ are metavariables ranging over terms.

C19. $(s_{1}=t_{1})\to \dots \to (s_{n}=t_{n})\to P(s_{1},\dots ,s_{n})\to P(t_{1},\dots ,t_{n})$ where P is a metavariable ranging over predicate symbols, and $s_{1},\dots ,s_{n},t_{1},\dots ,t_{n}$ are as above

Questions

Unfortunatelly, I lack the knowledge and overview. which could be needed to write a good summary article. The most interesting thing for me in the differences and common parts in the above approaches:

• In the "conservative extension" approach, can reduction ad absurdum be postulated in a from, so that it resembes more to $\lnot$-introduction? (while double negation axiom would playing the role of $\lnot$-elimination.) Thus, instead of

$(\lnot \alpha \to \beta )\to (\lnot \alpha \to \lnot \beta )\to \alpha$

could we postulate

$(\alpha \to \beta )\to (\alpha \to \lnot \beta )\to \lnot \alpha$

because I think, so it would form a nice $\lnot$-introduction / $\lnot$-elimination pair with

$\lnot \lnot \alpha \to \alpha$

• Why is the most interesting axiom for universal quantifier in "conservative extension" treatment:

$\forall x(\alpha _{0}\to \beta )\to \alpha _{0}\to \forall x(\beta )$ where x is not a free variable in $\alpha _{0}$

different from the corresponding axiom in "extension by definition" treatment:

$\forall x(\alpha \to \beta )\to \forall x(\alpha )\to \forall x(\beta )$

Maybe these questions are not really important here, thus, if they are not really relevant for the article and the topic itself, please do not waste time for them.

Physis 13:56, 15 November 2007 (UTC)

Possible references

In a book by Stolyar,

Abram Aronovich Stolyar 1970 Introduction to Elementary Mathematical Logic, Dover Publications Inc, NY ISBN 0-486-64561-4,

I found a reference to Alonzo Church 1956 'Introduction to Mathematical Logic, I [?? sic], Princeton University Press, 1956, and also David Hilbert and William Ackermann, Principles of Mathematical Logic, Chelsea, New York, 1950 (translation of 1928 German edition.)

On p. 102 Stolyar writes that "In one of Hilbert's systems, one takes the symbols for disjunction and implication" to form an axiom system for the propositional calculus. On page 167 Stolyar introduces the four formulas of the predicate calculus that appear in Kleene 1952:82, i.e. the same four that appear in the section above, in "Group A2". Bill Wvbailey (talk) 19:01, 18 November 2007 (UTC)

Concept of “judgment” as a more characteristic difference among various deduction systems

Maybe I have made an error as I wrote in the lead that an essential feature Hilbert-style deduction system (distinguishing it from other ones) is the specific trade-off between logical axioms versus rules of inference. I should have grasped the essence better. What is the main motivation? What is the most essential feature that sort of "defines" what can be regarded as a [variant of the many] Hilbert style deduction systems?

Two things could be explained in lead:

1. The main motivation. I lack the knowledge to undertake it.
2. Motivations, trade-offs are things that we can move along a continuous scale. But there is also a very clear, sharp, not-blurrable border that separates the various deduction systems, manifesting itself even in use of metasigns. This clear distinguishing (maybe defining?) characteristic feature is the way they define (and exploit) the auxiliary concept of “judgment”.

In Sequent calculus article, I read an approach that grasps the differences among deduction systems in the way they define the auxiliary concept of "judgment". Hilbert-style (HS), natural deduction (ND) and sequent calculus (SC) seem fro me increasingly exploiting this concept:

• from coinciding with a standalone formula (HS),
• through asserting deduction explicitly from a given context (ND),
• to reaching a sophisticated form (SC).

A standalone article could be written for Judgment (mathematical logic), detailing the roles of "judgment" in each of all the three deduction systems, in a similar way as it is worked out in Sequent calculus article. I lack the necessary sincerity of knowledge, thus I only have only written a stub (and extended also Judgment (disambiguation) slightly).

As for the other characteristics of Hilbert-style deduction system (trade-off between logical axioms and rules of inference, metatheorems that are not explicitly declared as building blocks, but can be demonstrated): are they only secondary phenomena following from the way judgments are defined? Theoretically, the number of rules of inference (or logical axioms) can be augmented (with declaring both-side rules for conjunction, disjunction, both quantifiers), but the resulting system will still be not the same as natural deduction, because judgments will still coincide with standalone formula themselves, lacking the explicit mentioning of context. Thus, it seems to be for me an independent feature, a casual coincidence, not giving the defining essence of Hilbert-style deduction systems (albeit tradition may suggest so).

In summary: how do these many things join to each other, and which are primary factors, which are of secondary nature, which are independent?

• motivation
• metatheorems
• trade-off between logical axioms and rules of inference
• exploiting auxiliary concept of "judgment"

Physis (talk) 23:45, 2 January 2008 (UTC)

I have began some changes. The way I have rewritten the lead of Hilbert-style deduction system, and initiated Judgment (mathematical logic) itself, can have serious flaws, of couse it can be reverted or rewritten. But I hope this way the proposal can be judged better, because it can be seen explicitly what changes it suggests.

Physis (talk) 01:18, 3 January 2008 (UTC)

Could you give a reference for this? I don't think I've seen it in, for example, the Handbook of Proof Theory, but I might have missed it. The "party line" is that Hilbert-style systems trade fewer inference rules for more axiom schemes. — Carl (CBM · talk) 02:42, 3 January 2008 (UTC)

Thank You very much for the quick feedback. I admit I cannot provide a reference it yet (except for article Sequent calculus, of couse I know Wikipedia cannot not be referenced by Wikipedia). But I remember vaguely a book that discusses the topic in a similar way, unfortunately I had to return it to the library, I try to take it again tomorrow. I hope I can provide exact references and more details then. Best wishes, Physis (talk) 03:42, 3 January 2008 (UTC)

Everything has also an article about "judgment" in formal theories], I shall check its references tomorrow (e.g. Pfenning, Frank and Rowan Davies. A Judgmental Reconstruction of Modal Logic. In Mathematical Structures in Computer Science, 11(4):511--540, August 2001). I shall check tomorrow if I can avail this article or someting refered by it. Physis (talk) 04:00, 3 January 2008 (UTC)

Dear Carl,

I have taken the book, its approach (pp. 168, 185, 193) seems to fit here. I shall summarize it tomorrow (the book is Hungarian language).

I shall try to look for English sources on the weekend. Till now, I have found Pfenning, Frank (2004 Spring). "Natural Deduction". 15-815 Automated Theorem Proving. {{cite book}}: Check date values in: |year= (help); External link in |chapterurl= (help); Unknown parameter |chapterurl= ignored (|chapter-url= suggested) (help) As far as I can grasp it now, it supports exactly this approach, but shall have to read through it thoroughly yet. I shall check also Kneale & Kneale The Development of Logic, and Curry Combinatory Logic tomorrow.

Best wishes,

Physis (talk) 04:25, 4 January 2008 (UTC)

Thank you very much. I'll need some time to look through those before I can comment sensibly here. My main concern is first to understand what is being referred to as a judgement. A secondary concern is judging the correct amount of weight our articles should give to the concept. I'll be away for a few days, as well. — Carl (CBM · talk) 12:59, 4 January 2008 (UTC)

---

I don't know what is the best way to explain Hilbert-style logic, natural deduction and sequent calculus in the most intelligible way but the distinction between proofs as simple derivations of formulas and proofs as derivations of formulas relative to a given context is probably rather difficult to justify.

Hilbert-style logic is not strictly free of assumptions. Typically, how could we state the deduction theorem if derivations in Hilbert-style logic were not relative to a context of assumptions? Especially the rule (from paragraph Formal deductions) that states that φ holds if φ is an assumption of the context requires a notion of context.

I don't think that considering Hilbert-style logic as a logic that maximizes the ratio axioms/inference rules is a wrong view as Physis wonders at the beginning of the talk.

I'm not sure that there is a so clear and sharp border that separates the various deduction systems. For instance, even sequent calculus, in some recent formulations, has been formalized as a system for deriving formulas, leaving away the need for explicit sequents. In practice, all of the three kinds of systems can be presented as systems of sequents of the form $\Gamma \vdash A$, and all of the three kinds of systems can also be presented as systems for deriving formulas from an implicit context "hanging in the air". --Hugo Herbelin (talk) 20:55, 5 January 2008 (UTC)

---

Dear Hugo Herbelin,

The idea has was instilled into me originally by article Sequent calculus, but later

• Pfenning, Frank (2004 Spring). "Natural Deduction". 15-815 Automated Theorem Proving. {{cite book}}: Check date values in: |year= (help); External link in |chapterurl= (help); Unknown parameter |chapterurl= ignored (|chapter-url= suggested) (help)

seemed for me to reinforce it, and

• Martin-Löf, Per (1983). "On the meaning of the logical constants and the justifications of the logical laws". Siena Lectures.

suggested me that Judgment (mathematical logic) is not only something capable of helping in the classification of various deduction systems, but something important examining it on its own as well.

(The whole reference list is being collected on Judgment (mathematical logic)#External links.)

I admit I have not read them through yet, just judged by the intoductory parts of both. Please forgive me if I had misunderstood them in a serious way, in that case please help me show the main track these papers want to say.

Thank You very for Your these information. The last sentence You wrote was especially novelty to me.

• Is the "simpler direction" (formalizing HS with explicit mentioning of contexts) solved in the trivial way (using contexts in an idle way)?
• And how is the "more interesting" direction (formalizing ND or SC without explicit contexts) solved? (I think techniques like "dischargement of hypothesis" is a "cheating" in this question: something of "context-changing" nature is hiding behind it.) Can You help me to find some works about this, or summarize the main ideas?

Similarly, it was novelty to me that there are recent treatments of sequent calculus without referring to given context. Can You write some details (or sources) about it (or about the analogous achievement for natural deduction)? What I am interested in most: how are those rules of inferences conveyed, which are inherently of "context-changing" nature (most importantly, implication-introduction). Are these recent approaches You wrote about really a way which can be compared to the way HS acts? Does it not "cheatingly" "bring back" context-changing in a disguised form? For example, I think, the technique of "discharging hypotheses" in the proof tree is a "cheating" (from the point of vies of this this problem): HS does not even need referring to any dischargment.

As for summarizing my conjecture: I think HS is something that is free from any kind of "context-changing rules of inference (of course metatheroems about context or even context-changing can be posed "on top of it"), while ND is something that incorporates something context-changing in its very kernel: it has context-changing rules of inference, at least that of implication-introduction (it corresponds to deduction theorem in HS, but HS has DT not incorporated in its kernel, but built on top of it, "in the shell"). I suppose that's why ND relies so heavily on a more sophisticated form of concept "judgment", while for HS such a minimalistic jdugment concept suffices.

• Of course natural deduction can be formalized also without $\Gamma \vdash \phi$-like rules, e.g. using techniques like discharging hypotheses in a proof tree. But I think that is "cheating" (from the point of viw of this problem): dischargement is an open admitting that something of context-changing nature is taking place. That is why I am very interested in Your message: a non-cheating way of approaching natural deduction without any context-changing rules of inference.
• On the other side, of course HS can be formalized via contexts, but (at least in the trivial solution I can think of now), this contexts will be idle, conveying no context-changing. Please summarize the main idea if the solution You have thought of is not this trivial one.

Hilbert-style versus natural deduction

To express it in images:

In Hilbert-style deduction system,	For contrast, in natural deduction,
judgments are of minimalistic form	judgment is of a more sophisticated form, playing significant role in the machinery.
DT is not connected to the notion judgment	$\to \mathrm {I}$ (implication-introduction, the correspondent of DT in HS) relies directly on the notion of judgment
DT is on the shell, built on top of the machinery as a metatheorem.	$\to \mathrm {I}$ is in the very kernel, incorporated as rule of inference, not just dropped onto the top of the already-built machinery.

I did not understand Your second paragraph (debating the claim that HS is free of notion of context). Of cause HS is as powerful as ND or SC, thus, we can define concept of derivation, introduce turnstyle symbol in the metalanguage, we can say metatheroems using it, posing things about context, even about context-changing. Deduction theorem surely holds for HS, but I did not really understand why DT (expressed as metatheroem) would contradict the claim that HS uses a minimalistic form of judgment. In short: after we have already built the machinery of HS, we can define deduction via it, and on top of all this, we can say (and prove) metatheorems about context-changing (including DT). But HS does not incorporate DT as a rule of inference, thus, it does not have anything of "context-changing" nature its very kernel, thus, concept of "judgment" can be of minimalistic form. In short, HS has DT in the "shell", while ND has it in the "kernel".

I know there are principal questions I could not answer yet: for example, as Talk:Judgment (mathematical logic) shows, I know almost nothing about "ontology" of the notion of judgment. The references I can find are being collected on Judgment (mathematical logic)#External links.

Physis (talk) 04:50, 6 January 2008 (UTC)

---

Dear Physis,

I now understand what you mean. Yes, HS is the only kind of deduction system (among HS, ND and SC) for which the context is never modified by the inference rules and hence, HS is the only system that, in the case one is interested in only tautologies (i.e. $\vdash \phi$) and not in hypothetical judgments (i.e. the more general form $\Gamma \vdash \phi$), one can formulate the notion of provability without introducing a notion of contexts.

That derivability of tautologies in HS can be defined more easily is certainly the reason why HS has come first, historically. Nevertheless, I would not restrict HS to this property. The most general form of HS needs to refer to judgements of the form $\Gamma \vdash \phi$ (again I'm thinking about DT) in its definition and the restricted, simplest form, that does not require to mention explicit contexts, addresses only the derivability of pure tautologies.

Especially, I agree that the property that contexts are never changed by the inference rules is an essential property of HS and I have no objection against saying that the not-changing nature of contexts in the definition of provability is the essence of HS.

Still, I would not consider that HS relies on a different kind of judgment than ND or SC do. In all three kinds of systems, judgments are predicates of the metalanguage that are characterized by a set of inference rules and a judgment is by no way reducible to a formula. A judgment asserts the provably of a formula, it is not itself a formula. The only difference with ND and SC is that in ND and SC, judgments in the empty context (i.e. judgements asserting the provability of a tautology) cannot be defined without referring to non-empty contexts while in HS, judgments in the empty context can be defined without referring to any kind of context.

DT is indeed not an inference rule of HS but DT is a statement about derivability, and it cannot be formulated without introducing the notion $\Gamma \vdash \phi$ at some point of the definition of HS.

From a didactic point of view, it may be indeed interesting to first define the judgments $\vdash \phi$ and to define the more general notion $\Gamma \vdash \phi$ (so that DT can be stated) only in a second step.

Regarding SC in implicit context form (i.e. as a tree of formulas, like ND), the trick is the following: Instead of having just a "judgment" of the form "A true" as in Natural deduction, we use three kinds of judgments which are "A true", "A false" and "contradiction". The inference rules (for classical logic), then, are the following:

${\cfrac {\begin{matrix}{\cfrac {}{A\ true}}u\\\vdots \\B\ true\end{matrix}}{A\supset B\ true}}\supset R^{u}\qquad {\cfrac {A\ true\quad B\ false}{A\supset B\ false}}\supset L$

${\cfrac {\begin{matrix}{\cfrac {}{A\ false}}u\\\vdots \\contradiction\end{matrix}}{A\ true}}\ ContradictR^{u}\qquad {\cfrac {\begin{matrix}{\cfrac {}{A\ true}}u\\\vdots \\contradiction\end{matrix}}{A\ false}}\ ContradictL^{u}$

${\frac {A\ true\qquad B\ true}{A\land B\ true}}\land R\qquad {\frac {A\ false}{A\land B\ false}}\land L_{1}\qquad {\frac {\qquad B\ false}{A\land B\ false}}\land L_{2}$

${\frac {A\ true\qquad A\ false}{contradiction}}Cut$

This is somehow a presentation which is standard for the introduction rules in the proof search community and that has additional rules for cut and reasoning by contradiction. I don't know how far this is an original presentation, it is taken from a work of mine (page 7).

I'm afraid not to be of great help regarding the "ontology" of the notion of judgments. I believe I generally use it in a rather naive way as a generic name for the kind of inductively defined predicates used in metatheory when talking about logic as an object of study. In its more general view, definitions like "$\phi$ is a formula", "$\phi$ and $\psi$ are isomorphic", "$\phi$ is provable", "$\phi$ is provable in the empty context", "$\phi$ is true", "t is a term built from symbols f₁,...,f_n", "the variable x occurs in formula $\phi$", etc. are considered by some authors as judgments.

PS: It could be interesting to look at how metatheory is formalized in practice. For instance the Coq proof assistant is a software in which the notions of provability in HS, ND or SC can be defined in a rather simple way. If I find time I may elaborate on the use of such software as a metalanguage for talking about logic. --Hugo Herbelin (talk) 13:30, 6 January 2008 (UTC)

---

Dear User:Hugo Herbelin,

Thank You very much the kind and detailed answer. It helped to me to unify several disjointed bits, I did not grasped such an overview before.

I lacked overview, now thank You for illuminating

• "judgment" is not an especially distinguished entity, it is not separated from other predicates in the metaheory. I thought previously that judgments are sort of "lower lever", "standing closer to the kernel", than "other" metatheoretic assertions, moreover, other metatheoretic assertions are built on top of them.
• HS can be formalized also in $\Gamma \vdash \phi$ style rules of inference. Although they are not context-changing, but this approach has still advantages, because in this way, we can define the concept of deduction in one go. The only solution I knew till now was to say axioms and rules in a context-less form, then build on top of it a $\Gamma \vdash \phi$ concept, using auxiliary techniques (e.g. sequence)
• Sequent calculus can be approached also by the discharging technique.

I shall modify my changes in both affected articles

• lead of Hilbert-style deduction system
• Judgment (mathematical logic)

accordingly to what You have written.

Thank You also for about writing about Coq. I read about it somewhere in the materials provided by the Haskell community, but I have to learn yet much about proof theoretic aspects of functional programming. The thing I did in Haskell was to write an untyped combinatory logic interpreter (augmented with some computer algebra capabilities), then with its help to write a quine in pure combinatory logic: an expression that is equivalent to its own quotation (i.e term tree representation).

Best wishes,

Physis (talk) 12:41, 7 January 2008 (UTC)

ϕ vs φ

The article uses ϕ in LaTeX formulas and φ in the text itself, as if they are the same symbol. It should be consistent and use only one of them. --salty-horse (talk) 22:44, 3 January 2009 (UTC)

Article name

Why is the frequently used Hilbert system a redirect to the infrequently used Hilbert-style deduction system? I propose to reverse this redirect. — Charles Stewart (talk) 10:01, 26 February 2009 (UTC)

Move applied. — Charles Stewart (talk) 07:33, 15 April 2009 (UTC)

Article is a mess...

...and some of it is my fault. I'll slap on a Template:Contradict notice on it. The main issues are:

1. Doesn't really recognise the differences between different sorts of Hilbert system. The most important distinction is the threefold distinction between (i) systems that have schemes that are short for infinite sets of axioms, (ii) systems with axioms that contain schematic variables, which have a special rule, typically combined into axiom instantiation and rule unification, and (iii) systems with a rule of uniform substitution.

2. Has a straightforward contradiction: the lede asserts that systems for predicate logic needs a generalisation rule, the body asserts that generalisation is a meta-theorem. The contradiction is introduced by me; which claim is true depends on which kind of Hilbert system one uses.

3. Has a convoluted reference section whose contents do not obviously provide sources to the article.

4. Has some rather glib claims, e.g. the asserted difference between Hilbert systems and natural deduction. In fact the inference system that takes a Hilbert system and extends its notion of inference by allowing such metatheorems as the deduction theorem as steps is widely called natural deduction.

5. Oh, and I also introduced -ise spelling into an article that was using -ize spelling. Trivial, but still an issue.

The article is clearly in need of intensive care. I haven't time in the next few days; it would be wonderful if on my return some kind soul had done the edits, otherwise I will get around to it... — Charles Stewart (talk) 08:36, 16 April 2009 (UTC)

What is missing is: (1) the idea that a Hilbert system is a fully-developed Formalist notion and what exactly this means (i.e. it is utterly mechanical in nature), (2) a fully-developed example of a formalist system that is traceable back to a reference/source; I put in two that are highly-polished and of historical importance (e.g. Gōdel in his 1930 and 1931 references Hilbert and Ackermann 1928; I have not seen this work, but it must be similar to Hilbert's 1927), and (3) the historical import (e.g. Gōdel in particular). Wvbailey (talk) 15:33, 16 April 2009 (UTC)

---

Well here it's almost 2 years later. So I've forgotten all this stuff. That means I'm looking at this with newbie eyes. I scanned the article and was left clueless. I figured I'd just blow this one off, but then I slept on it and woke up curious.

My first, most important, question: Is there a reliable source that I trust and I can comprehend (key concepts) that actually uses the words "Hilbert system"? (Yes, after a long search, exactly 1 book.)

Second question: And is a "Hilbert system" a "Hilbert-style deductive system"? (Haven't a clue.)

Third question: In fifty words or less, what is it? (It's an antidote to model theory called "proof theory" of which there are a number of alternates that includes the "Gentzen-type system" and has variants due to guys like von Neumann. Model theory is t and f and truth tables. Proof theory (I surmise) is how to get from INPUT (assertions) to OUTPUT (a derived formula) via manipulation of abstract symbols per rules defined at the outset (44 words).)

Fourth question: Does it include the four categories described in Hilbert 1927, or just the first one? Or just the first and second ones? (Haven't a clue):

1. Propositional calculus
2. Predicate calculus
3. Equality
4. Number theory

Fifth question: This is related to Question 6. Is this just some archaic, historically-interesting backwater? (Kleene shows how to analyze arguments. But does anyone use this stuff anymore?)

Sixth question: What's the relationship between this stuff and the theory of abstract machines [Turing machine or a counter machine]? At every instance of a conditional instruction and combinatorial line(s) (such as A ← A + B), "symbol manipulation" and modus ponens (detachment) is at work. That's how the computation proceeds: given that A + B, we detach the sum and put it in location A. It's all Markovian, once its been derived, we move on. And clearly we have replacement (substitution).

I hunted through all my books on logic (including Kleene 1952) and came up with only one "hit" re "Hilbert system"-- actually indexed that way in Kleene 1967 Mathematical Logic, republished 2002 by Dover Publications, Inc., Mineola, NY, ISBN 0-486-42339 (pbk.). In his 1952 he derives all the following stuff but doesn't actually call it a "Hibert system" that I could see.

Who called it a "Hilbert system"? Haven't a clue except it looks like Kleene can be implicated in the crime:

"It is controversial whether one does better to start with a postulated formulation of logic based on modus ponens (a "Hilbert-type system" §50, 54) and derive the introduction and elimination rules, as we have done, or to start out with a version of the latter as the postulated rules (a "Gentzen-type system").

"No one formulation is most convenient for all purposes. One formulation with postulated axioms and rules is necessary to give a firm starting point for proof theory . . . we have preferred to start from the struturally simpler Hilbert-type systems in §§ 9, 21." Pages 126-127

• So what's proof theory? It is a "theory" alternate to model theory:

We stood outside the language of the sentences themselves (the object language), and observed in another language (the observer's language) how the sentences (or formulas) are composed to atoms . . . we call this treatment of logic "model theory", as in it we replace the atoms by truth values t and f in all possible combinations, to obtain what can be considered models or concrete replicas of what the sentences may express."

Now we shall take up another way of founding logic. This treatment, called "proof theory" . . . But now . . . the inferences cannot be made by appealing to logical criteria but only to specifically stated axioms and rules. In proof theory, some sentences or formulas will be taken as logical "axioms" and some "rules of inference" will be established for making the inferences from some sentences to another sentence.

As axioms . . . we take all formulas of any of the forms shown after the symbol "⊧" in 1a-10b of Theorem 2 (and in the "List of Postulates" p. 387). These forms we call axiom schemata. Each axiom schema includes infinitely many axioms, one for each choice of the forumlas denoted by "A", "B", "C". . . [he gives an example]

As the sole rule of inference, called the ⊃-rule or modus ponens or the rule of detachment, we take the operation of passing from two formulas of the respective forms A and A⊃B to the formula B, for any choice of formulas A and B. In an inference by this rule, the formulas A and B are the premises, and B is the conclusion.

"We define a (formal) proof (in the propositional calculus) to be a finite list of (occurrrences of) formulas [etc] . . . A proof is said to be a proof of its last formula Bi. If a proof of a given formula B exists, we say B is (formally) provable, or is a (formal) theorem, or in symbols ⊦ B [assertion of B]." (pages 33-34).

So what is the little symbol ⊧ mean? It means "is valid" [cf p. 14 from an exhaustive truth-table investigation]. In a footnote he expands the notion:

" . . . "⊧ E" as a short way of writing E is valid¹⁵ ". ¹⁵ Expressions containing "⊧" ("⊧ E" here and "A₁, . . . , A_m ⊧ B" in §7) are not formulas of the object language, but expressions of the observer's languge used in writing concisely certain statements about formulas. . . . [hence it] outranks ∾, ⊃, &, V, ¬ . . .."(page 14)

Okay, so what are his "axioms"? Well, it depends. I believe we are talking only about the propositional calculus. But if we're going to inlcude the Predicate calculus, and Equality, then there are more. And for number theory, even more. For the propositional calculus:

• MODUS PONENS A, A ⊃ B ⇒ B. [I'm using the ⇒ to symbolize the traditional underline, i.e. "yields"]
• 1a. A ⊃ (B ⊃ A).
• 1b. (A ⊃ B) ⊃ ((A ⊃ (B ⊃ C)) ⊃ (A ⊃ C))
• 3. A ⊃ (B ⊃ A & B)
• 4a. A & B ⊃ A.
• 4b. A & B ⊃ B.
• 5a. A ⊃ A V B.
• 5b. B ⊃ A V B.
• 6. (A ⊃ C) ⊃ ((B ⊃ C)) ⊃ (A V B ⊃ C)).
• 7. (A ⊃ B) ⊃ ((A ⊃ ¬B) ⊃ ¬A).
• 8. ¬¬A ⊃ A.
• 9a. (A ⊃ B) ⊃ ((B ⊃ A) ⊃ ( A ∾ B). [Thus the ∾ symbol for Kleene is IFF, logical equality)
• 10a. ( A ∾ B) ⊃ (A ⊃ B)
• 10b. ( A ∾ B) ⊃ (B ⊃ A)

For the predicate calculus (additional, pp. 107, 94-96, 150):

• ∀-SCHEMA. ∀xA(x) ⊃ A(r). ∃-SCHEMA. A(r) ⊃ ∃xA(x).

The term r must be free fo the variable x in the formula A(x).

• ∀-RULE. C ⊃ A(x) ⇒ C ⊃ ∀xA(x). ∃-RULE. A(x) ⊃ C ⇒ ∃xA(x) ⊃ C.

The vriable x must not occur free in the formula C.

For the use of Equality (additional, p. 154)

• (a) x = x.
• (b) x = y. ⊃ (x = z ⊃ y = z)
• (c_iⁿ) x = y ⊃ (P(a₁, . . ., a_i-1, x, a_i+1, . . ., a_n) ⊃ P(a₁, . . ., a_i-1, y, a_i+1, . . ., a_n))
• (d_iⁿ) x = y ⊃ f(a₁, . . ., a_i-1, x, a_i+1, . . ., a_n) ⊃ f(a₁, . . ., a_i-1, y, a_i+1, . . ., a_n))

At least in my mind, the symbolisms etc need further expansion: what's a P() and a f()?

⊧⊃¬∼∾∀∃⇒ Anyway, he goes on in section 9 to discuss the notion of (formal) deduction from assumption formulas (page 35). In section 10 appears "The deduction theorem" which he blames on Herbrand 1930:

• If A ⊦ B, then ⊦ A ⊃ B. (b) If A₁, . . ., A_m-1, A_m ⊦ B, then A₁, . . ., A_m-1 ⊦ A_m ⊃ B.

The proof is sufficiently opaque. Section 11 is Introduction and Elimination Rules. Section 12 is Completeness., Section 13 is Use of Derived Rules. This is sufficiently overwhelming. So I'm going to stop now.

Anyway, this may provide some background that I can pull from. BillWvbailey (talk) 17:43, 3 February 2011 (UTC)

I made my edit in response to a request to see if the contradiction notice could be removed, and so I rewrote parts necessary to solve my points 1&2. It's still a mess, but not a contradictory mess now. — Charles Stewart (talk) 18:13, 3 February 2011 (UTC)

Answers:

1. It's well established. First book I pull off my shelf uses it: Blackburn, de Rijke & Venema, *Modal Logic*.
2. Yes. Hilbert system is used much more often
3. There's more to proof theory than what you say - Girard says pretty things like how it exposes the fundamental symmetries in logic - but yes, it must do what you say, and Hilbert system's are the simplest things that do the job.
4. The article axiomatises 1 to 3, but not 4. Showing how a modal logic can be axiomatised (say S5), would be nice.
5. No. It's the standard primitive-recursive way to axiomatise consequence relations.
6. Indirect, through number theory.
7. You'd be surprised at how much disagreement the exact definition of the terms "proof system" and "proof calculus" provoke amongst experts.

Cheers, — Charles Stewart (talk) 18:35, 3 February 2011 (UTC)

Thanks. I got the same request you did. But last time I looked at this was 2 years ago and I didn't clearly understand then that this is a topic in "proof theory" (as distinct from its extension via the extra axioms, into number theory). Which brings me to . . .

Some clarifications RE question #5, and a new question #7 re proof theory vs recursion.

• 5a. Does your answer "no" mean that proof theory it's just some archaic subject? Or does it mean it's still an active field of research, i.e. in "modal logic", or in recursion theory?
• 5b. Does "recursion" come about only after introduction of the extra axioms of "number" i.e. via the inductive axiom/hypothesis, the successor, 0, replacement/substitution? And then the "schema" we think of as recursion follow as a proof? Or is it something like modus ponens that has to be assumed at the outset?
• 7. Are the axioms of number necessary for number theory? There's no "looping" (as in recursion) allowed in proof theory is there? A proof "goes in a straight line", "down hill" as it were, no loop-backs allowed, correct? So it's combinatorial only, correct? Or is there a way to "build" number theory from only the 3 sets of axioms above? (Maybe even only the first two, without "equality").

Thanks again, Bill Wvbailey (talk) 19:58, 3 February 2011 (UTC)

Qn 5: I mean, no, it's not some historically interesting backwater, but it is a standard part of the logician's toolkit. You most often want to characterise the logical consequnce relation of a given logic using (i) a class of models and (ii) a Hilbert system. After that, you might be interested in various further formalisations, such as sequaent calculus, tableaux decision procedure, &c. By primitive recursive, I mean there is a primitive recursive acceptor of valid proofs: for Hilbert system's this is easy, as a proof is a list of formulae all of whose elements are either instances of axioms or obtained by modus ponens from other formulae earlier in the list, as axiomatised by Gödel. Qn 7: The axioms are not enough, since they are validated by models with any finite, nonzero number of elements. — Charles Stewart (talk) 20:38, 7 February 2011 (UTC)

Ben Ari [1] calls it "Hilbert system" --Anonymous 14:52, 1 September 2011 (UTC) — Preceding unsigned comment added by 84.58.201.140 (talk)

I'm not sure, but my impression is that things like satisfiability modulo theories are essentially (i.e. in practice, when implemented in software) Hilbert systems, with the "theories" referring to the model-theoritic theories resulting from additional axioms. So its not just equality (aka the "free theory") or number theory, but more practically the axioms of linear algebra (which are used in ? Maybe chip design layout? The best modern-day references I've ever seen on this topic were about formal design verification testing of some computer chip layout. Wish I could find them and re-read them...) I think that the point is that, because Hilbert systems are mechanistic, you can convert them to software, and then, by playing with different axiom sets, you'd have systems for testing different aspects of a chip design. So, in that sense, its an "active field of research", just maybe not in the philosophy/math depts of universities. And .. for this reason, it would be nice if this articlee was tightened up.67.198.37.16 (talk) 02:52, 15 December 2018 (UTC)

is it really a work by Hilbert?

from A. S. Troelstra in “basic proof theory”:

"2.5.3. Hilbert systems. Kleene [1952a] uses the term “Hilbert-type system”; this was apparently suggested by Gentzen [1935], who speaks of “einem dem Hilbertschen Formalismus angeglichenen Kalkiil”. Papers and books such as Hilbert [1926,1928], Hilbert and Ackermann [1928], Hilbert and Bernays [1934] have made such formalisms widely known, but they date from long before Hilbert; already Frege [1879] introduced a formalism of this kind (if one disregards the enormous notational differences). We have simplified the term “Hilbert-type system” to “Hilbert system”. There is one aspect in which our system differs from the systems used by Hilbert and Frege: they stated the axioms, not as schemas, but with proposition variables and/or relation variables for A, B, C, and added a substitution rule. As far as we know, von Neumann [1927] was the first to use axiom schemas."

Even in Hilbert and Ackermann [1928], they mentioned that this was first done by Frege. I think we should change the subject to something like "Hilbert-style system" or "Hilbert-type system" but I should take a look at A. Church’ Great Book for more information on history. — Preceding unsigned comment added by Mrmusavi (talk • contribs) 12:08, 8 October 2012 (UTC)

I support this idea. I would support a change to the article's title. I've been bothered from day one by the confusion between Hilbert's system (see Hilbert's papers in van Heijenoort, where it's clearly spelled out) and the various "systems" that followed. Kleene 1952:441ff indeed uses the words "Hilbert-type system" (see the index p. 543) in contrast to a formal system derived from Gentzen, as follows: "The formal system of propostiional and predicated calculus studied previously (Chapters IV ff.) we call now a Hilbert-type system, and denote by H. Precisely, H denotes any one or a particular one of several systems, according to wheter we are considering propositional calculus or predicate caluculus, in the classical or intuitionsitic version . . .."(p. 441) He then introduces the "Gentzen-type system G1". Previously in setting up his formal system (cf pages 69ff) Kleene makes use of "Hilbert and Ackermann 1928, Hibert and Bernays 1934, 1939, Gentzen 1934-5, Bernays 1936, and less immediate sources" (p. 69). Bill Wvbailey (talk) 14:40, 8 October 2012 (UTC)

I'd go even farther and rename it "Hilbert-style deductive system". Then it is very clear from the title what the article is about. Right now the title is completely opaque to me. — Carl (CBM · talk) 14:48, 8 October 2012 (UTC)

A 1989 paper I'm reading now says, I quote: "natural deduction as opposed to Hilbert-style deduction" 67.198.37.16 (talk) 02:38, 15 December 2018 (UTC)

Possible error in axiom list

I believe that the axioms listed for the Hilbert system have a small error. The logical axioms each need to be preceded by a list of arbitrary universal quantifiers. E.g., instead of

$\phi \rightarrow (\psi \rightarrow \phi ),$

it should read

$\forall ^{\star }(\phi \rightarrow (\psi \rightarrow \phi )),$

where $\forall ^{\star }$ denotes a sequence of arbitrarily many universal quantifiers over arbitrary variables. And so forth for all the other axioms. Otherwise you can't infer, e.g., $\forall x(R(x)\rightarrow R(x))$ (supposing that $R$ is a unary relation). (The universal introduction rule requires that the quantified variable not be free in the formula of interest.) See, e.g., https://cs.uwaterloo.ca/~david/cs245/cs-firstorder.pdf.

Nick Thomas <nwthomas@asu.edu> — Preceding unsigned comment added by 68.230.67.135 (talk) 10:06, 22 November 2012 (UTC)

And I think, in the equality axioms I8, I9, there should also be universal quantifiers at the beginning. 128.176.181.5 (talk) 16:41, 18 February 2013 (UTC)

The axioms do not need to be explicitly preceded by universal quantifiers, as non-closed propositions are implicitly assumed to be universally quantified in the semantics. In fact new rules need to be added to the calculus if the axioms are so changed, in order to eliminate occurences of the quantifiers when axioms are invoked, making the calculus both more complicated to formalise, more complicated to use and not the same calculus as that proposed by Hilbert and Ackermann. — Charles Stewart (talk) 08:54, 5 April 2016 (UTC)

Problems with Universal generalisation and Uniform substution

The page says: "Universal quantification is often given an alternative axiomatisation using an extra rule of generalisation (see the section on Metatheorems), in which case the rules Q6 and Q7 are redundant."

I can't see how this can be the case. It is easy to prove Q6 and Q7 using universal generalisation and the deduction theorem, but proving the deduction theorem as a metatheorem with universal generalisation as a rule (as well as modus ponens) requires Q6 and Q7.

Conversely, I don't see how you could do anything without universal generalisation as a rule. How would you prove something as simple as $\forall x(x=x)$? You can't use substitution of equivalents because $x=x$ contains x free.

Is there perhaps a mistake here?

The page also says: "US. Let $\phi (p)$ be a formula with one or more instances of the propositional variable $p$, and let $\psi$ be another formula. Then from $\phi (p)$, infer $\phi (\psi )$."

This also seems wrong to me. Let $\phi (p)$ be $p\rightarrow q$ and let $\psi$ be $\neg q$.

Then we have from $p\rightarrow q$, infer $\neg q\rightarrow q$, which is clearly wrong.

I think what it's meant to be is:

"US. Let $\phi (p)$ be a theorem with one or more instances of the propositional variable $p$, and let $\psi$ be a formula. Then $\phi (\psi )$ is also a theorem."

In other words, if $\vdash \!\phi (p)$ then $\vdash \!\phi (\psi )$

AndreRD (talk) 11:50, 16 June 2016 (UTC)

I agree. These seem like valid complaints. They need fixing. Let me add dubious tags 67.198.37.16 (talk) 02:13, 15 December 2018 (UTC)

Conjunction introduction and elimination

Am I reading this right?

A -> B -> A ^ B

I'm not seeing any mention of the branching rule used. This should be explicitly mentioned somehow. I'm assuming left branching and reading it this way: "(A implies B) implies (A and B)"

This would mean that if we accept that A implies B we have to accept B. What? And it means that if we accept that A implies B we have to accept A. What? Something seems to be wrong here.

If we assume some sort of right branching scheme it could be: "A implies (B implies (A and B))"

Which seems fine. But right branching schemes require reading all the way to the end of a potentially very long expression before you can even figure out how to group terms, and then going back to the beginning of the expression and employing the previously discovered grouping while reading the expression. Could this really be how a standard notation for a Hilbert system works? It seems to me there must be something wrong here. Perhaps the expression in question was formulated incorrectly. But either way, to avoid confusion, some convention should be employed to allow a reader to figure out notation conventions. Perhaps a section on notation should be included in each article that covers a logical system. If Wikipedia employs certain agreed upon conventions about logical notations, then one or more articles about those conventions should be crafted and those articles could be linked to in a sufficiently prominent way from articles about logical systems. Readers should not have to guess, and notation systems used should be made explicit somehow. Comiscuous (talk) 19:48, 19 December 2021 (UTC)