ในตรรกศาสตร์โดยเฉพาะอย่างยิ่งทฤษฎีการพิสูจน์ระบบฮิลเบิร์ตบางครั้งเรียกว่าแคลคูลัส ฮิ ลเบิร์ต ระบบแบบฮิลเบิร์ตระบบการพิสูจน์แบบฮิลเบิร์ต ระบบการอนุมานแบบฮิ ลเบิร์ต หรือระบบฮิลเบิร์ต-แอคเคอร์แมนน์เป็นระบบการพิสูจน์อย่างเป็นทางการ ประเภทหนึ่ง ที่เชื่อกันว่าเป็นผลงานของก็อตต์ลอบ เฟรเก^{[ 1 ]}และเดวิด ฮิลเบิร์ต^{[ 2 ]}ระบบการอนุมานเหล่านี้มักถูกศึกษาในตรรกศาสตร์ลำดับที่หนึ่งแต่ก็มีความน่าสนใจสำหรับตรรกศาสตร์อื่นๆ เช่นกัน

ระบบฮิลเบิร์ตถูกนิยามว่าเป็นระบบนิรนัยที่สร้างทฤษฎีบทจากสัจพจน์และกฎการอนุมาน^{[ 3 ] [ 4 ] [ 5 ]}โดยเฉพาะอย่างยิ่งหากกฎการอนุมานที่กำหนดไว้เพียงอย่างเดียวคือmodus ponens [ ^{6 ] [ 7 ] ระบบ} ฮิลเบิร์ตทุกระบบเป็น ระบบสัจพจน์ซึ่งผู้เขียนหลายคนใช้เป็นคำที่ไม่เฉพาะเจาะจงมากนักเพื่อประกาศระบบฮิลเบิร์ตของตน^{[ 8 ] [ 9 ] [ 10 ]}โดยไม่ต้องกล่าวถึงคำที่เฉพาะเจาะจงกว่านี้ ในบริบทนี้ "ระบบฮิลเบิร์ต" จะถูกเปรียบเทียบกับระบบนิรนัยตามธรรมชาติ^{[ 3 ]}ซึ่งไม่ได้ใช้สัจพจน์ แต่ใช้เฉพาะกฎการอนุมานเท่านั้น

ในขณะที่แหล่งข้อมูลทั้งหมดที่อ้างถึงระบบการพิสูจน์เชิงตรรกะแบบ "สัจพจน์" จะอธิบายลักษณะโดยง่ายว่าเป็นระบบการพิสูจน์เชิงตรรกะที่มีสัจพจน์ แหล่งข้อมูลที่ใช้คำว่า "ระบบฮิลเบิร์ต" ในรูปแบบต่างๆ บางครั้งก็ให้คำจำกัดความในลักษณะที่แตกต่างกัน ซึ่งจะไม่นำมาใช้ในบทความนี้ ตัวอย่างเช่นTroelstraนิยาม "ระบบฮิลเบิร์ต" ว่าเป็นระบบที่มีสัจพจน์และมีและเป็นกฎการอนุมานเพียงอย่างเดียว^{[ 11 ]}บางครั้งชุดสัจพจน์เฉพาะก็เรียกว่า "ระบบฮิลเบิร์ต" ^{[ 12 ]}หรือ "แคลคูลัสแบบฮิลเบิร์ต" ^{[ 13 ]}บางครั้ง คำว่า "แบบฮิลเบิร์ต" ใช้เพื่อสื่อถึงประเภทของระบบสัจพจน์ที่มีสัจพจน์ในรูปแบบแผนผัง^{[ 2 ]}ดังเช่นใน§ รูปแบบแผนผังของ P2ด้านล่าง—แต่แหล่งข้อมูลอื่นใช้คำว่า "แบบฮิลเบิร์ต" ครอบคลุมทั้งระบบที่มีสัจพจน์แบบแผนผังและระบบที่มีกฎการแทนที่^{[ 14 ]}ดังเช่นในบทความนี้ การใช้คำว่า "แบบฮิลเบิร์ต" และคำที่คล้ายกันเพื่ออธิบายระบบการพิสูจน์สัจพจน์ในตรรกศาสตร์นั้นเกิดจากอิทธิพลของหลักการตรรกศาสตร์ทางคณิตศาสตร์ของ ฮิลเบิร์ตและ แอคเคอร์แมน (1928) ^{[ 2 ]}${\displaystyle {\rightarrow }E}$${\displaystyle {\forall }I}$

ระบบฮิลเบิร์ตส่วนใหญ่ใช้แนวทางเฉพาะในการสร้างสมดุลระหว่างสัจพจน์เชิงตรรกะและกฎการอนุมาน^{[ 1 ] [ 6 ] [ 15 ] [ 11 ]} ระบบฮิลเบิร์ตสามารถระบุลักษณะได้จากการเลือกใช้ แบบแผนสัจพจน์เชิงตรรกะจำนวนมาก และชุด กฎการอนุมาน จำนวนน้อย ระบบการหักล้างตามธรรมชาติ ใช้แนวทางตรงกันข้าม โดยมีกฎการ หักล้างจำนวนมากแต่มีแบบแผนสัจพจน์น้อยมากหรือไม่มีเลย^{[ 3 ]}ระบบฮิลเบิร์ตที่ศึกษากันโดยทั่วไปมีกฎการอนุมานเพียงข้อเดียว – modus ponensสำหรับตรรกะเชิงประพจน์  – หรือสองข้อ – พร้อมการวางนัยทั่วไปเพื่อจัดการกับตรรกะเชิงภาคแสดงด้วย – และแบบแผนสัจพจน์อนันต์หลายแบบ ระบบฮิลเบิร์ตสำหรับตรรกะเชิงโมดอล เชิงความจริง ซึ่งบางครั้งเรียกว่าระบบฮิลเบิร์ต-ลูอิสยังต้องการกฎความจำเป็นเพิ่มเติม อีกด้วย บางระบบใช้รายการสูตรที่เป็นรูปธรรมจำนวนจำกัดเป็นสัจพจน์แทนที่จะใช้ชุดสูตรอนันต์ผ่านแผนผังสัจพจน์ ซึ่งในกรณีนี้จำเป็นต้องใช้กฎการแทนที่แบบสม่ำเสมอ^{[ 14 ]}

ลักษณะเด่นของระบบฮิลเบิร์ตหลายรูปแบบคือ บริบทจะไม่เปลี่ยนแปลงในกฎการอนุมานใดๆ ของระบบเหล่านั้น ในขณะที่การอนุมานแบบธรรมชาติและแคลคูลัสลำดับมีกฎที่เปลี่ยนแปลงบริบทอยู่บ้าง^{[ 16 ]}ดังนั้น หากเราสนใจเฉพาะการอนุมานสัจนิรันดร์ เท่านั้น โดยไม่สนใจการตัดสินเชิงสมมติฐาน เราสามารถทำให้ระบบฮิลเบิร์ตเป็นทางการได้ในลักษณะที่กฎการอนุมานของระบบนั้นประกอบด้วยการตัดสินในรูปแบบที่ค่อนข้างง่ายเท่านั้น ซึ่งไม่สามารถทำได้กับระบบการอนุมานอีกสองระบบ เนื่องจากบริบทเปลี่ยนแปลงไปในกฎการอนุมานบางข้อของระบบเหล่านั้น จึงไม่สามารถทำให้เป็นทางการได้เพื่อหลีกเลี่ยงการตัดสินเชิงสมมติฐาน แม้ว่าเราต้องการใช้ระบบเหล่านั้นเพื่อพิสูจน์การอนุมานสัจนิรันดร์เท่านั้นก็ตาม

ในระบบฮิลเบิร์ตการหักล้างอย่างเป็นทางการ (หรือการพิสูจน์ ) คือลำดับสูตรที่จำกัด ซึ่งแต่ละสูตรเป็นสัจพจน์หรือได้มาจากสูตรก่อนหน้าโดยใช้กฎการอนุมาน^{[ 17 ]}การหักล้างอย่างเป็นทางการเหล่านี้มีจุดประสงค์เพื่อสะท้อนการพิสูจน์ในภาษาธรรมชาติ แม้ว่าจะมีรายละเอียดมากกว่ามากก็ตาม^{[ 18 ]}

สมมติว่าเป็นเซตของสูตร ซึ่งถือเป็นสมมติฐานตัวอย่างเช่นอาจเป็นเซตของสัจพจน์สำหรับทฤษฎีกลุ่มหรือทฤษฎีเซตสัญลักษณ์หมายความว่ามีการอนุมานที่สิ้นสุดลงโดยใช้สัจพจน์เชิงตรรกะและองค์ประกอบของ เป็นสัจพจน์ เท่านั้น ^{[ 19 ]}ดังนั้น อย่างไม่เป็นทางการหมายความว่าสามารถพิสูจน์ได้โดยสมมติว่าสูตรทั้งหมดใน ${\displaystyle \Gamma }$${\displaystyle \Gamma }$${\displaystyle \Gamma \vdash \phi }$${\displaystyle \phi }$${\displaystyle \Gamma }$${\displaystyle \Gamma \vdash \phi }$${\displaystyle \phi }$${\displaystyle \Gamma }$

ระบบฮิลเบิร์ตมีลักษณะเฉพาะคือการใช้แผนผังของสัจพจน์เชิงตรรกะ จำนวนมาก แผนผังสัจพจน์คือเซตสัจพจน์อนันต์ที่ได้มาจากการแทนที่สูตรทั้งหมดในรูปแบบใดรูปแบบหนึ่งลงในรูปแบบเฉพาะ^{[ 20 ]}เซตของสัจพจน์เชิงตรรกะไม่เพียงแต่รวมถึงสัจพจน์ที่สร้างขึ้นจากรูปแบบนี้เท่านั้น แต่ยังรวมถึงการสรุปทั่วไปของสัจพจน์เหล่านั้นด้วย^{[ 21 ]} การสรุปทั่วไปของสูตรได้มาจากการเพิ่มตัวบ่งปริมาณสากลศูนย์ตัวหรือมากกว่านั้นไว้ข้างหน้าสูตร ตัวอย่างเช่น เป็นการสรุป ทั่วไป ของ${\displaystyle \forall y(\forall xPxy\to Pty)}$${\displaystyle \forall xPxy\to Pty}$

ต่อไปนี้เป็นระบบฮิลเบิร์ตบางส่วนที่ใช้ในตรรกศาสตร์เชิงประพจน์หนึ่งในนั้นคือรูปแบบแผนผังของ P2ซึ่งถือว่าเป็นระบบเฟรเกด้วย

การพิสูจน์เชิงสัจพจน์ถูกนำมาใช้ในคณิตศาสตร์ตั้งแต่ตำราเรียนภาษากรีกโบราณ ที่มีชื่อเสียง อย่างElements of Geometryของยูคลิดประมาณ 300 ปี ก่อน คริสตกาล แต่ระบบการพิสูจน์ ที่เป็นทางการอย่างสมบูรณ์แบบ ระบบ แรกที่รู้จักกันซึ่งมีคุณสมบัติเป็นระบบฮิลเบิร์ตนั้นย้อนกลับไปถึงBegriffsschriftของGottlob Frege ใน ปี 1879 ^{[ 9 ] [ 22 ]}ระบบของ Frege ใช้เพียงการบ่งชี้และการปฏิเสธเป็นตัวเชื่อม^{[ 23 ]}และมีสัจพจน์หกข้อ^{[ 22 ]}ซึ่งได้แก่: ^{[ 24 ] [ 25 ]}

• ข้อเสนอที่ 1:${\displaystyle a\supset (b\supset a)}$
• ข้อเสนอที่ 2:${\displaystyle (c\supset (b\supset a))\supset ((c\supset b)\supset (c\supset a))}$
• ข้อเสนอที่ 8:${\displaystyle (d\supset (b\supset a))\supset (b\supset (d\supset a))}$
• ข้อเสนอที่ 28:${\displaystyle (b\supset a)\supset (\neg a\supset \neg b)}$
• ข้อเสนอที่ 31:${\displaystyle \neg \neg a\supset a}$
• ข้อเสนอที่ 41:${\displaystyle a\supset \neg \neg a}$

สิ่งเหล่านี้ถูกใช้โดย Frege ร่วมกับ modus ponens และกฎการแทนที่ (ซึ่งถูกใช้แต่ไม่เคยระบุอย่างแม่นยำ) เพื่อให้ได้ระบบสัจพจน์ที่สมบูรณ์และสอดคล้องกันของตรรกะเชิงประพจน์แบบคลาสสิกที่ทำหน้าที่ความจริง^{[ 24 ]}

Jan Łukasiewiczแสดงให้เห็นว่าในระบบของ Frege นั้น "สัจพจน์ข้อที่สามนั้นไม่จำเป็น เนื่องจากสามารถอนุมานได้จากสัจพจน์สองข้อก่อนหน้า และสัจพจน์สามข้อสุดท้ายสามารถแทนที่ด้วยประโยคเดียวได้" ^{[ 25 ]} ซึ่งเมื่อนำออกจาก สัญลักษณ์ภาษาโปแลนด์ของ Łukasiewicz มาเป็นสัญลักษณ์สมัยใหม่ จะหมายถึงดังนั้น Łukasiewicz จึงได้รับการยกย่อง^{[ 22 ]}ด้วยระบบสัจพจน์สามข้อนี้: ${\displaystyle CCNpNqCqp}$${\displaystyle (\neg p\rightarrow \neg q)\rightarrow (q\rightarrow p)}$

• ${\displaystyle p\to (q\to p)}$
• ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$
• ${\displaystyle (\neg p\to \neg q)\to (q\to p)}$

เช่นเดียวกับระบบของ Frege ระบบนี้ใช้กฎการแทนที่และใช้ modus ponens เป็นกฎการอนุมาน^{[ 22 ]}ระบบเดียวกันนี้ได้รับการนำเสนอ (พร้อมกฎการแทนที่ที่ชัดเจน) โดย^Alonzo Church [ ^{26 ]}ซึ่งเรียกมันว่าระบบ P ₂ ^{[ 26 ] [ 27 ]}และช่วยเผยแพร่ให้เป็นที่นิยม^{[ 27 ]}

อาจหลีกเลี่ยงการใช้กฎการแทนที่โดยให้สัจพจน์ในรูปแบบแผนผัง โดยใช้สัจพจน์เหล่านั้นเพื่อสร้างชุดสัจพจน์อนันต์ ดังนั้น การใช้อักษรกรีกแทนแผนผัง (ตัวแปรอภิปรัชญาที่อาจแทนสูตรที่มีรูปแบบที่ดี ใดๆ ก็ได้ ) สัจพจน์จึงถูกกำหนดดังนี้: ^{[ 9 ] [ 27 ]}

• ${\displaystyle \varphi \to (\psi \to \varphi )}$
• ${\displaystyle (\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))}$
• ${\displaystyle (\neg \varphi \to \neg \psi )\to (\psi \to \varphi )}$

แผนผังเวอร์ชันของ P ₂ได้รับการระบุว่าเป็นผลงานของ^John von Neumann [ ^{22 ]}และใช้ในฐานข้อมูลการพิสูจน์อย่างเป็นทางการ "set.mm" ของ Metamath ^{[ 27 ]}อันที่จริง แนวคิดเรื่องการใช้แผนผังสัจพจน์เพื่อแทนที่กฎการแทนที่นั้นได้รับการระบุว่าเป็นผลงานของ von Neumann ^{[ 28 ]}แผนผังเวอร์ชันของ P ₂ยังได้รับการระบุว่าเป็นผลงานของHilbertและได้รับการตั้งชื่อในบริบทนี้ ด้วย ^{[ 29 ]}${\displaystyle {\mathcal {H}}}$

ระบบตรรกะเชิงประพจน์ที่มีกฎการอนุมานเป็นแบบแผนเรียกว่าระบบ Frege เช่นกัน ดังที่ผู้เขียนที่กำหนดคำว่า "ระบบ Frege" ^{[ 30 ]}ตั้งข้อสังเกตไว้ว่า ระบบนี้ไม่รวมระบบของ Frege เองที่กล่าวไว้ข้างต้น เนื่องจากมีสัจพจน์แทนที่จะเป็นแบบแผนสัจพจน์^{[ 28 ]}

ตัวอย่างเช่น การพิสูจน์ใน P ₂แสดงไว้ด้านล่าง ก่อนอื่น เราจะตั้งชื่อให้กับสัจพจน์: ${\displaystyle A\to A}$

(A1)${\displaystyle (p\to (q\to p))}$

(เอ2)${\displaystyle ((p\to (q\to r))\to ((p\to q)\to (p\to r)))}$

(เอ3)${\displaystyle ((\neg p\to \neg q)\to (q\to p))}$

และหลักฐานพิสูจน์มีดังนี้:

1. ${\displaystyle A\to ((B\to A)\to A)}$       (ตัวอย่างของ (A1))
2. ${\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}$       (ตัวอย่างของ (A2))
3. ${\displaystyle (A\to (B\to A))\to (A\to A)}$       (จาก (1) และ (2) โดยmodus ponens )
4. ${\displaystyle A\to (B\to A)}$       (ตัวอย่างของ (A1))
5. ${\displaystyle A\to A}$       (จาก (4) และ (3) โดย modus ponens)

ตรรกะเชิงประพจน์มีระบบสัจพจน์ได้มากมายนับไม่ถ้วน เนื่องจากตรรกะใดๆ ก็ตามย่อมมีอิสระในการเลือกสัจพจน์และกฎที่ใช้อธิบายตรรกะนั้นๆ ในที่นี้เราจะอธิบายระบบของฮิลเบิร์ตที่มีสัจพจน์เก้าข้อและกฎ modus ponens เพียงข้อเดียว ซึ่งเราเรียกว่าระบบสัจพจน์แบบกฎเดียว และเป็นระบบที่อธิบายตรรกะเชิงสมการแบบคลาสสิก เราจะกล่าวถึงภาษาขั้นต่ำสำหรับตรรกะนี้ โดยที่สูตรต่างๆ ใช้เพียงตัวเชื่อมและตัวบ่งปริมาณเท่านั้นต่อมาเราจะแสดงให้เห็นว่าระบบนี้สามารถขยายเพื่อรวมตัวเชื่อมทางตรรกะเพิ่มเติม เช่นและได้โดยไม่ต้องขยายขอบเขตของสูตรที่สามารถอนุมานได้ ${\displaystyle \lnot }$${\displaystyle \to }$${\displaystyle \forall }$${\displaystyle \land }$${\displaystyle \lor }$

แผนผังสัจพจน์เชิงตรรกะสี่แบบแรก (ร่วมกับ modus ponens) ช่วยให้สามารถจัดการกับตัวเชื่อมทางตรรกะได้

ป1.${\displaystyle \phi \to \phi }$

หน้า 2.${\displaystyle \phi \to \left(\psi \to \phi \right)}$

หน้า 3${\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}$

หน้า 4.${\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}$

สัจพจน์ P1 นั้นซ้ำซ้อน เนื่องจากเป็นผลมาจาก P3, P2 และ modus ponens (ดูการพิสูจน์ ) สัจพจน์เหล่านี้อธิบายตรรกศาสตร์ประพจน์แบบคลาสสิกหากไม่มีสัจพจน์ P4 เราจะได้ตรรกศาสตร์เชิงบ่งชี้เชิงบวกตรรกศาสตร์ขั้นต่ำสุดนั้นเกิดขึ้นได้โดยการเพิ่มสัจพจน์ P4m แทน หรือโดยการกำหนด เป็น${\displaystyle \lnot \phi }$${\displaystyle \phi \to \bot }$

พี4ม.${\displaystyle \left(\phi \to \psi \right)\to \left(\left(\phi \to \lnot \psi \right)\to \lnot \phi \right)}$

ตรรกศาสตร์เชิงสัญชาตญาณเกิดขึ้นได้จากการเพิ่มสัจพจน์ P4i และ P5i เข้าไปในตรรกศาสตร์เชิงบ่งชี้เชิงบวก หรือโดยการเพิ่มสัจพจน์ P5i เข้าไปในตรรกศาสตร์ขั้นต่ำ ทั้ง P4i และ P5i เป็นทฤษฎีบทของตรรกศาสตร์เชิงประพจน์แบบคลาสสิก

พี4i.${\displaystyle \left(\phi \to \lnot \phi \right)\to \lnot \phi }$

พี5i.${\displaystyle \lnot \phi \to \left(\phi \to \psi \right)}$

โปรดทราบว่าสิ่งเหล่านี้คือแผนผังสัจพจน์ ซึ่งแสดงถึงตัวอย่างเฉพาะของสัจพจน์จำนวนอนันต์ ตัวอย่างเช่น P1 อาจแสดงถึงตัวอย่างสัจพจน์เฉพาะหรืออาจแสดงถึง: เป็นตำแหน่งที่สามารถวางสูตรใดๆ ก็ได้ ตัวแปรเช่นนี้ที่ครอบคลุมสูตรต่างๆ เรียกว่า 'ตัวแปรแผนผัง' ${\displaystyle p\to p}$${\displaystyle \left(p\to q\right)\to \left(p\to q\right)}$${\displaystyle \phi }$

ด้วยกฎการแทนที่แบบสม่ำเสมอ ข้อที่สอง (US) เราสามารถเปลี่ยนแผนผังสัจพจน์แต่ละอันให้เป็นสัจพจน์เดียวได้ โดยแทนที่ตัวแปรแผนผังแต่ละตัวด้วยตัวแปรเชิงประพจน์บางตัวที่ไม่ได้กล่าวถึงในสัจพจน์ใดๆ เพื่อให้ได้สิ่งที่เราเรียกว่าการกำหนดสัจพจน์แบบแทนที่ การกำหนดรูปแบบทั้งสองแบบมีตัวแปร แต่ในขณะที่การกำหนดสัจพจน์แบบกฎเดียวมีตัวแปรแผนผังที่อยู่นอกเหนือภาษาของตรรกศาสตร์ การกำหนดสัจพจน์แบบแทนที่ใช้ตัวแปรเชิงประพจน์ที่ทำหน้าที่เดียวกันโดยการแสดงแนวคิดของตัวแปรที่ครอบคลุมสูตรต่างๆ ด้วยกฎที่ใช้การแทนที่

สหรัฐอเมริกา ให้เป็นสูตรที่มีตัวแปรเชิงประพจน์อย่างน้อยหนึ่งตัวและให้เป็นอีกสูตรหนึ่ง จากนั้นจากอนุมานได้ว่า${\displaystyle \phi (p)}$${\displaystyle p}$${\displaystyle \psi }$${\displaystyle \phi (p)}$${\displaystyle \phi (\psi )}$

แผนผังสัจพจน์เชิงตรรกะสามแบบถัดไปนี้เสนอวิธีการเพิ่ม จัดการ และลบตัวบ่งปริมาณสากล

Q5. โดยที่tสามารถใช้แทนx ได้ ใน${\displaystyle \forall x\left(\phi \right)\to \phi [x:=t]}$${\displaystyle \,\!\phi }$

คำถามที่ 6.${\displaystyle \forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)}$

Q7. โดยที่xไม่เป็นอิสระใน.${\displaystyle \phi \to \forall x\left(\phi \right)}$${\displaystyle \phi }$

กฎเพิ่มเติมทั้งสามข้อนี้ขยายระบบประพจน์เพื่อกำหนดสัจพจน์ให้กับตรรกะภาคแสดงแบบคลาสสิก ในทำนองเดียวกัน กฎทั้งสามข้อนี้ขยายระบบสำหรับตรรกะประพจน์แบบสัญชาตญาณ (ด้วย P1-3 และ P4i และ P5i) ไปสู่ ตรรกะภาคแสดง แบบ สัญชาตญาณ

การกำหนดปริมาณแบบสากลนั้น มักได้รับการกำหนดสัจพจน์ทางเลือกโดยใช้กฎการสรุปทั่วไปเพิ่มเติม ซึ่งในกรณีนี้ กฎ Q6 และ Q7 จะซ้ำซ้อน

• การสรุปทั่วไป : ถ้าและxไม่ปรากฏอย่างอิสระในสูตรใดๆของแล้ว${\displaystyle \Gamma \vdash \phi }$${\displaystyle \Gamma }$${\displaystyle \Gamma \vdash \forall x\phi }$

โครงร่างสัจพจน์ขั้นสุดท้ายจำเป็นสำหรับการทำงานกับสูตรที่มีสัญลักษณ์เท่ากับ

I8. สำหรับตัวแปรx ทุก ตัว${\displaystyle x=x}$

I9.${\displaystyle \left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)}$

โดยทั่วไป ระบบฮิลเบิร์ตมักจะประกอบด้วยสัจพจน์สำหรับตัวดำเนินการทางตรรกะ ได้แก่ การบ่งชี้และการปฏิเสธ เพื่อให้เกิดความสมบูรณ์เชิงฟังก์ชันเมื่อมีสัจพจน์เหล่านี้แล้ว ก็สามารถสร้างส่วนขยายแบบอนุรักษ์นิยมของทฤษฎีบทการอนุมานที่อนุญาตให้ใช้ตัวเชื่อมเพิ่มเติมได้ ส่วนขยายเหล่านี้เรียกว่าแบบอนุรักษ์นิยม เพราะหากสูตร φ ที่เกี่ยวข้องกับตัวเชื่อมใหม่ถูกเขียนใหม่เป็น สูตร θ ที่เทียบเท่าทางตรรกะ ซึ่งเกี่ยวข้องเฉพาะการปฏิเสธ การบ่งชี้ และการหาปริมาณสากลแล้ว φ จะสามารถหาได้ในระบบที่ขยายออกไปก็ต่อเมื่อ θ สามารถหาได้ในระบบดั้งเดิมเท่านั้น เมื่อขยายอย่างสมบูรณ์แล้ว ระบบฮิล เบิ ร์ตจะคล้ายคลึงกับระบบการอนุมานตามธรรมชาติ มากขึ้น

• การแนะนำ

${\displaystyle \forall x(\phi \to \exists y(\phi [x:=y]))}$

• การคัดออก

${\displaystyle \forall x(\phi \to \psi )\to (\exists x(\phi )\to \psi )}$โดยที่ไม่ใช่ตัวแปรอิสระของ${\displaystyle x}$${\displaystyle \psi }$

• การแนะนำและการกำจัดคำสันธาน

การแนะนำ:${\displaystyle \alpha \to (\beta \to \alpha \land \beta )}$

เหลือผู้เข้ารอบคัดออก:${\displaystyle \alpha \wedge \beta \to \alpha }$

สิทธิ์ในการคัดออก:${\displaystyle \alpha \wedge \beta \to \beta }$

• การแนะนำและการกำจัดการแยก

บทนำด้านซ้าย:${\displaystyle \alpha \to \alpha \vee \beta }$

บทนำด้านขวา:${\displaystyle \beta \to \alpha \vee \beta }$

การคัดออก:${\displaystyle (\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )}$

• รายชื่อระบบฮิลเบิร์ต
• การอนุมานตามธรรมชาติ
• แคลคูลัสลำดับ

• Gaifman, Haim. "ระบบนิรนัยแบบฮิลเบิร์ตสำหรับตรรกะประโยค ความสมบูรณ์ และความกะทัดรัด" (PDF )
• Farmer, WM "ตรรกศาสตร์เชิงประพจน์" (PDF )โดยจะอธิบาย (ในบรรดาเรื่องอื่นๆ) ระบบการพิสูจน์แบบฮิลเบิร์ตเฉพาะ (ซึ่งจำกัดเฉพาะแคลคูลัสเชิงประพจน์ )