ระบบฮิลเบิร์ต

Q: ข้อมูลสำคัญเกี่ยวกับ ระบบฮิลเบิร์ต

ในตรรกศาสตร์โดยเฉพาะอย่างยิ่งทฤษฎีการพิสูจน์ระบบฮิลเบิร์ตบางครั้งเรียกว่าแคลคูลัส ฮิ ลเบิร์ต ระบบแบบฮิลเบิร์ตระบบการพิสูจน์แบบฮิลเบิร์ตระบบการอนุมานแบบฮิล เบิร์ต หรือ ระบบ

Q: ตรรกศาสตร์เชิงประพจน์

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

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

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

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

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

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

การหักลดหย่อนอย่างเป็นทางการ

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

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

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

ตรรกศาสตร์เชิงประพจน์

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

Frege's Begriffsschrift

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

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

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

ของ Łukasiewicz

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

$p\to (q\to p)$
$(p\to (q\to r))\to ((p\to q)\to (p\to r))$
$(\neg p\to \neg q)\to (q\to p)$

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

รูปแบบแผนผังของ P

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

$\varphi \to (\psi \to \varphi )$
$(\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))$
$(\neg \varphi \to \neg \psi )\to (\psi \to \varphi )$

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

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

ตัวอย่างการพิสูจน์ในหน้า

ตัวอย่างเช่น การพิสูจน์ $A\to A$ ใน P มีรายละเอียดดังต่อไปนี้ ก่อนอื่น เราจะตั้งชื่อให้กับสัจพจน์ต่างๆ:

(A1)

(p\to (q\to p))

(เอ2)

((p\to (q\to r))\to ((p\to q)\to (p\to r)))

(เอ3)

((\neg p\to \neg q)\to (q\to p))

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

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

ตรรกศาสตร์ภาคแสดง (ระบบตัวอย่าง)

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

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

ป1.

\phi \to \phi

หน้า 2.

\phi \to \left(\psi \to \phi \right)

หน้า 3

\left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)

หน้า 4.

\left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)

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

พี4ม.

\left(\phi \to \psi \right)\to \left(\left(\phi \to \lnot \psi \right)\to \lnot \phi \right)

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

พี4i.

\left(\phi \to \lnot \phi \right)\to \lnot \phi

พี5i.

\lnot \phi \to \left(\phi \to \psi \right)

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

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

พวกเรา. ให้

\phi (p)

เป็นสูตรที่มีตัวแปรเชิงประพจน์อย่างน้อยหนึ่งตัว

p

และปล่อยให้

\psi

เป็นสูตรอื่น จากนั้นจากนั้น

\phi (p)

อนุมาน

\phi (\psi )

.

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

คำถามที่ 5.

\forall x\left(\phi \right)\to \phi [x:=t]

โดยที่tสามารถแทนด้วยxได้

\,\!\phi

คำถามที่ 6.

\forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)

คำถามที่ 7.

\phi \to \forall x\left(\phi \right)

โดยที่xไม่เป็นอิสระใน

\phi

.

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

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

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

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

I8.

x=x

สำหรับตัวแปรx ทุก ตัว

I9.

\left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)

ส่วนขยายแบบอนุรักษ์นิยม

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

การวัดเชิงอัตถิภาวะ

การแนะนำ

\forall x(\phi \to \exists y(\phi [x:=y]))

การคัดออก

\forall x(\phi \to \psi )\to (\exists x(\phi )\to \psi )

ที่ไหน

x

ไม่ใช่ตัวแปรอิสระของ

\psi

.

การเชื่อมและการแยก

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

การแนะนำ:

\alpha \to (\beta \to \alpha \land \beta )

เหลือผู้เข้ารอบคัดออก:

\alpha \wedge \beta \to \alpha

สิทธิ์ในการคัดออก:

\alpha \wedge \beta \to \beta

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

บทนำด้านซ้าย:

\alpha \to \alpha \vee \beta

บทนำด้านขวา:

\beta \to \alpha \vee \beta

การคัดออก:

(\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )

ดูเพิ่มเติม

หมายเหตุ

1 2 Máté & Ruzsa 1997:129
1 2 3 Smith, Peter (2013-02-21). บทนำสู่ทฤษฎีบทของเกอเดล . สำนักพิมพ์มหาวิทยาลัยเคมบริดจ์. หน้า 10. ISBN 978-1-107-02284-3.
1 2 3 Restall, Greg (2002-09-11). บทนำสู่ตรรกศาสตร์เชิงโครงสร้างย่อย . Routledge. หน้า73–74 . ISBN 978-1-135-11131-1.
↑ Gaifman, Haim (2002). "ระบบนิรนัยแบบฮิลเบิร์ตสำหรับตรรกะประโยค ความสมบูรณ์ และความกะทัดรัด" (PDF) . โคลัมเบีย. สืบค้นเมื่อ2024-08-19 .
↑ Benthem, Johan van; Gupta, Amitabha; Parikh, Rohit (2011-04-02). การพิสูจน์ การคำนวณ และตัวแทน: ตรรกะ ณ ทางแยก Springer Science & Business Media. หน้า41. ISBN 978-94-007-0080-2.
1 2เบคอน, แอนดรูว์ (2023-09-29). บทนำเชิงปรัชญาสู่ตรรกศาสตร์ลำดับสูง . เทย์เลอร์ แอนด์ ฟรานซิส. หน้า424. ISBN 978-1-000-92575-3.
↑ไอค์, ยาน ฟาน (1991-02-26) Logics in AI: European Workshop JELIA '90, อัมสเตอร์ดัม, เนเธอร์แลนด์, 10-14 กันยายน 1990. การดำเนินการ สื่อวิทยาศาสตร์และธุรกิจสปริงเกอร์ พี113. ไอเอสบีเอ็น 978-3-540-53686-4.
↑ Haack, Susan (27 กรกฎาคม 1978). ปรัชญาตรรกศาสตร์ . สำนักพิมพ์มหาวิทยาลัยเคมบริดจ์. หน้า19. ISBN 978-0-521-29329-7.
1 2 3 Bostock, David (1997). ตรรกศาสตร์ระดับกลาง . อ็อกซ์ฟอร์ด: นิวยอร์ก: สำนักพิมพ์แคลเรนดอน; สำนักพิมพ์มหาวิทยาลัยอ็อกซ์ฟอร์ด. หน้า4–5 , 8–13 , 18–19 , 22, 27, 29, 191, 194. ISBN 978-0-19-875141-0.
↑ Lucas, JR (2018-10-10). ตำราว่าด้วยเวลาและอวกาศ . Routledge. หน้า152. ISBN 978-0-429-68517-0.
1 2 Troelstra, AS; Schwichtenberg, H. (2000). ทฤษฎีการพิสูจน์พื้นฐาน . Cambridge Tracts in Theoretical Computer Science ( ฉบับที่ 2). Cambridge: Cambridge University Press. หน้า51. doi : 10.1017/cbo9781139168717 . ISBN 978-0-521-77911-1.
↑ "บทนำสู่ตรรกศาสตร์ - บทที่ 4" . intrologic.stanford.edu . สืบค้นเมื่อ2024-08-16 .
↑ Buss, SR (9 กรกฎาคม 1998). คู่มือทฤษฎีการพิสูจน์ . Elsevier. หน้า552–553 . ISBN 978-0-08-053318-6.
1 2 Ono, Hiroakira (2019-08-02). ทฤษฎีการพิสูจน์และพีชคณิตในตรรกศาสตร์ . Springer. หน้า5. ISBN 978-981-13-7997-0.
↑ไอค์, ยาน ฟาน (1991-02-26) Logics in AI: European Workshop JELIA '90, อัมสเตอร์ดัม, เนเธอร์แลนด์, 10-14 กันยายน 1990. การดำเนินการ สื่อวิทยาศาสตร์และธุรกิจสปริงเกอร์ พี113. ไอเอสบีเอ็น 978-3-540-53686-4.
↑ Gabbay, Dov M.; Guenthner, Franz (14 มีนาคม 2013). คู่มือตรรกศาสตร์เชิงปรัชญา . Springer Science & Business Media. หน้า201. ISBN 978-94-017-0458-8.
↑ Kute, Tushar B. "ระบบฮิลเบิร์ต" (PDF) . มหาวิทยาลัยสโตนีบรูก. สืบค้นเมื่อ21 พฤศจิกายน 2025 .
↑ Stonybrook. "บทที่ 8: ระบบฮิลเบิร์ต" (PDF) . มหาวิทยาลัยสโตนีบรูก. สืบค้นเมื่อ21 พฤศจิกายน 2025 .
↑ Kute, Tushar B. "ระบบฮิลเบิร์ต" (PDF) . มหาวิทยาลัยสโตนีบรูก. สืบค้นเมื่อ21 พฤศจิกายน 2025 .
↑ Goertzel, Ben. "การอนุมานในตรรกศาสตร์ลำดับที่หนึ่ง" (PDF) . Goertzel.org . สืบค้นเมื่อ21 พฤศจิกายน 2025 .
↑ Kute, Tushar B. "ระบบฮิลเบิร์ต" (PDF) . มหาวิทยาลัยสโตนีบรูก. สืบค้นเมื่อ21 พฤศจิกายน 2025 .
1 2 3 4 5 Smullyan, Raymond M. (2014-07-23). คู่มือเบื้องต้นสำหรับตรรกศาสตร์คณิตศาสตร์ . Courier Corporation. หน้า102–103 . ISBN 978-0-486-49237-7.
↑ Franks, Curtis (2023), "ตรรกศาสตร์เชิงประพจน์"ใน Zalta, Edward N.; Nodelman, Uri (บรรณาธิการ), สารานุกรมปรัชญาแห่งมหาวิทยาลัยสแตนฟอร์ด ( ฉบับฤดูใบไม้ร่วง 2023), ห้องปฏิบัติการวิจัยอภิปรัชญา มหาวิทยาลัยสแตนฟอร์ด สืบค้นเมื่อ2024-03-22
1 2 Mendelsohn, Richard L. (2005-01-10). ปรัชญาของ Gottlob Frege . สำนักพิมพ์มหาวิทยาลัยเคมบริดจ์. หน้า185. ISBN 978-1-139-44403-3.
1 2วูคาซีวิคซ์ ม.ค. (1970) Jan Lukasiewicz: ผลงานที่เลือก . นอร์ธฮอลแลนด์ พี136.
1 2 Church, Alonzo (1996). บทนำสู่ตรรกศาสตร์ทางคณิตศาสตร์ . สำนักพิมพ์มหาวิทยาลัยพรินซ์ตัน. หน้า119. ISBN 978-0-691-02906-1.
1 2 3 4 "Proof Explorer - หน้าหลัก - Metamath" . us.metamath.org . สืบค้นเมื่อ2024-07-02 .
1 2 Cook, Stephen A.; Reckhow, Robert A. (1979). "ประสิทธิภาพเชิงสัมพัทธ์ของระบบการพิสูจน์เชิงประพจน์"วารสารตรรกศาสตร์เชิงสัญลักษณ์ 44 ( 1): 39. doi : 10.2307/2273702 . ISSN 0022-4812 . JSTOR 2273702 .
↑ Walicki, Michał (2017). บทนำสู่ตรรกศาสตร์ทางคณิตศาสตร์ ( ฉบับขยาย). นิวเจอร์ซีย์: World Scientific. หน้า126. ISBN 978-981-4719-95-7.
↑ Pudlák, Pavel; Buss, Samuel R. (1995). "วิธีการโกหกโดยไม่ถูกตัดสินว่ามีความผิด (อย่างง่ายดาย) และความยาวของการพิสูจน์ในแคลคูลัสเชิงประพจน์"ใน Pacholski, Leszek; Tiuryn, Jerzy (บรรณาธิการ). ตรรกศาสตร์วิทยาการคอมพิวเตอร์ . บันทึกการบรรยายในวิทยาการคอมพิวเตอร์. เล่มที่933. เบอร์ลิน, ไฮเดลเบิร์ก: Springer. หน้า152. doi : 10.1007/BFb0022253 . ISBN 978-3-540-49404-1.

ลิงก์ภายนอก

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

[Máté_&_Ruzsa_1997-1] 1 2 Máté & Ruzsa 1997:129

[:1-2] 1 2 3 Smith, Peter (2013-02-21). บทนำสู่ทฤษฎีบทของเกอเดล . สำนักพิมพ์มหาวิทยาลัยเคมบริดจ์. หน้า 10. ISBN 978-1-107-02284-3.

[:2-3] 1 2 3 Restall, Greg (2002-09-11). บทนำสู่ตรรกศาสตร์เชิงโครงสร้างย่อย . Routledge. หน้า73–74 . ISBN 978-1-135-11131-1.

[4] Gaifman, Haim (2002). "ระบบนิรนัยแบบฮิลเบิร์ตสำหรับตรรกะประโยค ความสมบูรณ์ และความกะทัดรัด" (PDF) . โคลัมเบีย. สืบค้นเมื่อ2024-08-19 .

[5] Benthem, Johan van; Gupta, Amitabha; Parikh, Rohit (2011-04-02). การพิสูจน์ การคำนวณ และตัวแทน: ตรรกะ ณ ทางแยก Springer Science & Business Media. หน้า41. ISBN 978-94-007-0080-2.

[Bacon_424-6] 1 2เบคอน, แอนดรูว์ (2023-09-29). บทนำเชิงปรัชญาสู่ตรรกศาสตร์ลำดับสูง . เทย์เลอร์ แอนด์ ฟรานซิส. หน้า424. ISBN 978-1-000-92575-3.

[7] ไอค์, ยาน ฟาน (1991-02-26) Logics in AI: European Workshop JELIA '90, อัมสเตอร์ดัม, เนเธอร์แลนด์, 10-14 กันยายน 1990. การดำเนินการ สื่อวิทยาศาสตร์และธุรกิจสปริงเกอร์ พี113. ไอเอสบีเอ็น 978-3-540-53686-4.

[8] Haack, Susan (27 กรกฎาคม 1978). ปรัชญาตรรกศาสตร์ . สำนักพิมพ์มหาวิทยาลัยเคมบริดจ์. หน้า19. ISBN 978-0-521-29329-7.

[BostockIntermediate-9] 1 2 3 Bostock, David (1997). ตรรกศาสตร์ระดับกลาง . อ็อกซ์ฟอร์ด: นิวยอร์ก: สำนักพิมพ์แคลเรนดอน; สำนักพิมพ์มหาวิทยาลัยอ็อกซ์ฟอร์ด. หน้า4–5 , 8–13 , 18–19 , 22, 27, 29, 191, 194. ISBN 978-0-19-875141-0.

[10] Lucas, JR (2018-10-10). ตำราว่าด้วยเวลาและอวกาศ . Routledge. หน้า152. ISBN 978-0-429-68517-0.

[Basic_Proof_Theory-11] 1 2 Troelstra, AS; Schwichtenberg, H. (2000). ทฤษฎีการพิสูจน์พื้นฐาน . Cambridge Tracts in Theoretical Computer Science ( ฉบับที่ 2). Cambridge: Cambridge University Press. หน้า51. doi : 10.1017/cbo9781139168717 . ISBN 978-0-521-77911-1.

[12] "บทนำสู่ตรรกศาสตร์ - บทที่ 4" . intrologic.stanford.edu . สืบค้นเมื่อ2024-08-16 .

[13] Buss, SR (9 กรกฎาคม 1998). คู่มือทฤษฎีการพิสูจน์ . Elsevier. หน้า552–553 . ISBN 978-0-08-053318-6.

[Ono_5-14] 1 2 Ono, Hiroakira (2019-08-02). ทฤษฎีการพิสูจน์และพีชคณิตในตรรกศาสตร์ . Springer. หน้า5. ISBN 978-981-13-7997-0.

[15] ไอค์, ยาน ฟาน (1991-02-26) Logics in AI: European Workshop JELIA '90, อัมสเตอร์ดัม, เนเธอร์แลนด์, 10-14 กันยายน 1990. การดำเนินการ สื่อวิทยาศาสตร์และธุรกิจสปริงเกอร์ พี113. ไอเอสบีเอ็น 978-3-540-53686-4.

[16] Gabbay, Dov M.; Guenthner, Franz (14 มีนาคม 2013). คู่มือตรรกศาสตร์เชิงปรัชญา . Springer Science & Business Media. หน้า201. ISBN 978-94-017-0458-8.

[17] Kute, Tushar B. "ระบบฮิลเบิร์ต" (PDF) . มหาวิทยาลัยสโตนีบรูก. สืบค้นเมื่อ21 พฤศจิกายน 2025 .

[18] Stonybrook. "บทที่ 8: ระบบฮิลเบิร์ต" (PDF) . มหาวิทยาลัยสโตนีบรูก. สืบค้นเมื่อ21 พฤศจิกายน 2025 .

[19] Kute, Tushar B. "ระบบฮิลเบิร์ต" (PDF) . มหาวิทยาลัยสโตนีบรูก. สืบค้นเมื่อ21 พฤศจิกายน 2025 .

[20] Goertzel, Ben. "การอนุมานในตรรกศาสตร์ลำดับที่หนึ่ง" (PDF) . Goertzel.org . สืบค้นเมื่อ21 พฤศจิกายน 2025 .

[21] Kute, Tushar B. "ระบบฮิลเบิร์ต" (PDF) . มหาวิทยาลัยสโตนีบรูก. สืบค้นเมื่อ21 พฤศจิกายน 2025 .

[:44-22] 1 2 3 4 5 Smullyan, Raymond M. (2014-07-23). คู่มือเบื้องต้นสำหรับตรรกศาสตร์คณิตศาสตร์ . Courier Corporation. หน้า102–103 . ISBN 978-0-486-49237-7.

[SEP_PropositionalLogic-23] Franks, Curtis (2023), "ตรรกศาสตร์เชิงประพจน์"ใน Zalta, Edward N.; Nodelman, Uri (บรรณาธิการ), สารานุกรมปรัชญาแห่งมหาวิทยาลัยสแตนฟอร์ด ( ฉบับฤดูใบไม้ร่วง 2023), ห้องปฏิบัติการวิจัยอภิปรัชญา มหาวิทยาลัยสแตนฟอร์ด สืบค้นเมื่อ2024-03-22

[:45-24] 1 2 Mendelsohn, Richard L. (2005-01-10). ปรัชญาของ Gottlob Frege . สำนักพิมพ์มหาวิทยาลัยเคมบริดจ์. หน้า185. ISBN 978-1-139-44403-3.

[:46-25] 1 2วูคาซีวิคซ์ ม.ค. (1970) Jan Lukasiewicz: ผลงานที่เลือก . นอร์ธฮอลแลนด์ พี136.

[:47-26] 1 2 Church, Alonzo (1996). บทนำสู่ตรรกศาสตร์ทางคณิตศาสตร์ . สำนักพิมพ์มหาวิทยาลัยพรินซ์ตัน. หน้า119. ISBN 978-0-691-02906-1.

[:48-27] 1 2 3 4 "Proof Explorer - หน้าหลัก - Metamath" . us.metamath.org . สืบค้นเมื่อ2024-07-02 .

[:12-28] 1 2 Cook, Stephen A.; Reckhow, Robert A. (1979). "ประสิทธิภาพเชิงสัมพัทธ์ของระบบการพิสูจน์เชิงประพจน์"วารสารตรรกศาสตร์เชิงสัญลักษณ์ 44 ( 1): 39. doi : 10.2307/2273702 . ISSN 0022-4812 . JSTOR 2273702 .

[:49-29] Walicki, Michał (2017). บทนำสู่ตรรกศาสตร์ทางคณิตศาสตร์ ( ฉบับขยาย). นิวเจอร์ซีย์: World Scientific. หน้า126. ISBN 978-981-4719-95-7.

[:0-30] Pudlák, Pavel; Buss, Samuel R. (1995). "วิธีการโกหกโดยไม่ถูกตัดสินว่ามีความผิด (อย่างง่ายดาย) และความยาวของการพิสูจน์ในแคลคูลัสเชิงประพจน์"ใน Pacholski, Leszek; Tiuryn, Jerzy (บรรณาธิการ). ตรรกศาสตร์วิทยาการคอมพิวเตอร์ . บันทึกการบรรยายในวิทยาการคอมพิวเตอร์. เล่มที่933. เบอร์ลิน, ไฮเดลเบิร์ก: Springer. หน้า152. doi : 10.1007/BFb0022253 . ISBN 978-3-540-49404-1.

[

[ 4 ]

[ 5 ]

6 ] [

7 ] ระบบ

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[ 13 ]

[ 14 ]

[ 15 ]

[ 16 ]

[ 17 ]

[ 18 ]

19

[ 20 ]

[ 21 ]

[