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

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

คำว่า "ลำดับที่หนึ่ง" ใช้เพื่อแยกความแตกต่างระหว่างตรรกะลำดับที่หนึ่งกับตรรกะลำดับที่สูงกว่าซึ่งมีภาคแสดงที่มีภาคแสดงหรือฟังก์ชันเป็นอาร์กิวเมนต์ หรือซึ่งอนุญาตให้มีการกำหนดปริมาณเหนือภาคแสดง ฟังก์ชัน หรือทั้งสองอย่าง^{[ 4 ] : 56} ในทฤษฎีลำดับที่หนึ่ง ภาคแสดงมักจะเกี่ยวข้องกับเซต ในทฤษฎีลำดับที่สูงกว่าที่ตีความได้ ภาคแสดงอาจถูกตีความว่าเป็นเซตของเซต

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

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

รากฐานของตรรกะลำดับที่หนึ่งได้รับการพัฒนาโดยอิสระโดยGottlob FregeและCharles Sanders Peirce [ ^{5 ] สำหรับ}ประวัติของตรรกะลำดับที่หนึ่งและวิธีที่มันเข้ามาครอบงำตรรกะเชิงรูปธรรม โปรดดู José Ferreirós (2001)

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

พิจารณาประโยคสองประโยคคือ “ โสกราตีสเป็นนักปรัชญา” และ “ เพลโตเป็นนักปรัชญา” ในตรรกศาสตร์เชิงประพจน์ประโยคเหล่านี้ถูกมองว่าเป็นบุคคลที่ศึกษา และอาจแสดงด้วยตัวแปร เช่นpและq เป็นต้น ประโยค เหล่านี้ไม่ได้ถูกมองว่าเป็นการประยุกต์ใช้ภาคแสดง เช่นกับวัตถุใดๆ ในขอบเขตของการสนทนา แต่ถูกมองว่าเป็นเพียงคำพูดที่อาจเป็นจริงหรือเท็จ^{[ 6 ]}อย่างไรก็ตาม ในตรรกศาสตร์ลำดับที่หนึ่ง ประโยคสองประโยคนี้อาจถูกกำหนดให้เป็นข้อความที่ระบุว่าบุคคลหรือวัตถุที่ไม่ใช่เชิงตรรกะบางอย่างมีคุณสมบัติ ในตัวอย่างนี้ ประโยคทั้งสองมีรูปแบบทั่วไปสำหรับบุคคลบางคนในประโยคแรก ค่าของตัวแปรxคือ “โสกราตีส” และในประโยคที่สองคือ “เพลโต” เนื่องจากความสามารถในการพูดถึงบุคคลที่ไม่ใช่เชิงตรรกะพร้อมกับตัวเชื่อมเชิงตรรกะดั้งเดิม ตรรกศาสตร์ลำดับที่หนึ่งจึงรวมถึงตรรกศาสตร์เชิงประพจน์ด้วย^{[ 7 ] : 29–30} ${\displaystyle {\text{คือนักปรัชญา}}}$${\displaystyle {\text{isPhilosopher}}(x)}$${\displaystyle x}$

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

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

การปฏิเสธประโยค "สำหรับทุกxถ้าxเป็นนักปรัชญาแล้วxก็เป็นนักวิชาการ" นั้น สมมูลทางตรรกะกับประโยค "มีอยู่xที่xเป็นนักปรัชญาและxไม่ใช่นักวิชาการ" ตัวบ่งชี้การมีอยู่ "มีอยู่" แสดงให้เห็นว่าข้อความ " xเป็นนักปรัชญาและxไม่ใช่นักวิชาการ" นั้นเป็นจริงสำหรับ x บางกรณี

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

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

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

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

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

โดยทั่วไปแล้ว สัญลักษณ์ของตัวอักษรจะแบ่งออกเป็นสัญลักษณ์เชิงตรรกะซึ่งมีความหมายเหมือนกันเสมอ และสัญลักษณ์ที่ไม่ใช่เชิงตรรกะซึ่งความหมายจะแตกต่างกันไปตามการตีความ^{[ 9 ]}ตัวอย่างเช่น สัญลักษณ์เชิงตรรกะจะแทน "และ" เสมอ จะไม่ถูกตีความว่าเป็น "หรือ" ซึ่งแทนด้วยสัญลักษณ์เชิงตรรกะอย่างไรก็ตาม สัญลักษณ์ภาคแสดงที่ไม่ใช่เชิงตรรกะ เช่น Phil( x ) อาจถูกตีความว่าหมายถึง " xเป็นนักปรัชญา" " xเป็นผู้ชายชื่อฟิลิป" หรือภาคแสดงเอกภาคอื่น ๆ ขึ้นอยู่กับการตีความในขณะนั้น ${\displaystyle \land }$${\displaystyle \lor }$

สัญลักษณ์ตรรกะคือชุดอักขระที่แตกต่างกันไปตามผู้เขียน แต่โดยทั่วไปจะประกอบด้วยสิ่งต่อไปนี้: ^{[ 10 ]}

• สัญลักษณ์ตัวบ่งปริมาณ : ∀สำหรับการบ่งปริมาณแบบสากลและ∃สำหรับการบ่งปริมาณแบบมีอยู่จริง
• ตัวเชื่อมตรรกะ : ∧สำหรับการเชื่อม , ∨สำหรับการแยก , →สำหรับการบ่งชี้ , ↔สำหรับเงื่อนไขสองทาง , ¬สำหรับการปฏิเสธ ผู้เขียนบางคน^{[ 11 ]}ใช้ C pqแทน→และ E pqแทน↔โดยเฉพาะในบริบทที่→ถูกใช้เพื่อวัตถุประสงค์อื่น ยิ่งไปกว่านั้น เกือกม้า⊃อาจใช้แทน→ได้^{[ 8 ]}ขีดสามเส้น≡อาจใช้แทน↔ ได้เครื่องหมายทิลเด ( ~ ), N pหรือ F pอาจใช้แทน¬ ได้เครื่องหมายขีดคู่, , ^{[ 12 ]}หรือ A pqอาจใช้แทน∨ ได้และเครื่องหมายแอมเปอร์แซนด์& , K pqหรือจุดกลาง⋅อาจใช้แทน∧ ได้ โดยเฉพาะหากไม่มีสัญลักษณ์เหล่านี้เนื่องจากเหตุผลทางเทคนิค${\displaystyle \|}$${\displaystyle +}$
• วงเล็บ วงเล็บเหลี่ยม และเครื่องหมายวรรคตอนอื่นๆ การเลือกใช้เครื่องหมายเหล่านี้แตกต่างกันไปตามบริบท
• เซตของตัวแปรอนันต์ซึ่งมักใช้ตัวอักษรพิมพ์เล็กที่อยู่ท้ายสุดของตัวอักษร เช่น_{x ,} y , z , ...โดยมักใช้ตัวห้อยเพื่อแยกแยะตัวแปร เช่นx₀ , x₁ , x₂ _, ...
• เครื่องหมายเท่ากับ (บางครั้งเรียกว่าเครื่องหมายเอกลักษณ์ ) = (ดูหัวข้อ § ความเท่าเทียมและสัจพจน์ด้านล่าง)

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

สัญลักษณ์ทางตรรกะอื่นๆ ได้แก่:

• ค่าคงที่ความจริง: T หรือ⊤สำหรับ "จริง" และ F หรือ⊥สำหรับ "เท็จ" เนื่องจากไม่มีตัวดำเนินการตรรกะใดที่มีค่าคงที่เท่ากับ 0 ค่าคงที่ทั้งสองนี้จึงสามารถแสดงได้โดยใช้ตัวบ่งปริมาณเท่านั้น
• ตัวเชื่อมตรรกะเพิ่มเติม เช่น เครื่องหมายSheffer stroke , D pq (NAND) และ ตัว เชื่อมOR พิเศษ , J pq

สัญลักษณ์ที่ไม่ใช่ตรรกะใช้แทน述语 (ความสัมพันธ์) ฟังก์ชัน และค่าคงที่ ในอดีต การใช้ชุดสัญลักษณ์ที่ไม่ใช่ตรรกะจำนวนอนันต์ที่กำหนดไว้ตายตัวสำหรับการใช้งานทุกวัตถุประสงค์ถือเป็นมาตรฐาน:

• สำหรับจำนวนเต็มn  ≥ 0 ทุกตัว จะมีชุดของสัญลักษณ์แสดงความสัมพันธ์แบบ n - ary หรือ n - place เนื่องจากสัญลักษณ์เหล่านี้แสดงความสัมพันธ์ระหว่าง องค์ประกอบ nตัว จึงเรียกอีกอย่างว่าสัญลักษณ์แสดงความสัมพันธ์สำหรับแต่ละค่า arity nจะมีสัญลักษณ์เหล่านี้อยู่เป็นจำนวนอนันต์:

  P ⁿ ₀ , P ⁿ ₁ , P ⁿ ₂ , P ⁿ ₃ , ...

• สำหรับจำนวนเต็มn  ≥ 0 ทุกตัว จะมีสัญลักษณ์ฟังก์ชัน n -ary อยู่เป็นจำนวนอนันต์ :

  f ⁿ ₀ , f ⁿ ₁ , f ⁿ ₂ , f ⁿ ₃ , ...

เมื่อความหมายของสัญลักษณ์กริยาหรือสัญลักษณ์ฟังก์ชันชัดเจนจากบริบทมักจะละเว้นตัว ยก n

ในแนวทางดั้งเดิมนี้ มีเพียงภาษาเดียวของตรรกะลำดับที่หนึ่ง^{[ 13 ]}แนวทางนี้ยังคงเป็นที่นิยม โดยเฉพาะในหนังสือที่เน้นปรัชญา

แนวทางปฏิบัติล่าสุดคือการใช้สัญลักษณ์ที่ไม่ใช่ตรรกะที่แตกต่างกันไปตามแอปพลิเคชันที่ต้องการใช้งาน ดังนั้นจึงจำเป็นต้องตั้งชื่อชุดของสัญลักษณ์ที่ไม่ใช่ตรรกะทั้งหมดที่ใช้ในแอปพลิเคชันเฉพาะ การเลือกนี้ทำผ่านลายเซ็น^{[ 14 ]}

ลายเซ็นทั่วไปในคณิตศาสตร์คือ {1, ×} หรือเพียงแค่ {×} สำหรับกลุ่ม [ ^{3 ]}หรือ {0, 1, +, ×, <} สำหรับฟิลด์เรียงลำดับไม่มีข้อจำกัดเกี่ยวกับจำนวนสัญลักษณ์ที่ไม่ใช่ตรรกะ ลายเซ็นอาจ^ว่างเปล่าจำกัด หรืออนันต์ หรือแม้แต่ไม่สามารถนับได้ ลายเซ็นที่ไม่สามารถนับได้เกิดขึ้นตัวอย่างเช่นในการพิสูจน์ ทฤษฎีบท Löwenheim–Skolemใน ยุคปัจจุบัน

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

ในแนวทางนี้ สัญลักษณ์ที่ไม่ใช่เชิงตรรกะทุกตัวจะเป็นประเภทใดประเภทหนึ่งต่อไปนี้:

• สัญลักษณ์แสดงภาคแสดง (หรือสัญลักษณ์แสดงความสัมพันธ์ ) ที่มีค่าความสัมพันธ์(หรือจำนวนอาร์กิวเมนต์) มากกว่าหรือเท่ากับ 0 โดยทั่วไปมักใช้ตัวอักษรพิมพ์ใหญ่ เช่นP , QและRตัวอย่าง:
  • ในP ( x ) นั้นPเป็นสัญลักษณ์ภาคแสดงที่มีระดับความสัมพันธ์ 1 การตีความที่เป็นไปได้ประการหนึ่งคือ " xเป็นผู้ชาย"
  • ในQ ( x , y ) นั้นQเป็นสัญลักษณ์ภาคแสดงที่มีระดับความสัมพันธ์ 2 การตีความที่เป็นไปได้ ได้แก่ " xมากกว่าy " และ " xเป็นพ่อของy "
  • ความสัมพันธ์ที่มีค่าความสัมพันธ์เป็น 0 สามารถระบุได้ด้วยตัวแปรเชิงประพจน์ซึ่งสามารถแทนข้อความใดๆ ก็ได้ การตีความที่เป็นไปได้ประการหนึ่งของRคือ "โสกราตีสเป็นผู้ชาย"
• สัญลักษณ์ฟังก์ชันที่มีค่าความนำไฟฟ้ามากกว่าหรือเท่ากับ 0 มักใช้ตัวอักษรโรมัน ตัวเล็ก เช่นf , gและhแทน ตัวอย่างเช่น:
  • f ( x ) อาจตีความได้ว่า "พ่อของx " ในทางเลขคณิตอาจหมายถึง "-x" ในทฤษฎีเซต อาจหมายถึง " เซตกำลังของ x"
  • ในทางเลขคณิตg ( x , y ) อาจหมายถึง " x + y " ส่วนในทฤษฎีเซต อาจหมายถึง "การรวมกันของxและy "
  • สัญลักษณ์ฟังก์ชันที่มีค่าคงที่เท่ากับ 0 เรียกว่าสัญลักษณ์ค่าคงที่และมักใช้ตัวอักษรพิมพ์เล็กที่ขึ้นต้นด้วยตัวพิมพ์ใหญ่ เช่นa , bและcสัญลักษณ์aอาจหมายถึงโสกราตีส ในทางเลขคณิต อาจหมายถึง 0 และในทฤษฎีเซต อาจหมายถึงเซตว่าง

แนวทางดั้งเดิมสามารถนำกลับมาใช้ในแนวทางสมัยใหม่ได้ โดยการระบุลายเซ็น "แบบกำหนดเอง" ให้ประกอบด้วยลำดับสัญลักษณ์ที่ไม่ใช่ตรรกะแบบดั้งเดิม

< index > ::= "" | < index > "'" < variable > ::= "x" < index > < constant > ::= "c" < index > < unary function > ::= "f1" < index > < binary function > ::= "f2" < index > < ternary function > ::= "f3" < index > < unary predicate > ::= "p1" < index > < binary predicate > ::= "p2" < index > < ternary predicate > ::= "p3" < index > < term > ::= < variable > | < constant > | < unary function > "(" < term > ")" | < ฟังก์ชันไบนารี> "(" < เทอม> "," < เทอม> ")" | < ฟังก์ชันไตรภาค> "(" < เทอม> "," < เทอม> "," < เทอม> ")" < สูตรอะตอม> ::= "จริง" | "เท็จ" | < เทอม> "=" < เทอม> | < เอกภาค> "(" < เทอม> ")" | < ตัวบ่งชี้ไบนารี> "(" < เทอม> "," < เทอม> ")" | < ternary predicate > "(" < term > "," < term > "," < term > ")" < formula > ::= < atomic formula > | "¬" < formula > | < formula > "∧" < formula > | < formula > "∨" < formula > | < formula > "⇒" < formula > | < formula > "⇔" < formula > | "(" < formula > ")" | "∀" < ตัวแปร> < สูตร> | "∃" < ตัวแปร> < สูตร>

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

ชุดของเงื่อนไข ได้ รับการกำหนดแบบอุปนัยตามกฎต่อไปนี้: ^{[ 17 ]}

1. ตัวแปรสัญลักษณ์ตัวแปรใดๆ ก็ตามถือเป็นเทอม
2. ฟังก์ชันถ้าfเป็น สัญลักษณ์ฟังก์ชัน n -ary และt ₁ , ..., t _nเป็นเทอมแล้วf ( t ₁ ,..., t _n ) ก็เป็นเทอมเช่นกัน โดยเฉพาะอย่างยิ่ง สัญลักษณ์ที่แทนค่าคงที่แต่ละตัวจะเป็นสัญลักษณ์ฟังก์ชัน nullary และดังนั้นจึงเป็นเทอมด้วย

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

ชุดของสูตร (เรียกอีกอย่างว่าสูตรที่มีรูปแบบดี^{[ 18 ]}หรือWFFs ) ถูกกำหนดแบบอุปนัยโดยกฎต่อไปนี้:

1. สัญลักษณ์ภาคแสดงถ้าPเป็น สัญลักษณ์ภาคแสดงแบบ n -ary และt ₁ , ..., t _nเป็นเทอมแล้วP ( t ₁ ,..., t _n ) จะเป็นสูตร
   • ความเท่าเทียมกันหากถือว่าสัญลักษณ์ความเท่าเทียมกันเป็นส่วนหนึ่งของตรรกะ และ t ₁กับ t ₂เป็นพจน์แล้ว t ₁ = t ₂ก็คือสูตร
2. การปฏิเสธถ้าเป็นสูตร แล้ว ก็เป็นสูตรเช่นกัน${\displaystyle \varphi }$${\displaystyle \lnot \varphi }$
3. ตัวเชื่อมตรรกะไบนารีถ้า⁠ ⁠${\displaystyle \varphi }$และ⁠ ⁠${\displaystyle \psi }$เป็นสูตรแล้ว ( ) ก็เป็นสูตรเช่นกัน กฎที่คล้ายกันนี้ใช้กับตัวเชื่อมตรรกะไบนารีอื่นๆ ด้วย${\displaystyle \varphi \rightarrow \psi }$
4. ตัวบ่งปริมาณถ้า เป็นสูตร และxเป็นตัวแปร แล้ว(สำหรับทุก x จะเป็นจริง) และ(มี x อยู่จริงที่ทำให้) เป็นสูตร${\displaystyle \varphi }$${\displaystyle \forall x\varphi }$${\displaystyle \varphi }$${\displaystyle \exists x\varphi }$${\displaystyle \varphi }$

สูตรคือสูตรที่ได้จากการใช้กฎข้อ 1–4 เพียงจำนวนจำกัดเท่านั้น สูตรที่ได้จากกฎข้อแรกเรียกว่าสูตรอะตอมิก

ตัวอย่างเช่น:

${\displaystyle \forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))}$

เป็นสูตร ถ้าfเป็นสัญลักษณ์ฟังก์ชันเอกภาคPเป็นสัญลักษณ์述语เอกภาค และ Q เป็นสัญลักษณ์述语ไตรภาค อย่างไรก็ตามไม่ใช่สูตร แม้ว่าจะเป็นสตริงของสัญลักษณ์จากตัวอักษรก็ตาม ${\displaystyle \forall x\,x\rightarrow }$

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

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

• ${\displaystyle \lnot }$ได้รับการประเมินก่อน
• ${\displaystyle \land }$และจะได้รับการประเมินต่อไป${\displaystyle \lor }$
• ตัวบ่งชี้ปริมาณจะได้รับการประเมินต่อไป
• ${\displaystyle \to }$และจะได้รับการประเมินเป็นลำดับสุดท้าย${\displaystyle \leftrightarrow }$

นอกจากนี้ อาจมีการแทรกเครื่องหมายวรรคตอนเพิ่มเติมที่ไม่จำเป็นตามคำจำกัดความ เพื่อให้สูตรอ่านง่ายขึ้น ดังนั้นสูตรจึงเป็นดังนี้:

${\displaystyle \lnot \forall xP(x)\to \exists x\lnot P(x)}$

อาจเขียนได้ดังนี้:

${\displaystyle (\lnot [\forall xP(x)])\to \exists x[\lnot P(x)].}$

ในสูตร ตัวแปรอาจปรากฏแบบอิสระหรือแบบมีเงื่อนไข (หรือทั้งสองอย่าง) การกำหนดรูปแบบอย่างเป็นทางการของแนวคิดนี้มาจาก Quine โดยเริ่มจากการกำหนดแนวคิดของการปรากฏของตัวแปร จากนั้นจึงพิจารณาว่าการปรากฏของตัวแปรนั้นเป็นอิสระหรือแบบมีเงื่อนไข และสุดท้ายพิจารณาว่าสัญลักษณ์ตัวแปรโดยรวมเป็นอิสระหรือแบบมีเงื่อนไข เพื่อแยกแยะการปรากฏที่แตกต่างกันของสัญลักษณ์x ที่เหมือนกัน การปรากฏแต่ละครั้งของสัญลักษณ์ตัวแปรxในสูตร φ จะถูกระบุด้วยสตริงย่อยเริ่มต้นของ φ จนถึงจุดที่สัญลักษณ์x ดังกล่าว ปรากฏ^{[ 8 ]หน้า 297}จากนั้น การปรากฏของxจะเรียกว่ามีเงื่อนไขหากการปรากฏของx นั้น อยู่ภายในขอบเขตของอย่างน้อยหนึ่งอย่างใดอย่างหนึ่งสุดท้ายx จะมีเงื่อนไขใน φ หากการปรากฏทั้งหมดของxใน φ มีเงื่อนไข^{[ 8 ]หน้า 142–143}${\displaystyle \exists x}$${\displaystyle \forall x}$

โดยสัญชาตญาณ สัญลักษณ์ตัวแปรจะเป็นอิสระในสูตรหากไม่มีการกำหนดปริมาณที่จุดใดเลย: ^{[ 8 ]หน้า 142–143}ใน∀ y P ( x , y )การปรากฏเพียงครั้งเดียวของตัวแปรxเป็นอิสระ ในขณะที่การปรากฏของyถูกผูกไว้ การปรากฏของตัวแปรอิสระและถูกผูกไว้ในสูตรจะถูกกำหนดโดยการอุปนัยดังต่อไปนี้

สูตรอะตอม

ถ้าφเป็นสูตรอะตอมิกแล้วxจะปรากฏอย่างอิสระในφก็ต่อเมื่อxปรากฏในφ เท่านั้น ยิ่งไปกว่านั้น ไม่มีตัวแปรผูกมัดในสูตรอะตอมิกใดๆ

การปฏิเสธ

xปรากฏอย่างอิสระใน ¬ φก็ต่อเมื่อxปรากฏอย่างอิสระในφเท่านั้นxปรากฏอย่างถูกผูกมัดใน ¬ φก็ต่อเมื่อxปรากฏอย่างถูกผูกมัดในφ เท่านั้น

ตัวเชื่อมไบนารี

xปรากฏอย่างอิสระใน ( φ → ψ ) ก็ต่อเมื่อxปรากฏอย่างอิสระในφหรือψเท่านั้นxปรากฏอย่างถูกผูกไว้ใน ( φ → ψ ) ก็ต่อเมื่อxปรากฏอย่างถูกผูกไว้ในφหรือψเท่านั้น กฎเดียวกันนี้ใช้ได้กับตัวเชื่อมไบนารีอื่นๆ ที่ใช้แทน →

ตัวบ่งปริมาณ

xปรากฏอย่างอิสระใน∀ y φก็ต่อเมื่อ x ปรากฏอย่างอิสระในφและxเป็นสัญลักษณ์ที่แตกต่างจากyนอกจากนี้xปรากฏแบบผูกติดใน∀ y φก็ต่อเมื่อxคือyหรือxปรากฏแบบผูกติดในφกฎเดียวกันนี้ใช้ได้กับ∃แทน∀ด้วย

ตัวอย่างเช่น ใน∀ x ∀ y ( P ( x ) → Q ( x , f ( x ), z )) x และyปรากฏเฉพาะในรูปแบบผูกพัน^{[ 19 ]} zปรากฏเฉพาะในรูปแบบอิสระ และwไม่ใช่ทั้งสองอย่างเพราะไม่ปรากฏใน สูตร

ตัวแปรอิสระและตัวแปรที่ถูกผูกไว้ในสูตรไม่จำเป็นต้องเป็นเซตที่ไม่ทับซ้อนกัน: ในสูตรP ( x ) → ∀ x Q ( x )การปรากฏครั้งแรกของxในฐานะอาร์กิวเมนต์ของPเป็นตัวแปรอิสระ ในขณะที่การปรากฏครั้งที่สอง ในฐานะอาร์กิวเมนต์ของQเป็นตัวแปรที่ถูกผูกไว้

สูตรในตรรกศาสตร์ลำดับที่หนึ่งที่ไม่มีตัวแปรอิสระปรากฏ เรียกว่าประโยคลำดับที่หนึ่งสูตรเหล่านี้จะมีค่าความจริง ที่กำหนดไว้อย่างชัดเจน ภายใต้การตีความ ตัวอย่างเช่น ความจริงของสูตรเช่น Phil( x ) ขึ้นอยู่กับว่าxแทนอะไร แต่ประโยค∃x Phil ( x )จะเป็นจริงหรือเท็จในการตีความที่กำหนด

ในทางคณิตศาสตร์ ภาษาของกลุ่มอาเบเลียน เรียงลำดับ มีสัญลักษณ์ค่าคงที่ 0 หนึ่งตัว สัญลักษณ์ฟังก์ชันเอกภาค − หนึ่งตัว สัญลักษณ์ฟังก์ชันทวิภาค + หนึ่งตัว และสัญลักษณ์ความสัมพันธ์ทวิภาค ≤ หนึ่งตัว ดังนั้น:

• นิพจน์ +( x , y ) และ +( x , +( y , −( z ))) เป็นเทอมโดยทั่วไปจะเขียนในรูปx + yและx + y − z
• นิพจน์ +( x , y ) = 0 และ ≤(+( x , +( y , −( z ))), +( x , y )) เป็นสูตรอะตอมิกซึ่งโดยทั่วไปจะเขียนในรูปx + y = 0 และx + y − z  ≤  x + y
• นิพจน์นี้เป็นสูตรซึ่งโดยปกติจะเขียนในรูปสูตรนี้มีตัวแปรอิสระหนึ่งตัวคือz${\displaystyle (\forall x\forall y\,[\mathop {\leq } (\mathop {+} (x,y),z)\to \forall x\,\forall y\,\mathop {+} (x,y)=0)]}$${\displaystyle \forall x\forall y(x+y\leq z)\to \forall x\forall y(x+y=0).}$

สัจพจน์สำหรับกลุ่มอาเบเลียนเรียงลำดับสามารถแสดงได้ในรูปของชุดประโยคในภาษานั้น ตัวอย่างเช่น สัจพจน์ที่ระบุว่ากลุ่มนั้นเป็นกลุ่มสลับที่ได้ มักจะเขียนว่า${\displaystyle (\forall x)(\forall y)[x+y=y+x].}$

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

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

ขอบเขตของการสนทนาDคือเซตที่ไม่ว่างเปล่าของ "วัตถุ" บางชนิด ตามสัญชาตญาณแล้ว เมื่อกำหนดการตีความ สูตรลำดับที่หนึ่งจะกลายเป็นข้อความเกี่ยวกับวัตถุเหล่านี้ ตัวอย่างเช่นระบุการมีอยู่ของวัตถุบางอย่างในDซึ่ง述语Pเป็นจริง (หรือกล่าวให้แม่นยำยิ่งขึ้นคือ ซึ่ง述语ที่กำหนดให้กับสัญลักษณ์述语Pโดยการตีความนั้นเป็นจริง) ตัวอย่างเช่น เราสามารถกำหนดให้Dเป็นเซตของจำนวนเต็มได้ ${\displaystyle \exists xP(x)}$

สัญลักษณ์ที่ไม่ใช่เชิงตรรกะจะถูกตีความดังนี้:

• การตีความ สัญลักษณ์ฟังก์ชัน n- ary คือฟังก์ชันจากDnไปยัง^Dnตัวอย่างเช่น ถ้าโดเมนของการพิจารณาคือเซตของจำนวนเต็ม สัญลักษณ์ฟังก์ชันfที่มี arity 2 สามารถตีความได้ว่าเป็นฟังก์ชันที่ให้ผลรวมของอาร์กิวเมนต์ กล่าวอีกนัยหนึ่ง สัญลักษณ์fเกี่ยวข้องกับฟังก์ชันซึ่งใน${\displaystyle I(f)}$การตีความนี้คือการบวก
• ^{การตีความสัญลักษณ์ค่าคงที่ (สัญลักษณ์ฟังก์ชันที่มีอาร์กิวเมนต์เป็น 0} ) คือฟังก์ชันจากD₀ (เซตที่มีสมาชิกเพียงตัวเดียวคือทูเปิล ว่าง ) ไปยังDซึ่งสามารถระบุได้ง่ายๆ ด้วยวัตถุในDตัวอย่างเช่น การตีความอาจกำหนดค่าให้กับสัญลักษณ์ค่าคงที่${\displaystyle I(c)=10}$${\displaystyle c}$
• การตีความสัญลักษณ์述語แบบn -ary คือเซตของn -tuple ขององค์ประกอบในDซึ่งให้ค่าอาร์กิวเมนต์ที่ทำให้述語เป็นจริง ตัวอย่างเช่น การตีความสัญลักษณ์述語แบบไบนารีPอาจเป็นเซตของคู่จำนวนเต็มที่จำนวนแรกน้อยกว่าจำนวนที่สอง ตามการตีความนี้ 述語Pจะเป็นจริงก็ต่อเมื่ออาร์กิวเมนต์ตัวแรกน้อยกว่าอาร์กิวเมนต์ตัวที่สอง หรืออาจกำหนดฟังก์ชันค่าบูลีนจากD ⁿไปยังn ให้กับสัญลักษณ์述語ได้เช่นกัน${\displaystyle I(P)}$${\displaystyle \{\mathrm {true,false} \}}$

สูตรจะให้ค่าเป็นจริงหรือเท็จ โดยขึ้นอยู่กับการตีความและการกำหนดค่าตัวแปร μ ซึ่งเชื่อมโยงองค์ประกอบของโดเมนการสนทนากับตัวแปรแต่ละตัว เหตุผลที่ต้องมีการกำหนดค่าตัวแปรก็เพื่อให้ความหมายแก่สูตรที่มีตัวแปรอิสระ เช่นค่าความจริงของสูตรนี้จะเปลี่ยนแปลงไปตามค่าที่xและyแทน ${\displaystyle y=x}$

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

• ตัวแปร . ตัวแปรแต่ละตัวxจะมีค่าเป็นμ ( x )
• ฟังก์ชัน . เมื่อกำหนดเทอมที่ได้รับการประเมินค่าเป็นองค์ประกอบของโดเมนของการสนทนา และสัญลักษณ์ฟังก์ชันn -ary fเทอมนั้นจะประเมินค่าเป็น.${\displaystyle t_{1},\ldots ,t_{n}}$${\displaystyle d_{1},\ldots ,d_{n}}$${\displaystyle f(t_{1},\ldots ,t_{n})}$${\displaystyle (I(f))(d_{1},\ldots ,d_{n})}$

ถัดไป แต่ละสูตรจะได้รับการกำหนดค่าความจริง นิยามอุปนัยที่ใช้ในการกำหนดค่านี้เรียกว่าT- schema

• สูตรอะตอม (1)สูตรจะเชื่อมโยงค่าจริงหรือเท็จขึ้นอยู่กับว่า โดยที่คือการประเมินเงื่อนไขและคือการตีความซึ่งตามสมมติฐานคือเซตย่อยของ${\displaystyle P(t_{1},\ldots ,t_{n})}$${\displaystyle \langle v_{1},\ldots ,v_{n}\rangle \in I(P)}$${\displaystyle v_{1},\ldots ,v_{n}}$${\displaystyle t_{1},\ldots ,t_{n}}$${\displaystyle I(P)}$${\displaystyle P}$${\displaystyle D^{n}}$
• สูตรอะตอม (2)สูตรจะถูกกำหนดให้เป็นจริงก็ต่อเมื่อและประเมินค่าเป็นวัตถุเดียวกันของโดเมนของการสนทนา (ดูส่วนเกี่ยวกับความเท่าเทียมกันด้านล่าง)${\displaystyle t_{1}=t_{2}}$${\displaystyle t_{1}}$${\displaystyle t_{2}}$
• ตัวเชื่อมทางตรรกะสูตรในรูปแบบ, , เป็นต้น จะถูกประเมินตามตารางค่าความจริงของตัวเชื่อมนั้นๆ เช่นเดียวกับในตรรกศาสตร์เชิงประพจน์${\displaystyle \neg \varphi }$${\displaystyle \varphi \rightarrow \psi }$
• ตัวบ่งปริมาณเชิงการมีอยู่สูตรจะเป็นจริงตามMก็ต่อเมื่อมีการประเมินค่าตัวแปรที่แตกต่างจาก ค่า xไม่เกิน โดยที่ φ เป็นจริงตามการตีความMและการกำหนดค่าตัวแปรนิยามอย่างเป็นทางการนี้แสดงให้เห็นถึงแนวคิดที่ว่าเป็นจริงก็ต่อเมื่อมีวิธีเลือกค่าxที่ทำให้ φ( x ) เป็นจริง${\displaystyle \exists x\varphi (x)}$${\displaystyle \mu }$${\displaystyle \mu '}$${\displaystyle \mu }$${\displaystyle \mu '}$${\displaystyle \exists x\varphi (x)}$
• ตัวบ่งปริมาณสากลสูตรจะเป็นจริงตามMและถ้า φ( x ) เป็นจริงสำหรับทุกคู่ที่ประกอบขึ้นจากการตีความMและการกำหนดค่าตัวแปรบางอย่างที่แตกต่างกันไม่เกินค่าของxนี่คือแนวคิดที่ว่าเป็นจริงก็ต่อเมื่อทุกตัวเลือกที่เป็นไปได้ของค่าxทำให้ φ( x ) เป็นจริง${\displaystyle \forall x\varphi (x)}$${\displaystyle \mu }$${\displaystyle \mu '}$${\displaystyle \mu }$${\displaystyle \forall x\varphi (x)}$

ถ้าสูตรไม่มีตัวแปรอิสระ และดังนั้นจึงเป็นประโยค การกำหนดค่าตัวแปรเริ่มต้นจะไม่ส่งผลต่อค่าความจริงของสูตรนั้น กล่าวอีกนัยหนึ่ง ประโยคจะเป็นจริงตามเงื่อนไขMก็ต่อเมื่อเป็นจริงตามเงื่อนไขMและการกำหนดค่าตัวแปรอื่นๆ ทุกค่า ${\displaystyle \mu }$${\displaystyle \mu '}$

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

• ตัวบ่งปริมาณเชิงการมีอยู่ (ทางเลือก)สูตรจะเป็นจริงตามMถ้ามีd บางตัว ในโดเมนของการสนทนาที่ทำให้เป็นจริง นี่คือผลลัพธ์ของการแทนที่ c _dสำหรับทุกการปรากฏอิสระของxใน φ${\displaystyle \exists x\varphi (x)}$${\displaystyle \varphi (c_{d})}$${\displaystyle \varphi (c_{d})}$
• ตัวบ่งปริมาณสากล (ทางเลือก)สูตรจะเป็นจริงตามMถ้าสำหรับทุกdในขอบเขตของการสนทนา สูตร นั้นจะเป็นจริงตามM${\displaystyle \forall x\varphi (x)}$${\displaystyle \varphi (c_{d})}$

วิธีการทางเลือกนี้ให้ค่าความจริงที่เหมือนกันทุกประการแก่ทุกประโยคเช่นเดียวกับวิธีการกำหนดค่าตัวแปร

ถ้าประโยค φ มีค่าเป็นจริงภายใต้การตีความM ที่กำหนด เราจะกล่าวว่าM สอดคล้องกับ φ ซึ่งแสดงด้วย^{[ 20 ]} ประโยคหนึ่งๆ สามารถทำให้เป็นจริงได้ก็ต่อเมื่อมีการตีความบางอย่างที่ทำให้ประโยคนั้นเป็นจริง ซึ่งแตกต่างเล็กน้อยจากสัญลักษณ์จากทฤษฎีแบบจำลอง โดยที่แสดงถึงความสามารถในการทำให้เป็นจริงในแบบจำลอง กล่าวคือ "มีการกำหนดค่าที่เหมาะสมในโดเมนของ ให้กับสัญลักษณ์ตัวแปรของ" ^{[ 21 ]}${\displaystyle M\vDash \varphi }$${\displaystyle \vDash }$${\displaystyle M\vDash \phi }$${\displaystyle M}$${\displaystyle \phi }$

ความสามารถในการทำให้สูตรที่มีตัวแปรอิสระเป็นจริงนั้นซับซ้อนกว่า เพราะการตีความเพียงอย่างเดียวไม่สามารถกำหนดค่าความจริงของสูตรดังกล่าวได้ ธรรมเนียมปฏิบัติที่ใช้กันทั่วไปคือ สูตร φ ที่มีตัวแปรอิสระ, ..., จะถือว่าเป็นจริงโดยการตีความ หากสูตร φ ยังคงเป็นจริงไม่ว่าบุคคลใดจากโดเมนของการสนทนาจะถูกกำหนดให้กับตัวแปรอิสระ, ... , ซึ่งมีผลเช่นเดียวกับการกล่าวว่าสูตร φ เป็นจริงก็ต่อเมื่อการปิดแบบสากล ของสูตรนั้น เป็นจริง ${\displaystyle x_{1}}$${\displaystyle x_{n}}$${\displaystyle x_{1}}$${\displaystyle x_{n}}$${\displaystyle \forall x_{1}\dots \forall x_{n}\phi (x_{1},\dots ,x_{n})}$

สูตรจะถือว่าถูกต้องตามหลักตรรกะ (หรือถูกต้อง ตามหลักตรรกะ ) หากสูตรนั้นเป็นจริงในทุกการตีความ^{[ 22 ]}สูตรเหล่านี้มีบทบาทคล้ายกับสัจพจน์ในตรรกะเชิงประพจน์

สูตร φ เป็นผลลัพธ์เชิงตรรกะของสูตร ψ ก็ต่อเมื่อการตีความทุกอย่างที่ทำให้ ψ เป็นจริง ก็ทำให้ φ เป็นจริงด้วย ในกรณีนี้กล่าวได้ว่า φ เป็นผลลัพธ์เชิงตรรกะที่ได้จาก ψ

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

• พีชคณิตทรงกระบอกโดยAlfred Tarskiและคณะ;
• พีชคณิตหลายเหลี่ยมโดยPaul Halmos ;
• ตรรกศาสตร์ฟังก์ชันภาคแสดง (Predicate functor logic ) โดยหลักแล้วเป็นผลงานของวิลลาร์ด ไควน์

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

Tarski และ Givant (1987) แสดงให้เห็นว่าเศษส่วนของตรรกะลำดับแรกที่ไม่มีประโยคอะตอมิกที่อยู่ในขอบเขตของตัวบ่งปริมาณมากกว่าสามตัวนั้นมีพลังการแสดงออกเท่ากับพีชคณิตความสัมพันธ์ [ ^{23 ] : 32–33} เศษส่วนนี้มีความน่าสนใจอย่างมากเพราะเพียงพอสำหรับเลขคณิตของ Peanoและทฤษฎีเซตเชิงสัจพจน์ ส่วนใหญ่ รวมถึงทฤษฎีเซต Zermelo–Fraenkel (ZFC) ที่เป็นมาตรฐาน พวกเขายังพิสูจน์ว่าตรรกะลำดับแรกที่มีคู่ลำดับ ดั้งเดิม เทียบเท่ากับพีชคณิตความสัมพันธ์ที่มีฟังก์ชันการฉายภาพ คู่ลำดับสอง ฟังก์ชัน^{[ 24 ] : 803}

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

โครงสร้างลำดับแรกที่สอดคล้องกับประโยคทั้งหมดในทฤษฎีที่กำหนด เรียกว่าแบบจำลองของทฤษฎีนั้นชั้นพื้นฐานคือ เซตของโครงสร้างทั้งหมดที่สอดคล้องกับทฤษฎีเฉพาะนั้น ชั้นเหล่านี้เป็นหัวข้อหลักในการศึกษาทฤษฎีแบบจำลอง

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

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

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

อย่างไรก็ตาม โดเมนที่ว่างเปล่ามีปัญหาอยู่หลายประการ:

• กฎการอนุมานทั่วไปหลายข้อใช้ได้เฉพาะเมื่อโดเมนของการพิจารณาต้องไม่ว่างเปล่า ตัวอย่างเช่น กฎที่ระบุว่าหมายความ ว่า เมื่อxไม่ใช่ตัวแปรอิสระในกฎนี้ซึ่งใช้ในการแปลงสูตรให้อยู่ในรูปแบบปกติ prenexนั้นถูกต้องในโดเมนที่ไม่ว่างเปล่า แต่ไม่ถูกต้องหากอนุญาตให้โดเมนว่างเปล่าได้${\displaystyle \varphi \lor \exists x\psi }$${\displaystyle \exists x(\varphi \lor \psi )}$${\displaystyle \varphi }$
• นิยามของความจริงในการตีความที่ใช้ฟังก์ชันการกำหนดค่าตัวแปรนั้นใช้ไม่ได้กับโดเมนว่าง เพราะไม่มีฟังก์ชันการกำหนดค่าตัวแปรใดที่มีช่วงค่าว่าง (ในทำนองเดียวกัน เราไม่สามารถกำหนดการตีความให้กับสัญลักษณ์คงที่ได้) นิยามความจริงนี้กำหนดให้เราต้องเลือกฟังก์ชันการกำหนดค่าตัวแปร (μ ข้างต้น) ก่อนที่จะสามารถกำหนดค่าความจริงสำหรับสูตรอะตอมได้ แม้กระทั่งสูตรอะตอม จากนั้นค่าความจริงของประโยคจะถูกกำหนดให้เป็นค่าความจริงภายใต้การกำหนดค่าตัวแปรใดๆ และพิสูจน์ได้ว่าค่าความจริงนี้ไม่ขึ้นอยู่กับการเลือกการกำหนดค่าใด เทคนิคนี้ใช้ไม่ได้หากไม่มีฟังก์ชันการกำหนดค่าเลย ต้องเปลี่ยนแปลงเพื่อรองรับโดเมนว่าง

ดังนั้น เมื่ออนุญาตให้ใช้โดเมนว่างได้ มักจะต้องถือว่าเป็นกรณีพิเศษ อย่างไรก็ตาม ผู้เขียนส่วนใหญ่มักจะยกเว้นโดเมนว่างโดยนิยามอยู่แล้ว

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

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

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

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

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

ตัวอย่างเช่น กฎการอนุมานที่ใช้กันทั่วไปอย่างหนึ่งคือกฎการแทนที่ถ้าtเป็นพจน์ และ φ เป็นสูตรที่อาจมีตัวแปรxแล้ว φ[ t / x ] คือผลลัพธ์ของการแทนที่ตัวแปรx ที่เป็นอิสระทั้งหมด ด้วยtใน φ กฎการแทนที่ระบุว่า สำหรับ φ ใดๆ และพจน์t ใดๆ เราสามารถสรุป φ[ t / x ] จาก φ ได้ โดยมีเงื่อนไขว่าไม่มีตัวแปรอิสระของtตัวใดถูกผูกไว้ในระหว่างกระบวนการแทนที่ (ถ้าตัวแปรอิสระของt บางตัว ถูกผูกไว้ ในการแทนที่tด้วยxนั้น จำเป็นต้องเปลี่ยนตัวแปรที่ถูกผูกไว้ของ φ ให้แตกต่างจากตัวแปรอิสระของt ก่อน )

เพื่อให้เข้าใจว่าทำไมข้อจำกัดเกี่ยวกับตัวแปรที่ถูกผูกไว้จึงจำเป็น ลองพิจารณาสูตร φ ที่ถูกต้องตามหลักตรรกะซึ่งกำหนดโดยในรูปแบบ (0,1,+,×,=) ของเลขคณิต ถ้าtคือพจน์ "x + 1" สูตร φ[ t / y ] คือซึ่งจะเป็นเท็จในหลายๆ การตีความ ปัญหาคือตัวแปรอิสระxของtกลายเป็นตัวแปรที่ถูกผูกไว้ในระหว่างการแทนที่ การแทนที่ที่ต้องการสามารถทำได้โดยการเปลี่ยนชื่อตัวแปรที่ถูกผูกไว้xของ φ เป็นอย่างอื่น เช่นzเพื่อให้สูตรหลังจากการแทนที่คือซึ่งถูกต้องตามหลักตรรกะอีกครั้ง ${\displaystyle \exists x(x=y)}$${\displaystyle \exists x(x=x+1)}$${\displaystyle \exists z(z=x+1)}$

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

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

ระบบการอนุมานเชิงธรรมชาติคล้ายกับระบบแบบฮิลเบิร์ตตรงที่การอนุมานเป็นรายการสูตรที่มีจำนวนจำกัด อย่างไรก็ตาม ระบบการอนุมานเชิงธรรมชาติไม่มีสัจพจน์ทางตรรกะ แต่ชดเชยด้วยการเพิ่มกฎการอนุมานเพิ่มเติมที่สามารถใช้ในการจัดการตัวเชื่อมทางตรรกะในสูตรในบทพิสูจน์ได้

แคลคูลัสลำดับถูกพัฒนาขึ้นเพื่อศึกษาคุณสมบัติของระบบการอนุมานตามธรรมชาติ^{[ 25 ]}แทนที่จะทำงานกับสูตรทีละสูตร จะใช้ลำดับซึ่งเป็นนิพจน์ในรูปแบบ:

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},}$

โดยที่ A ₁ , ..., A _n , B ₁ , ..., B _kเป็นสูตร และสัญลักษณ์ประตูหมุนใช้เป็นเครื่องหมายวรรคตอนเพื่อแยกสองส่วนออกจากกัน ตามสัญชาตญาณแล้ว ลำดับแสดงถึงแนวคิดที่บ่งบอกว่า ${\displaystyle \vdash }$${\displaystyle (A_{1}\land \cdots \land A_{n})}$${\displaystyle (B_{1}\lor \cdots \lor B_{k})}$

แตกต่างจากวิธีการที่กล่าวมาข้างต้น การพิสูจน์ในวิธีการแบบตาราง (tableaux method) ไม่ใช่รายการของสูตร แต่เป็นการพิสูจน์เป็นโครงสร้างแบบต้นไม้ของสูตร เพื่อแสดงว่าสูตร A สามารถพิสูจน์ได้ วิธีการแบบตารางจะพยายามแสดงให้เห็นว่านิเสธของ A นั้นไม่สามารถทำให้เป็นจริงได้ โครงสร้างแบบต้นไม้ของการพิสูจน์มีรากอยู่ที่จุดหนึ่ง และแตกแขนงออกไปในลักษณะที่สะท้อนโครงสร้างของสูตร ตัวอย่างเช่น การแสดงว่าไม่สามารถทำให้เป็นจริงได้นั้น จำเป็นต้องแสดงว่า C และ D ต่างก็ไม่สามารถทำให้เป็นจริงได้เช่นกัน ซึ่งสอดคล้องกับจุดแตกแขนงในต้นไม้ที่มีC และ D เป็น ตัวแปรหลักและตัวแปรย่อย${\displaystyle \lnot A}$${\displaystyle C\lor D}$${\displaystyle C\lor D}$

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

วิธีการแก้ปัญหาใช้ได้เฉพาะกับสูตรที่เป็นผลรวมของสูตรอะตอมเท่านั้น สูตรใดๆ ก็ตามจะต้องถูกแปลงให้อยู่ในรูปแบบนี้ก่อนโดยใช้กระบวนการสโกเลไมเซชันกฎการแก้ปัญหาบอกว่าจากสมมติฐานและข้อสรุปสามารถหาได้ ${\displaystyle A_{1}\lor \cdots \lor A_{k}\lor C}$${\displaystyle B_{1}\lor \cdots \lor B_{l}\lor \lnot C}$${\displaystyle A_{1}\lor \cdots \lor A_{k}\lor B_{1}\lor \cdots \lor B_{l}}$

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

${\displaystyle \lnot \forall x\,P(x)\Leftrightarrow \exists x\,\lnot P(x)}$

${\displaystyle \lnot \exists x\,P(x)\Leftrightarrow \forall x\,\lnot P(x)}$

${\displaystyle \forall x\,\forall y\,P(x,y)\Leftrightarrow \forall y\,\forall x\,P(x,y)}$

${\displaystyle \exists x\,\exists y\,P(x,y)\Leftrightarrow \exists y\,\exists x\,P(x,y)}$

${\displaystyle \forall x\,P(x)\land \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\land Q(x))}$

${\displaystyle \exists x\,P(x)\lor \exists x\,Q(x)\Leftrightarrow \exists x\,(P(x)\lor Q(x))}$

${\displaystyle P\land \exists x\,Q(x)\Leftrightarrow \exists x\,(P\land Q(x))}$(ซึ่งต้องไม่เกิดขึ้นโดยอิสระใน)${\displaystyle x}$${\displaystyle P}$

${\displaystyle P\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P\lor Q(x))}$(ซึ่งต้องไม่เกิดขึ้นโดยอิสระใน)${\displaystyle x}$${\displaystyle P}$

มีธรรมเนียมปฏิบัติที่แตกต่างกันหลายประการสำหรับการใช้ความเท่าเทียมกัน (หรือเอกลักษณ์) ในตรรกะลำดับที่หนึ่ง ธรรมเนียมปฏิบัติที่พบได้บ่อยที่สุด ซึ่งเรียกว่าตรรกะลำดับที่หนึ่งที่มีความเท่าเทียมกันนั้น รวมถึงสัญลักษณ์ความเท่าเทียมกันเป็นสัญลักษณ์ตรรกะพื้นฐานซึ่งจะถูกตีความเสมอว่าเป็นความสัมพันธ์ความเท่าเทียมกันที่แท้จริงระหว่างสมาชิกของโดเมนของการสนทนา โดยที่สมาชิก "สอง" ตัวที่กำหนดนั้นเป็นสมาชิกเดียวกัน แนวทางนี้ยังเพิ่มสัจพจน์บางประการเกี่ยวกับความเท่าเทียมกันให้กับระบบการอนุมานที่ใช้ สัจพจน์ความเท่าเทียมกันเหล่านี้คือ: ^{[ 26 ] : 198–200}

• การสะท้อนกลับสำหรับแต่ละตัวแปรx , x = x .
• การแทนที่ฟังก์ชัน สำหรับตัวแปร xและyทั้งหมดและสัญลักษณ์ฟังก์ชันf ใด ๆ

  x = y → f (..., x , ...) = f (..., y , ...).

• การแทนที่สำหรับสูตรต่างๆสำหรับตัวแปรxและy ใดๆ และสูตร φ( z ) ใดๆ ที่มีตัวแปรอิสระ z แล้ว:

  x = y → (φ(x) → φ(y))

เหล่านี้คือแผนผังสัจพจน์ซึ่งแต่ละแผนผังระบุชุดสัจพจน์อนันต์ แผนผังที่สามเรียกว่ากฎของไลบ์นิซ "หลักการทดแทน" "ความไม่สามารถแยกแยะสิ่งเหมือนกันได้" หรือ "คุณสมบัติการแทนที่" แผนผังที่สองซึ่งเกี่ยวข้องกับสัญลักษณ์ฟังก์ชันfนั้น (เทียบเท่ากับ) กรณีพิเศษของแผนผังที่สาม โดยใช้สูตร:

φ(z): f (..., x , ...) = f (..., z , ...)

แล้ว

x = y → ( f (..., x , ...) = f (..., x , ...) → f (..., x , ...) = f (..., y , ...)).

เนื่องจากกำหนดให้x = y และ f (..., x , ...) = f (..., x , ...) เป็นจริงโดยสมบัติการสะท้อนกลับ เราจึงได้ว่าf (..., x , ...) = f (..., y , ...)

คุณสมบัติอื่นๆ ของความเท่าเทียมกันอีกมากมายเป็นผลสืบเนื่องมาจากสัจพจน์ข้างต้น ตัวอย่างเช่น:

• สมมาตรถ้าx = yแล้วy = x ^{[ 27 ]}​
• ^{คุณสมบัติ}การถ่ายทอดถ้าx = yและy = zแล้วx = z ^{[ 28} ]

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

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

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

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

ทฤษฎีบางทฤษฎีอนุญาตให้ มีการกำหนดนิยามความเท่าเทียมกัน แบบเฉพาะกิจ อื่นๆ ได้ :

• ในทฤษฎีลำดับบางส่วนที่มีสัญลักษณ์ความสัมพันธ์ ≤ หนึ่งตัว เราสามารถกำหนดให้s = tเป็นตัวย่อของs ≤ t t ≤ sได้${\displaystyle \wedge }$
• ในทฤษฎีเซตที่มีความสัมพันธ์ ∈ เพียงหนึ่งเดียว เราอาจกำหนดให้s = tเป็นตัวย่อของ∀ x ( s ∈ x ↔ t ∈ x ) ∀ x ( x ∈ s ↔ x ∈ t )${\displaystyle \wedge }$นิยามของความเท่าเทียมกันนี้จะสอดคล้องกับสัจพจน์ของความเท่าเทียมกันโดยอัตโนมัติ ในกรณีนี้ เราควรแทนที่สัจพจน์เรื่องความเท่าเทียมกัน ตามปกติ ซึ่งสามารถกล่าวได้ว่าด้วยสูตรทางเลือกอื่นที่กล่าวว่า ถ้าเซตxและyมีสมาชิกเหมือนกันแล้ว สมาชิกทั้งสองนั้นก็จะอยู่ในเซตเดียวกันด้วย${\displaystyle \forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow x=y]}$${\displaystyle \forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)]}$

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

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

แตกต่างจากตรรกศาสตร์เชิงประพจน์ตรรกศาสตร์อันดับหนึ่งไม่สามารถตัดสินได้ (แม้ว่าจะสามารถตัดสินได้บางส่วน) โดยมีเงื่อนไขว่าภาษาดังกล่าวต้องมีภาคแสดงอย่างน้อยหนึ่งภาคแสดงที่มีจำนวนสมาชิกอย่างน้อย 2 ตัว (นอกเหนือจากความเท่าเทียมกัน) ซึ่งหมายความว่าไม่มีกระบวนการตัดสินใจใดที่สามารถระบุได้ว่าสูตรใดๆ นั้นถูกต้องตามหลักตรรกศาสตร์หรือไม่ ผลลัพธ์นี้ได้รับการพิสูจน์โดยอิสระโดยAlonzo ChurchและAlan Turingในปี 1936 และ 1937 ตามลำดับ ซึ่งเป็นการให้คำตอบเชิงลบต่อปัญหาการตัดสินใจ (Entscheidungsproblem)ที่David HilbertและWilhelm Ackermann ตั้งขึ้น ในปี 1928 บทพิสูจน์ของพวกเขาแสดงให้เห็นถึงความเชื่อมโยงระหว่างความไม่สามารถแก้ปัญหาการตัดสินใจสำหรับตรรกศาสตร์อันดับหนึ่งและความไม่สามารถแก้ปัญหาการหยุดทำงานได้

มีระบบที่อ่อนแอกว่าตรรกะลำดับที่หนึ่งแบบสมบูรณ์ซึ่งความสัมพันธ์ของผลลัพธ์เชิงตรรกะสามารถตัดสินได้ ซึ่งรวมถึงตรรกะเชิงประพจน์และตรรกะภาคแสดงเอกภาคซึ่งเป็นตรรกะลำดับที่หนึ่งที่จำกัดเฉพาะสัญลักษณ์ภาคแสดงเอกภาคและไม่มีสัญลักษณ์ฟังก์ชัน ตรรกะอื่นๆ ที่ไม่มีสัญลักษณ์ฟังก์ชันซึ่งสามารถตัดสินได้ ได้แก่ส่วนย่อยที่มีการป้องกันของตรรกะลำดับที่หนึ่ง เช่นเดียวกับตรรกะสองตัวแปร คลาส Bernays –Schönfinkelของสูตรลำดับที่หนึ่งก็สามารถตัดสินได้เช่นกัน เซตย่อยที่สามารถตัดสินได้ของตรรกะลำดับที่หนึ่งยังได้รับการศึกษาในกรอบของตรรกะเชิงพรรณนาดู (Pratt-Hartmann, 2023) สำหรับเอกสารวิจัย^{[ 29 ]}

ตัวอย่างของส่วนย่อยที่ตัดสินได้: ^{[ 30 ]}

• C ₂ , FOL ที่มีตัวแปรสองตัวและตัวบ่งปริมาณการนับ และ. ^{[ 31 ]}${\displaystyle \exists ^{\geq n}}$${\displaystyle \exists ^{\leq n}}$
• ส่วนย่อยลำดับที่หนึ่งแบบเอกภาค (MFO หรือส่วนย่อยของโลเวนไฮม์): FOL ที่ไม่มีความเท่าเทียมกัน ไม่มีสัญลักษณ์ฟังก์ชัน และมีเพียงสัญลักษณ์ภาคแสดงเอกภาคเท่านั้น
• ส่วนประกอบ Löb–Gurevich: FOL ที่ไม่มีความเท่าเทียมกัน มีเพียงสัญลักษณ์ฟังก์ชันเอกภาค และมีเพียงสัญลักษณ์ภาคแสดงเอกภาค
• ส่วนของ Rabin: FOL ที่มีความเท่าเทียมกัน มีสัญลักษณ์ฟังก์ชันเอกภาคเพียงตัวเดียว และมีสัญลักษณ์ภาคแสดงเอกภาคเท่านั้น
• เศษส่วน Bernays–Schönfinkel–Ramsey: ประโยคเชิงสัมพันธ์ลำดับที่หนึ่งทั้งหมดในรูปแบบปกติ prenex ที่มีคำนำหน้าและมีความเท่าเทียมกัน${\displaystyle \exists ^{*}\forall ^{*}}$

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

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

ทฤษฎีความกะทัดรัดระบุว่าเซตของประโยคลำดับที่หนึ่งจะมีแบบจำลองก็ต่อเมื่อเซตย่อยจำกัดทุกเซตของประโยคนั้นมีแบบจำลอง^{[ 32 ]}ซึ่งหมายความว่าหากสูตรเป็นผลสืบเนื่องเชิงตรรกะของเซตอนันต์ของสัจพจน์ลำดับที่หนึ่งแล้ว สูตรนั้นจะเป็นผลสืบเนื่องเชิงตรรกะของสัจพจน์จำนวนจำกัดบางจำนวน ทฤษฎีบทนี้ได้รับการพิสูจน์ครั้งแรกโดย Kurt Gödel เป็นผลสืบเนื่องมาจากทฤษฎีบทความสมบูรณ์ แต่มีการพิสูจน์เพิ่มเติมอีกมากมายในช่วงเวลาต่อมา มันเป็นเครื่องมือสำคัญในทฤษฎีแบบจำลอง ซึ่งเป็นวิธีการพื้นฐานสำหรับการสร้างแบบจำลอง

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

นอกจากนี้ยังมีข้อจำกัดที่ละเอียดอ่อนกว่าของตรรกศาสตร์ลำดับที่หนึ่งซึ่งบ่งบอกโดยทฤษฎีความกะทัดรัด ตัวอย่างเช่น ในวิทยาศาสตร์คอมพิวเตอร์ สถานการณ์หลายอย่างสามารถจำลองได้เป็นกราฟแบบมีทิศทางของสถานะ (โหนด) และการเชื่อมต่อ (ขอบแบบมีทิศทาง) การตรวจสอบความถูกต้องของระบบดังกล่าวอาจต้องแสดงให้เห็นว่าไม่มีสถานะ "ไม่ดี" ใดที่สามารถเข้าถึงได้จากสถานะ "ดี" ใดๆ ดังนั้นจึงต้องพิจารณาว่าสถานะที่ดีและไม่ดีอยู่ในส่วนประกอบที่เชื่อมต่อกัน ที่แตกต่างกัน ของกราฟหรือไม่ อย่างไรก็ตาม ทฤษฎีความกะทัดรัดสามารถใช้เพื่อแสดงว่ากราฟที่เชื่อมต่อกันไม่ใช่คลาสพื้นฐานในตรรกศาสตร์ลำดับที่หนึ่ง และไม่มีสูตร φ( x , y ) ของตรรกศาสตร์ลำดับที่หนึ่งในตรรกศาสตร์ของกราฟที่แสดงแนวคิดว่ามีเส้นทางจากxไปยังyการเชื่อมต่อสามารถแสดงได้ในตรรกศาสตร์ลำดับที่สองแต่ไม่ใช่ด้วยตัวบ่งปริมาณเซตที่มีอยู่เพียงอย่างเดียว เนื่องจากก็มีความกะทัดรัดเช่นกัน ${\displaystyle \Sigma _{1}^{1}}$

เพอร์ ลินด์สตรอมแสดงให้เห็นว่าคุณสมบัติเชิงอภิปรัชญาที่กล่าวถึงไปข้างต้นนั้น แท้จริงแล้วเป็นลักษณะเฉพาะของตรรกะลำดับที่หนึ่ง ในแง่ที่ว่าไม่มีตรรกะที่แข็งแกร่งกว่าใดที่จะมีคุณสมบัติเหล่านั้นได้ (Ebbinghaus and Flum 1994, บทที่ XIII) ลินด์สตรอมได้นิยามคลาสของระบบตรรกะนามธรรม และนิยามที่เข้มงวดของความแข็งแกร่งสัมพัทธ์ของสมาชิกในคลาสนี้ เขาสร้างทฤษฎีบทสองข้อสำหรับระบบประเภทนี้:

• ระบบตรรกะที่ตรงตามคำนิยามของลินด์สตรอม ซึ่งประกอบด้วยตรรกะอันดับหนึ่ง และตรงตามทั้งทฤษฎีบทโลเวนไฮม์-สโกเลมและทฤษฎีบทความกะทัดรัด จะต้องเทียบเท่ากับตรรกะอันดับหนึ่ง
• ระบบตรรกะที่ตรงตามคำนิยามของลินด์สตรอม ซึ่งมีความสัมพันธ์เชิงผลลัพธ์เชิงตรรกะแบบกึ่งตัดสินได้ และตรงตามทฤษฎีบทโลเวนไฮม์-สโกเลม จะต้องเทียบเท่ากับตรรกะอันดับหนึ่ง

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

ทฤษฎีบทLöwenheim–Skolemแสดงให้เห็นว่า ถ้าทฤษฎีลำดับที่หนึ่งมีแบบจำลองอนันต์ใดๆ แล้ว ทฤษฎีบทนั้นก็จะมีแบบจำลองอนันต์ของทุกขนาดจำนวนสมาชิกด้วย โดยเฉพาะอย่างยิ่ง ไม่มีทฤษฎีลำดับที่หนึ่งใดๆ ที่มีแบบจำลองอนันต์จะเป็นตรรกะเชิงหมวดหมู่ได้ดังนั้น จึงไม่มีทฤษฎีลำดับที่หนึ่งใดๆ ที่มีแบบจำลองเพียงแบบเดียวที่มีเซตของจำนวนธรรมชาติเป็นโดเมน หรือที่มีแบบจำลองเพียงแบบเดียวที่มีเซตของจำนวนจริงเป็นโดเมน การขยายตรรกะลำดับที่หนึ่งหลายอย่าง รวมถึงตรรกะอนันต์และตรรกะลำดับสูงกว่า มีความสามารถในการแสดงออกมากกว่าในแง่ที่ว่ามันอนุญาตให้มีการกำหนดสัจพจน์เชิงหมวดหมู่ของจำนวนธรรมชาติหรือจำนวนจริง อย่างไรก็ตาม ความสามารถในการแสดงออกนี้มาพร้อมกับต้นทุนทางอภิตรรกะ: ตามทฤษฎีบทของ Lindströmทฤษฎีบทความกะทัดรัดและทฤษฎีบท Löwenheim–Skolem แบบลงล่างไม่สามารถใช้ได้ในตรรกะใดๆ ที่แข็งแกร่งกว่าลำดับที่หนึ่ง

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

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

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

ตรรกศาสตร์ลำดับที่หนึ่งสามารถศึกษาได้ในภาษาที่มีสัญลักษณ์ทางตรรกศาสตร์น้อยกว่าที่ได้กล่าวไว้ข้างต้น:

• เนื่องจากสามารถแสดงได้เป็นและสามารถแสดงได้เป็น ดังนั้นตัวบ่งปริมาณทั้งสองตัวคือและสามารถละทิ้งได้${\displaystyle \exists x\varphi (x)}$${\displaystyle \neg \forall x\neg \varphi (x)}$${\displaystyle \forall x\varphi (x)}$${\displaystyle \neg \exists x\neg \varphi (x)}$${\displaystyle \exists }$${\displaystyle \forall }$
• เนื่องจากสามารถแสดงได้เป็นและสามารถแสดงได้เป็นดังนั้นจึง สามารถตัด หรือออกได้ กล่าวอีกนัยหนึ่งคือ เพียงพอที่จะมีและหรือและเป็นตัวเชื่อมทางตรรกะเพียงอย่างเดียว${\displaystyle \varphi \lor \psi }$${\displaystyle \lnot (\lnot \varphi \land \lnot \psi )}$${\displaystyle \varphi \land \psi }$${\displaystyle \lnot (\lnot \varphi \lor \lnot \psi )}$${\displaystyle \vee }$${\displaystyle \wedge }$${\displaystyle \neg }$${\displaystyle \vee }$${\displaystyle \neg }$${\displaystyle \wedge }$
• ในทำนองเดียวกัน การใช้เพียงตัวเชื่อมตรรกะ " และ" หรือการใช้เพียงตัว ดำเนินการ Sheffer stroke (NAND) หรือ ตัวดำเนินการ Peirce arrow (NOR) ก็เพียงพอแล้ว${\displaystyle \neg }$${\displaystyle \rightarrow }$
• เป็นไปได้ที่จะหลีกเลี่ยงสัญลักษณ์ฟังก์ชันและสัญลักษณ์ค่าคงที่โดยสิ้นเชิง โดยเขียนใหม่ผ่านสัญลักษณ์ภาคแสดงในลักษณะที่เหมาะสม ตัวอย่างเช่น แทนที่จะใช้สัญลักษณ์ค่าคง ที่ อาจใช้ภาคแสดง (ตีความว่า) และแทนที่ภาคแสดงทุกตัว เช่นด้วยฟังก์ชันเช่นจะถูกแทนที่ด้วยภาคแสดง ที่ตีความว่า ใน ทำนองเดียวกัน การเปลี่ยนแปลงนี้จำเป็นต้องเพิ่มสัจพจน์เพิ่มเติมลงในทฤษฎีที่มีอยู่ เพื่อให้การตีความสัญลักษณ์ภาคแสดงที่ใช้มีความหมายที่ถูกต้อง^{[ 34 ]}${\displaystyle \;0}$${\displaystyle \;0(x)}$${\displaystyle \;x=0}$${\displaystyle \;P(0,y)}$${\displaystyle \forall x\;(0(x)\rightarrow P(x,y))}$${\displaystyle f(x_{1},x_{2},...,x_{n})}$${\displaystyle F(x_{1},x_{2},...,x_{n},y)}$${\displaystyle y=f(x_{1},x_{2},...,x_{n})}$

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

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

การตีความลำดับแรกทั่วไปมีโดเมนการสนทนาเดียวซึ่งตัวบ่งปริมาณทั้งหมดครอบคลุมตรรกะลำดับแรกแบบหลายประเภทอนุญาตให้ตัวแปรมีประเภท ที่แตกต่างกัน ซึ่งมีโดเมนที่แตกต่างกัน สิ่งนี้เรียกว่าตรรกะลำดับแรกแบบมีประเภท และประเภทต่างๆ เรียกว่าประเภท (เช่นเดียวกับประเภทข้อมูล ) แต่มันไม่เหมือนกับทฤษฎีประเภท ลำดับแรก ตรรกะลำดับแรกแบบหลายประเภทมักใช้ในการศึกษาเลขคณิตลำดับที่สอง^{[ 35 ]}

เมื่อมีชนิดเพียงจำนวนจำกัดในทฤษฎี ตรรกะลำดับที่หนึ่งที่มีหลายชนิดสามารถลดรูปเป็นตรรกะลำดับที่หนึ่งที่มีชนิดเดียวได้^{[ 36 ] : 296–299} มีการนำสัญลักษณ์ภาคแสดงเอกภาคสำหรับแต่ละชนิดในทฤษฎีที่มีหลายชนิดมาใส่ในทฤษฎีที่มีชนิดเดียว และเพิ่มสัจพจน์ที่ระบุว่าภาคแสดงเอกภาคเหล่านี้แบ่งโดเมนของการสนทนา ตัวอย่างเช่น ถ้ามีชนิดสองชนิด จะเพิ่มสัญลักษณ์ภาคแสดงและและสัจพจน์: ${\displaystyle P_{1}(x)}$${\displaystyle P_{2}(x)}$

${\displaystyle \forall x(P_{1}(x)\lor P_{2}(x))\land \lnot \exists x(P_{1}(x)\land P_{2}(x))}$.

จากนั้น องค์ประกอบที่ตรงตามเงื่อนไขจะถูกมองว่าเป็นองค์ประกอบประเภทแรก และองค์ประกอบที่ไม่ตรงตามเงื่อนไขจะถูกมองว่าเป็นองค์ประกอบประเภทที่สอง เราสามารถกำหนดปริมาณให้กับแต่ละประเภทได้โดยใช้สัญลักษณ์ภาคแสดงที่เกี่ยวข้องเพื่อจำกัดขอบเขตของการกำหนดปริมาณ ตัวอย่างเช่น หากต้องการกล่าวว่ามีองค์ประกอบประเภทแรกที่ตรงตามเงื่อนไขเราจะเขียนว่า: ${\displaystyle P_{1}}$${\displaystyle P_{2}}$${\displaystyle \varphi (x)}$

${\displaystyle \exists x(P_{1}(x)\land \varphi (x))}$.

สามารถเพิ่มตัวบ่งปริมาณเพิ่มเติมลงในตรรกะลำดับที่หนึ่งได้

• บางครั้ง การกล่าวว่า " P ( x )เป็นจริงสำหรับx เพียงตัวเดียว " ซึ่งสามารถแสดงได้เป็น∃! x P ( x ) นั้นมีประโยชน์ สัญลักษณ์นี้เรียกว่าการกำหนดปริมาณความเป็นเอกลักษณ์ซึ่งอาจใช้เพื่อย่อสูตร เช่น∃ x ( P ( x ) ∀ y ( P ( y ) → ( x = y${\displaystyle \wedge }$ ) ) )
• ตรรกศาสตร์ลำดับที่หนึ่งที่มีตัวบ่งปริมาณเพิ่มเติมจะมีตัวบ่งปริมาณใหม่Qx ,..., ซึ่งมีความหมายเช่น "มีx จำนวนมาก ที่ทำให้..." โปรดดูตัวบ่งปริมาณแบบแยกสาขาและตัวบ่งปริมาณพหูพจน์ของGeorge Boolosและคนอื่นๆ ด้วย
• ตัวบ่งปริมาณแบบมีขอบเขตมักถูกนำมาใช้ในการศึกษาทฤษฎีเซตหรือเลขคณิต

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

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

ตรรกศาสตร์อนันต์ที่นิยมศึกษามากที่สุดจะใช้สัญลักษณ์L _αβโดยที่ α และ β เป็นจำนวนเชิงคาร์ดินัลหรือสัญลักษณ์ ∞ ในสัญลักษณ์นี้ ตรรกศาสตร์อันดับหนึ่งทั่วไปจะใช้สัญลักษณ์L _ωωในตรรกศาสตร์L _∞ωอนุญาตให้ใช้การเชื่อมหรือการแยกแบบใดก็ได้ในการสร้างสูตร และมีตัวแปรไม่จำกัดจำนวน โดยทั่วไปแล้ว ตรรกศาสตร์ที่อนุญาตให้ใช้การเชื่อมหรือการแยกที่มีส่วนประกอบน้อยกว่า κ เรียกว่าL _κωตัวอย่างเช่นL _{ω 1 ω}อนุญาตให้ ใช้ การเชื่อมและการแยกที่ นับได้

เซตของตัวแปรอิสระในสูตรของL _κωสามารถมีจำนวนสมาชิกน้อยกว่า κ อย่างเคร่งครัดได้ แต่มีเพียงจำนวนจำกัดเท่านั้นที่อยู่ในขอบเขตของตัวบ่งปริมาณใดๆ เมื่อสูตรปรากฏเป็นสูตรย่อยของสูตรอื่น^{[ 37 ]}ในตรรกะอนันต์อื่นๆ สูตรย่อยอาจอยู่ในขอบเขตของตัวบ่งปริมาณจำนวนอนันต์ ตัวอย่างเช่น ในL _κ∞ตัวบ่งปริมาณสากลหรือตัวบ่งปริมาณที่มีอยู่เพียงตัวเดียวอาจผูกตัวแปรจำนวนมากพร้อมกันได้ ในทำนองเดียวกัน ตรรกะL _κλอนุญาตให้มีการบ่งปริมาณพร้อมกันเหนือตัวแปรน้อยกว่า λ เช่นเดียวกับการเชื่อมโยงและการแยกที่มีขนาดน้อยกว่า κ

• ตรรกศาสตร์ลำดับที่หนึ่งแบบสัญชาตญาณนิยมใช้การให้เหตุผลแบบสัญชาตญาณนิยมแทนการให้เหตุผลแบบคลาสสิก ตัวอย่างเช่น ¬¬φ ไม่จำเป็นต้องเทียบเท่ากับ φ และ ¬ ∀x.φ โดยทั่วไปแล้วจะไม่เทียบเท่ากับ ∃ x.¬φ
• ตรรกศาสตร์โมดอลลำดับที่หนึ่งช่วยให้เราสามารถอธิบายโลกที่เป็นไปได้อื่นๆ ได้เช่นเดียวกับโลกที่เราอาศัยอยู่ซึ่งเป็นจริงโดยบังเอิญ ในบางเวอร์ชัน เซตของโลกที่เป็นไปได้จะแตกต่างกันไปขึ้นอยู่กับว่าเราอาศัยอยู่ในโลกที่เป็นไปได้ใด ตรรกศาสตร์โมดอลมีตัวดำเนินการโมดอล พิเศษ ที่มีความหมายซึ่งสามารถอธิบายอย่างไม่เป็นทางการได้ เช่น "จำเป็นที่ φ" (เป็นจริงในทุกโลกที่เป็นไปได้) และ "เป็นไปได้ที่ φ" (เป็นจริงในบางโลกที่เป็นไปได้) ด้วยตรรกศาสตร์ลำดับที่หนึ่งแบบมาตรฐาน เรามีโดเมนเดียว และแต่ละ述语จะถูกกำหนดส่วนขยายหนึ่งส่วน ด้วยตรรกศาสตร์โมดอลลำดับที่หนึ่ง เรามีฟังก์ชันโดเมนที่กำหนดโดเมนให้กับแต่ละโลกที่เป็นไปได้ เพื่อให้แต่ละ述语ได้รับส่วนขยายเฉพาะที่สัมพันธ์กับโลกที่เป็นไปได้เหล่านั้นเท่านั้น สิ่งนี้ช่วยให้เราสามารถจำลองกรณีต่างๆ ได้ เช่น อเล็กซ์เป็นนักปรัชญา แต่เขาอาจเป็นนักคณิตศาสตร์ และอาจไม่มีอยู่จริงเลยก็ได้ ในโลกที่เป็นไปได้แรกP ( a ) เป็นจริง ในโลกที่สองP ( a ) เป็นเท็จ และในโลกที่เป็นไปได้ที่สาม ไม่มีa อยู่ ในโดเมนเลย
• ตรรกะคลุมเครือลำดับที่หนึ่งเป็นส่วนขยายลำดับที่หนึ่งของตรรกะคลุมเครือเชิงประพจน์ ไม่ใช่แคลคูลัสเชิงประพจน์ แบบคลาสสิ ก

ตรรกะจุดตรึงขยายตรรกะลำดับที่หนึ่งโดยการเพิ่มการปิดภายใต้จุดตรึงที่น้อยที่สุดของตัวดำเนินการบวก^{[ 38 ]}

ลักษณะเด่นของตรรกศาสตร์ลำดับที่หนึ่งคือ สามารถกำหนดปริมาณของตัวบุคคลได้ แต่ไม่สามารถกำหนดปริมาณของภาคแสดงได้ ดังนั้น

${\displaystyle \exists a({\text{Phil}}(a))}$

เป็นสูตรลำดับแรกทางกฎหมาย แต่

${\displaystyle \exists {\text{Phil}}({\text{Phil}}(a))}$

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

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

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

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

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

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

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

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

• "แคลคูลัสภาคแสดง" , สารานุกรมคณิตศาสตร์ , EMS Press , 2001 [1994]
• สารานุกรมปรัชญาแห่งสแตนฟอร์ด (2000): Shapiro, S. , " ตรรกศาสตร์คลาสสิก " ครอบคลุมไวยากรณ์ ทฤษฎีแบบจำลอง และอภิปรัชญาสำหรับตรรกศาสตร์ลำดับที่หนึ่งในรูปแบบการอนุมานตามธรรมชาติ
• Magnus, PD; forall x: an introduction to formal logic . ครอบคลุมความหมายเชิงรูปธรรมและทฤษฎีการพิสูจน์สำหรับตรรกะลำดับที่หนึ่ง
• Metamath : โครงการออนไลน์ที่กำลังดำเนินอยู่เพื่อสร้างคณิตศาสตร์ขึ้นใหม่ในฐานะทฤษฎีลำดับที่หนึ่งขนาดใหญ่ โดยใช้ตรรกะลำดับที่หนึ่งและทฤษฎีเซตเชิงสัจพจน์ ZFC Principia Mathematicaฉบับปรับปรุงใหม่
• พอดนีคส์, คาร์ล; บทนำสู่ตรรกศาสตร์ทางคณิตศาสตร์
• บันทึกย่อวิชาคณิตศาสตร์ระดับ Tripos ของเคมบริดจ์ (จัดพิมพ์โดย จอห์น เฟรมลิน) บันทึกย่อเหล่านี้ครอบคลุมส่วนหนึ่งของ หลักสูตร วิชาคณิตศาสตร์ระดับ Tripos ของเคมบริดจ์ ในอดีต ซึ่งสอนให้กับนักศึกษาระดับปริญญาตรี (โดยปกติ) ในปีที่สาม หลักสูตรนี้มีชื่อว่า "ตรรกศาสตร์ การคำนวณ และทฤษฎีเซต" และครอบคลุมเนื้อหาเกี่ยวกับจำนวนเชิงอันดับและจำนวนเชิงคาร์ดินัล โพเซตและทฤษฎีบทของซอร์น ตรรกศาสตร์เชิงประพจน์ ตรรกศาสตร์เชิงภาคแสดง ทฤษฎีเซต และประเด็นความสอดคล้องที่เกี่ยวข้องกับ ZFC และทฤษฎีเซตอื่นๆ
• โปรแกรม Tree Proof Generatorสามารถตรวจสอบความถูกต้องหรือไม่ถูกต้องของสูตรตรรกะลำดับที่หนึ่งได้โดยใช้ วิธี ตารางความหมาย (semantic tableaux method)