ระบบที่เป็นทางการ (หรือระบบนิรนัย ) คือโครงสร้างนามธรรมและการทำให้เป็นทางการของระบบสัจพจน์ที่ใช้สำหรับการอนุมานทฤษฎีบทจากสัจพจน์โดยใช้กฎการอนุมาน^{[ 1 ]}

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

คำว่า รูปแบบนิยม (formalism)บางครั้งมีความหมายเหมือนกับระบบที่เป็นทางการ (formal system ) อย่างคร่าวๆ แต่ก็ยังหมายถึงรูปแบบการเขียนสัญลักษณ์ แบบใดแบบหนึ่งด้วย เช่นสัญลักษณ์ bra–ketของPaul Dirac

ระบบที่เป็นทางการมีส่วนประกอบต่อไปนี้เป็นอย่างน้อย: ^{[ 3 ] [ 4 ] [ 5 ]}

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

กล่าวได้ว่าระบบที่เป็นทางการนั้นเป็นระบบแบบเรียกซ้ำ (กล่าวคือมีประสิทธิภาพ) หรือสามารถแจงนับได้แบบเรียกซ้ำ หากเซตของสัจพจน์และเซตของกฎการอนุมานเป็นเซตที่ตัดสินได้หรือเซตที่ตัดสินได้บางส่วนตามลำดับ

ภาษาเชิงรูปธรรมคือ ภาษาที่ใช้ชุดของสตริงซึ่งสัญลักษณ์ต่างๆ มาจากตัวอักษรเฉพาะ และใช้การดำเนินการเพื่อสร้างประโยคจากสตริงเหล่านั้น เช่นเดียวกับภาษาในทางภาษาศาสตร์ภาษาเชิงรูปธรรมโดยทั่วไปมีสองด้าน:

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

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

ระบบนิรนัยหรือเรียกอีกอย่างว่าเครื่องมือนิรนัย [ ^{8 ]}ประกอบด้วยสัจพจน์ (หรือ^{แผนผัง}สัจพจน์ ) และกฎการอนุมานที่สามารถใช้เพื่ออนุมานทฤษฎีบทของระบบ^{[ 1 ]}

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

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

ตัวอย่างของระบบนิรนัย ได้แก่ กฎการอนุมานและสัจพจน์เกี่ยวกับความเท่าเทียมกันที่ ใช้ในตรรกศาสตร์ลำดับที่หนึ่ง

ระบบการอนุมานหลักสองประเภทคือ ระบบการพิสูจน์และความหมายเชิงรูปธรรม^{[ 8 ] [ 9 ]}

การพิสูจน์เชิงรูปธรรม คือ ลำดับของสูตรที่มีรูปแบบดี (หรือ WFF สำหรับเรียกสั้นๆ) ซึ่งอาจเป็นสัจพจน์หรือเป็นผลมาจากการใช้กฎการอนุมานกับ WFF ก่อนหน้าในลำดับการพิสูจน์

เมื่อกำหนดระบบที่เป็นทางการแล้ว เราสามารถกำหนดเซตของทฤษฎีบทที่สามารถพิสูจน์ได้ภายในระบบที่เป็นทางการนั้น เซตนี้ประกอบด้วย WFF ทั้งหมดที่มีการพิสูจน์ ดังนั้นสัจพจน์ทั้งหมดจึงถือว่าเป็นทฤษฎีบท แตกต่างจากไวยากรณ์สำหรับ WFF ตรงที่ไม่มีการรับประกันว่าจะมีขั้นตอนการตัดสินใจว่า WFF ที่กำหนดให้เป็นทฤษฎีบทหรือไม่

มุมมองที่ว่าการสร้างบทพิสูจน์เชิงรูปธรรมเป็นทั้งหมดของคณิตศาสตร์นั้น มักเรียกว่าลัทธิรูปนิยม (Formalism ) เดวิด ฮิลเบิร์ตได้ก่อตั้งอภิคณิตศาสตร์ (Metamathematics) ขึ้นมา ในฐานะสาขาวิชาสำหรับการอภิปรายระบบเชิงรูปธรรม ภาษาใดๆ ที่ใช้ในการพูดคุยเกี่ยวกับระบบเชิงรูปธรรมเรียกว่าภาษาอภิ (Metalanguage ) ภาษาอภิอาจเป็นภาษาธรรมชาติ หรืออาจเป็นภาษาที่มีการกำหนดรูปแบบบางส่วน แต่โดยทั่วไปแล้วจะกำหนดรูปแบบได้ไม่สมบูรณ์เท่ากับส่วนประกอบภาษาเชิงรูปธรรมของระบบเชิงรูปธรรมที่กำลังพิจารณาอยู่ ซึ่งเรียกว่าภาษาเป้าหมาย (Object language)หรือก็คือสิ่งที่เป็นเป้าหมายของการอภิปรายนั่นเอง แนวคิดของทฤษฎีบทที่เพิ่งนิยามไปนั้นไม่ควรสับสนกับทฤษฎีบทเกี่ยวกับระบบเชิงรูปธรรมซึ่งเพื่อหลีกเลี่ยงความสับสน มักเรียกว่าทฤษฎีบทอภิ (Metatheorems )

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

ระบบตรรกะคือ:

• ถูกต้องหากสูตรที่สมบูรณ์ซึ่งสามารถอนุมานได้จากสัจพจน์ทุกข้อนั้น สอดคล้องกับแบบจำลองทุกแบบของระบบตรรกะ
• สมบูรณ์ในเชิงความหมายหากสูตรที่ถูกต้องทุกสูตรซึ่งเป็นจริงในทุกแบบจำลองของระบบตรรกะ สามารถอนุมานได้จากสัจพจน์

ตัวอย่างของระบบตรรกะคือเลขคณิตของ Peanoแบบจำลองมาตรฐานของเลขคณิตกำหนดโดเมนของการสนทนาให้เป็นจำนวนเต็มที่ไม่เป็นลบและให้สัญลักษณ์มีความหมายตามปกติ^{[ 10 ]}นอกจากนี้ยังมี แบบจำลอง เลขคณิต ที่ไม่เป็นมาตรฐาน อีกด้วย

ระบบตรรกศาสตร์ยุคแรก ได้แก่ ตรรกศาสตร์ของปาณินี ในอินเดีย ตรรกศาสตร์เชิงอนุมานของอริสโตเติล ตรรกศาสตร์เชิงประพจน์ของลัทธิสโตอิก และตรรกศาสตร์ของกงซุนหลง ในจีน (ประมาณ 325–250 ปีก่อนคริสตกาล) ในยุคต่อมา ผู้มีส่วนร่วมสำคัญ ได้แก่จอร์จ บูลออกัสตัส เดอ มอร์แกนและก็อตต์ล็อบ เฟรเกตรรกศาสตร์ทางคณิตศาสตร์ได้รับการพัฒนาในยุโรปช่วง ศตวรรษที่ 19

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

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

• Hunter, Geoffrey (1996) [1971]. Metalogic: An Introduction to the Metatheory of Standard First-Order Logic . สำนักพิมพ์มหาวิทยาลัยแคลิฟอร์เนีย (ตีพิมพ์ปี 1973). ISBN 9780520023567. OCLC  36312727 .( สามารถเข้าถึงได้สำหรับผู้ใช้บริการที่มีความบกพร่องทางการอ่าน )

• ฮอฟสตัดเตอร์, ดักลาส , 1979. เกอเดล, เอสเชอร์, บาค: สายใยทองคำนิรันดร์ ISBN 978-0-465-02656-2777 หน้า
• Kleene, Stephen C. , 1967. ตรรกศาสตร์ทางคณิตศาสตร์พิมพ์ซ้ำโดย Dover, 2002. ISBN 0-486-42533-9.
• Smullyan, Raymond M. , 1961. ทฤษฎีระบบเชิงรูปธรรม: วารสารการศึกษาคณิตศาสตร์สำนักพิมพ์มหาวิทยาลัยพรินซ์ตัน (1 เมษายน 1961), 156 หน้าISBN 0-691-08047-X.

ลองค้นหาคำว่า formalisationใน Wiktionary ซึ่งเป็นพจนานุกรมออนไลน์ฟรี

• สื่อที่เกี่ยวข้องกับระบบที่เป็นทางการในวิกิมีเดียคอมมอนส์
• สารานุกรมบริแทนนิกา, คำจำกัดความ ของระบบที่เป็นทางการ , 2007
• แดเนียล ริชาร์ดสัน, ระบบเชิงรูปธรรม, ตรรกศาสตร์ และความหมาย
• ระบบเชิงทางการที่PlanetMath
• สารานุกรมคณิตศาสตร์ระบบเชิงรูปธรรม
• ปีเตอร์ ซูเบอร์, ระบบเชิงรูปธรรมและเครื่องจักร: ไอโซมอร์ฟิซึม

เก็บถาวรเมื่อ 2011-05-24 ที่Wayback Machine , 917

• เรย์ ทาโอล, ระบบเชิงรูปธรรม
• ระบบที่เป็นทางการคืออะไร? เก็บถาวรเมื่อวันที่ 7 มิถุนายน 2011 ที่Wayback Machine : ข้อความบางส่วนจากหนังสือ "Artificial Intelligence: The Very Idea" (1985) ของ John Haugeland หน้า 48–64