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

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

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

ภาษาทางการสามารถกำหนดอย่างเป็นทางการได้ว่าเป็นเซตAของสตริง (ลำดับจำกัด) บนตัวอักษร α ที่กำหนดไว้ ผู้เขียนบางคน รวมถึงRudolf Carnapกำหนดภาษาเป็นคู่ลำดับ <α, A > ^{[ 3 ]} Carnap ยังกำหนดให้แต่ละองค์ประกอบของ α ต้องปรากฏในสตริงอย่างน้อยหนึ่งสตริงในAด้วย

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

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

ระบบที่เป็นทางการสามารถนิยามได้อย่างเป็นทางการว่าเป็นสามสิ่งเรียงลำดับ <α, , d> โดยที่d คือความสัมพันธ์ของการอนุมานโดยตรง ความสัมพันธ์นี้เข้าใจได้ในความหมาย ที่ครอบคลุม กล่าวคือ ประโยคพื้นฐานของระบบที่เป็นทางการนั้นถือว่าสามารถอนุมานได้ โดยตรง จากเซตว่างของประโยค การอนุมานโดยตรงเป็นความสัมพันธ์ระหว่างประโยคกับเซตจำกัดของประโยค ซึ่งอาจเป็นเซตว่างก็ได้ สัจพจน์ถูกเลือกเพื่อให้สมาชิกอันดับแรกของd ทุกตัวเป็นสมาชิกของและสมาชิกอันดับสองทุกตัวเป็นเซตย่อยจำกัดของ ${\displaystyle {\คณิตศาสตร์ {I}}}$${\displaystyle {\mathcal {D}}}$${\displaystyle {\mathcal {D}}}$${\displaystyle {\mathcal {D}}}$${\displaystyle {\คณิตศาสตร์ {I}}}$${\displaystyle {\คณิตศาสตร์ {I}}}$

ระบบที่เป็นทางการยังสามารถกำหนดได้ด้วยความสัมพันธ์d เท่านั้น โดยสามารถละเว้น α ในคำจำกัดความของภาษาที่เป็นทางการที่ตีความได้และระบบที่เป็นทางการที่ตีความได้อย่างไรก็ตาม วิธีนี้อาจเข้าใจและใช้งานได้ยากกว่า^{[ 3 ]}${\displaystyle {\mathcal {D}}}$${\displaystyle {\คณิตศาสตร์ {I}}}$

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

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

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

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

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

บทความนี้มีชื่อว่า "เมตาตรรกศาสตร์" (Metalogic) บทความนี้กล่าวถึงเมตาตรรกศาสตร์

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

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

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

ผลลัพธ์ที่สำคัญเกี่ยวกับความสมบูรณ์หรือความไม่สมบูรณ์ ได้แก่:

• ความสมบูรณ์ของตรรกะเชิงประพจน์ฟังก์ชัน ความจริง ( พอล เบอร์เนย์ส 1918) ^{[ 5 ]} (เอมิล โพสต์ 1920) ^{[ 2 ]}
• ความสมบูรณ์ของตรรกะภาคแสดงเอกภาคลำดับที่หนึ่ง (เลโอโปลด์ โลเวนไฮม์ 1915)
• ความสมบูรณ์ของ ตรรกศาสตร์ภาคแสดงลำดับที่หนึ่ง( ทฤษฎีบทความสมบูรณ์ของเกอเดลปี 1930)
• ทฤษฎีบทความไม่สมบูรณ์ข้อแรกของเกอเดลปี 1931
• ทฤษฎีบทความไม่สมบูรณ์ข้อที่สองของเกอเดลปี 1931

ผลลัพธ์ด้านความสอดคล้องที่สำคัญ ได้แก่:

• ความสอดคล้องของตรรกะเชิงประพจน์ ที่ทำหน้าที่ความจริง ( เอมิล โพสต์ 1920)
• ความสอดคล้องของ ตรรกะภาคแสดงเอกภาคลำดับที่หนึ่ง( เลโอโปลด์ โลเวนไฮม์ 1915)
• ความสอดคล้องของตรรกศาสตร์ภาคแสดงลำดับที่หนึ่ง ( เดวิด ฮิลเบิร์ตและวิลเฮล์ม แอคเคอร์มันน์ 1928)

ผลลัพธ์สำคัญด้านความสามารถในการตัดสินใจ ได้แก่:

• ความสามารถในการตัดสินใจของตรรกะเชิงประพจน์ฟังก์ชันความจริง (Emil Post 1920) ^{[ 2 ]}
• ความสามารถในการตัดสินใจของตรรกะภาคแสดงเอกภาคลำดับที่หนึ่ง (เลโอโปลด์ โลเวนไฮม์ 1915)
• ความไม่สามารถตัดสินได้ของตรรกะภาคแสดงลำดับที่หนึ่ง ( ทฤษฎีบทของเชิร์ชปี 1936)

ผลลัพธ์เชิงอภิปรัชญาที่สำคัญอื่นๆ ได้แก่:

• การมีอยู่ของแบบจำลองที่มีจำนวนสมาชิกอนันต์ตามอำเภอใจสำหรับทฤษฎีอันดับหนึ่งที่นับได้ซึ่งมีแบบจำลองอนันต์ ทฤษฎีบทโลเวนไฮม์-สโกเล็ม ( เลโอโปลด์ โลเวนไฮม์ 1915 และธอร์รัล์ฟ สโกเล็ม 1919)
• การพิสูจน์ทฤษฎีบทการกำจัดส่วนตัดสำหรับแคลคูลัสลำดับ ( บทความหลักของเกนท์เซนปี 1934)
• ทฤษฎีบทที่ไม่สามารถกำหนดได้ของ Tarski (Gödel และ Tarski ในช่วงทศวรรษที่ 1930)

• การเขียนโปรแกรมเชิงตรรกะขั้นสูง
• อภิคณิตศาสตร์

• สื่อที่เกี่ยวข้องกับMetalogicใน Wikimedia Commons
• Dragalin, AG (2001) [1994], "Meta-logic" , Encyclopedia of Mathematics , EMS Press