ในตรรกศาสตร์ทางคณิตศาสตร์สัจนิรันดร์ (จากภาษากรีกโบราณ: ταυτολογία ) คือสูตรที่จริงเสมอไม่ว่าจะตีความส่วนประกอบต่างๆ อย่างไรก็ตามโดยมีเพียงค่าคงที่ทางตรรกศาสตร์ เท่านั้น ที่มีความหมายคงที่ มันคือความจริงทางตรรกศาสตร์ตัวอย่างเช่น สูตรที่กล่าวว่า "ลูกบอลเป็นสีเขียวหรือลูกบอลไม่ใช่สีเขียว" นั้นเป็นจริงเสมอ ไม่ว่าลูกบอลจะเป็นอย่างไรและไม่ว่าสีของมันจะเป็นอะไรก็ตาม โดยทั่วไปแล้ว สัจนิรันดร์มักใช้เพื่ออ้างถึงสูตรที่ถูกต้องของตรรกศาสตร์เชิงประพจน์แต่ ก็ไม่เสมอไป

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

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

สัญลักษณ์ประตูหมุนคู่${\displaystyle \vDash S}$ใช้เพื่อระบุว่าSเป็นสัจนิรันดร์ สัจนิรันดร์บางครั้งใช้สัญลักษณ์ "V pq " และความขัดแย้งใช้สัญลักษณ์ "O pq " สัญลักษณ์ที${\displaystyle \top }$บางครั้งใช้เพื่อแสดงถึงสัจนิรันดร์โดยพลการ โดยใช้สัญลักษณ์คู่${\displaystyle \bot }$( เท็จ ) แสดงถึงความขัดแย้งโดยพลการ ในสัญลักษณ์ใดๆ สัจนิรันดร์อาจใช้แทนค่าความจริง " จริง " ได้ เช่น ใช้สัญลักษณ์ "1" ^{[ 1 ]}

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

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

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

ในปี ค.ศ. 1800 อิมมานูเอล คานต์ได้เขียนไว้ในหนังสือตรรกศาสตร์ ของเขา ว่า:

เอกลักษณ์ของแนวคิดในการตัดสินเชิงวิเคราะห์อาจเป็นแบบชัดเจน ( explicita ) หรือไม่ชัดเจน ( implicita ) ก็ได้ ในกรณีแรก ข้อเสนอเชิงวิเคราะห์จะเป็นสัจพจน์

ในที่นี้ประโยคเชิงวิเคราะห์หมายถึงความจริงเชิงวิเคราะห์ซึ่งเป็นข้อความในภาษาธรรมชาติที่เป็นจริงเพียงเพราะเงื่อนไขที่เกี่ยวข้องเท่านั้น

ในปี ค.ศ. 1884 ก็อตต์ลอบ เฟรเกอเสนอในหนังสือ Grundlagen ของเขา ว่า ความจริงจะเป็นความจริงเชิงวิเคราะห์ได้ก็ต่อเมื่อสามารถอนุมานได้โดยใช้ตรรกะ อย่างไรก็ตาม เขายังคงแยกแยะความแตกต่างระหว่างความจริงเชิงวิเคราะห์ (กล่าวคือ ความจริงที่อิงตามความหมายของคำเท่านั้น) กับสัจนิรันดร์ (กล่าวคือ ข้อความที่ปราศจากเนื้อหา)

ในหนังสือTractatus Logico-Philosophicusปี 1921 ลุดวิก วิทเกนสไตน์ เสนอว่าข้อความที่สามารถอนุมานได้โดยการอนุมานเชิงตรรกะเป็นข้อความสัจนิรันดร์ (ว่างเปล่าจากความหมาย) และเป็นความจริงเชิงวิเคราะห์ด้วยเช่นกันอองรี ปวงกาเรเคยกล่าวถึงเรื่องนี้ในทำนองเดียวกันในหนังสือ Science and Hypothesisปี 1905 แม้ว่า ในตอนแรก เบอร์ทรานด์ รัสเซลล์จะโต้แย้งข้อสังเกตของวิทเกนสไตน์และปวงกาเร โดยอ้างว่าความจริงทางคณิตศาสตร์ไม่เพียงแต่ไม่ใช่สัจนิรันดร์ แต่ยังเป็นความจริงเชิงสังเคราะห์ด้วย แต่ต่อมาเขาก็กล่าวสนับสนุนข้อสังเกตเหล่านั้นในปี 1918

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

ในที่นี้ประโยคตรรกะหมายถึงประโยคที่สามารถพิสูจน์ได้โดยใช้กฎของตรรกะ

นักตรรกศาสตร์หลายคนในช่วงต้นศตวรรษที่ 20 ใช้คำว่า 'สัจนิรันดร์' สำหรับสูตรใดๆ ที่ถูกต้องในทุกกรณี ไม่ว่าจะเป็นสูตรของตรรกศาสตร์เชิงประพจน์หรือตรรกศาสตร์เชิงภาคแสดงในความหมายกว้างๆ นี้ สัจนิรันดร์คือสูตรที่เป็นจริงภายใต้การตีความ ทั้งหมด หรือเทียบเท่าทางตรรกะกับการปฏิเสธของความขัดแย้งTarskiและGödelใช้ตามนี้ และปรากฏในตำราเรียน เช่น ตำราของ Lewis และ Langford ^{[ 3 ]}การใช้คำในความหมายกว้างๆ นี้ไม่ค่อยพบเห็นในปัจจุบัน แม้ว่าตำราเรียนบางเล่มยังคงใช้อยู่^{[ 4 ] [ 5 ]}

ตำราเรียนสมัยใหม่มักจะจำกัดการใช้ 'สัจนิรันดร์' ไว้เฉพาะประโยคที่ถูกต้องของตรรกะเชิงประพจน์ หรือประโยคที่ถูกต้องของตรรกะเชิงภาคแสดงที่สามารถลดรูปเป็นสัจนิรันดร์เชิงประพจน์ได้โดยการแทนที่^{[ 6 ] [ 7 ]}

ตรรกศาสตร์เชิงประพจน์เริ่มต้นด้วยตัวแปรเชิงประพจน์ซึ่งเป็นหน่วยพื้นฐานที่แทนประพจน์ที่เป็นรูปธรรมสูตรประกอบด้วยตัวแปรเชิงประพจน์ที่เชื่อมต่อกันด้วยตัวเชื่อมทางตรรกะ สร้างขึ้นในลักษณะที่ว่าความจริงของสูตรโดยรวมสามารถอนุมานได้จากความจริงหรือความเท็จของแต่ละตัวแปรค่าประเมินคือฟังก์ชันที่กำหนดค่าให้กับตัวแปรเชิงประพจน์แต่ละตัวเป็น T (สำหรับความจริง) หรือ F (สำหรับความเท็จ) ดังนั้นโดยใช้ตัวแปรเชิงประพจน์AและBตัวเชื่อมแบบไบนารี${\displaystyle \lor }$และ${\displaystyle \land }$แทนการแยกและการเชื่อมต่อตามลำดับ และตัวเชื่อมเอกภาค${\displaystyle \lnot }$เมื่อแทนการปฏิเสธจะได้สูตรดังต่อไปนี้:${\displaystyle (A\land B)\lor (\lnot A)\lor (\lnot B)}$.

ในการประเมินค่าตรงนี้ จะต้องกำหนดค่าให้กับ AและBแต่ละตัวว่าเป็นจริงหรือเท็จ แต่ไม่ว่าการกำหนดค่าจะเป็นอย่างไร สูตรโดยรวมก็จะยังคงเป็นจริงอยู่ดี เพราะถ้าเงื่อนไขแรกเป็นจริง${\displaystyle (A\land B)}$หากค่าที่กำหนดไม่ตรงกับเงื่อนไขใดเงื่อนไขหนึ่ง แสดงว่าAหรือBต้องถูกกำหนดค่าเป็น F ซึ่งจะทำให้เงื่อนไขใดเงื่อนไขหนึ่งต่อไปนี้ถูกกำหนดค่าเป็น T ในภาษาธรรมชาติ เงื่อนไขคือ A และ B ทั้งสองเป็นจริง หรืออย่างน้อยหนึ่งตัวเป็นเท็จ

สูตรตรรกศาสตร์เชิงประพจน์เป็นสัจนิรันดร์หากสูตรนั้นเป็นจริงเสมอ ไม่ว่าตัวแปรเชิงประพจน์จะถูกกำหนดค่าอย่างไรก็ตาม สัจนิรันดร์มีอยู่เป็นจำนวนอนันต์

ในตัวอย่างต่อไปนี้หลายๆ ตัวอย่างAแทนข้อความ "วัตถุXถูกผูกไว้" Bแทนข้อความ "วัตถุXเป็นหนังสือ" และ C แทนข้อความ "วัตถุXอยู่บนชั้นวาง" หากไม่มีการระบุวัตถุX ที่อ้างถึงอย่างเฉพาะ เจาะจง${\displaystyle A\to B}$ สอดคล้องกับข้อเสนอที่ว่า "สิ่งของที่ถูกผูกมัดทั้งหมดล้วนเป็นหนังสือ"

• ${\displaystyle (A\lor \lไม่ใช่ A)}$(“ Aหรือไม่ใช่A ”) กฎของตัวกลางที่ไม่รวมอยู่ด้วยสูตรนี้มีตัวแปรเชิงประพจน์เพียงตัวเดียวคือAการประเมินค่าใดๆ สำหรับสูตรนี้ ตามคำนิยาม จะต้องกำหนด ค่าความจริงให้กับ Aเป็นค่าใดค่าหนึ่งระหว่างจริงหรือเท็จและกำหนดค่าให้กับ A${\displaystyle \lnot }$ค่าความจริงอีกค่า หนึ่งตัวอย่างเช่น "แมวเป็นสีดำ หรือ แมวไม่ใช่สีดำ"
• ${\displaystyle (A\to B)\Leftrightarrow (\lnot B\to \lnot A)}$(“ถ้าAบ่งชี้ว่าBแล้ว ถ้าไม่ใช่Bก็ไม่ใช่A ” และในทางกลับกัน) ซึ่งแสดงถึงกฎแห่งการแย้งตัวอย่างเช่น “ถ้ามันถูกเย็บเล่ม มันก็คือหนังสือ ถ้ามันไม่ใช่หนังสือ มันก็ไม่ได้ถูกเย็บเล่ม” และในทางกลับกัน
• ${\displaystyle ((\lnot A\to B)\land (\lnot A\to \lnot B))\to A}$(“ถ้าไม่ใช่Aหมายความว่าทั้งBและไม่ใช่B ซึ่งเป็นการปฏิเสธของ A แล้ว ไม่ใช่Aต้องเป็นเท็จ แล้วAต้องเป็นจริง”) ซึ่งเป็นหลักการที่เรียกว่าการพิสูจน์โดยการหักล้าง (reductio ad absurdum ) ตัวอย่างเช่น “ถ้ามันไม่ได้ถูกเย็บเล่ม เราก็รู้ว่ามันเป็นหนังสือ ถ้ามันไม่ถูกเย็บเล่ม เราก็รู้ว่ามันไม่ใช่หนังสือ ดังนั้นมันจึงถูกเย็บเล่ม”
• ${\displaystyle \lnot (A\land B)\Leftrightarrow (\lnot A\lor \lnot B)}$(“ถ้าไม่ใช่ทั้งAและBก็ไม่ใช่Aหรือไม่ใช่B ” และในทางกลับกัน) ซึ่งเป็นที่รู้จักกันในชื่อกฎของเดอ มอร์แกน “ถ้ามันไม่ใช่ทั้งหนังสือและไม่ได้เข้าเล่ม เราก็มั่นใจได้ว่ามันไม่ใช่หนังสือหรือมันไม่ได้เข้าเล่ม” และในทางกลับกัน
• ${\displaystyle ((A\to B)\land (B\to C))\to (A\to C)}$("ถ้าAบ่งชี้BและBบ่งชี้Cแล้วAบ่งชี้C ") ซึ่งเป็นหลักการที่เรียกว่าการอนุมานเชิงสมมติฐาน "ถ้ามันถูกเย็บเล่มแล้ว มันก็คือหนังสือ และถ้ามันเป็นหนังสือ มันก็ต้องอยู่บนชั้นนั้น ดังนั้นถ้ามันถูกเย็บเล่มแล้ว มันก็ต้องอยู่บนชั้นนั้น"
• ${\displaystyle ((A\lor B)\land (A\to C)\land (B\to C))\to C}$(“ถ้าอย่างน้อยหนึ่งข้อระหว่างAหรือBเป็นจริง และแต่ละข้อบ่งชี้ถึงCแล้วCก็ต้องเป็นจริงด้วย”) ซึ่งเป็นหลักการที่เรียกว่าการพิสูจน์โดยกรณีต่างๆ “สิ่งของที่เข้าเล่มและหนังสืออยู่บนชั้นนั้น ถ้าเป็นหนังสือหรือเข้าเล่มแล้ว ก็ต้องอยู่บนชั้นนั้น”

สัจนิรันดร์ขั้นต่ำ คือ สัจนิรันดร์ที่ไม่ใช่ตัวอย่างของสัจนิรันดร์ที่สั้นกว่า

• ${\displaystyle (A\lor B)\to (A\lor B)}$เป็นสัจนิรันดร์ แต่ไม่ใช่สัจนิรันดร์ขั้นต่ำ เพราะมันเป็นตัวอย่างของ${\displaystyle C\to C}$.

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

ตัวอย่างเช่น ลองพิจารณาสูตรนี้

${\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C)).}$

ตัวแปรเชิงประพจน์A , B , C มีค่าที่เป็นไปได้ 8 ค่า ซึ่งแสดงโดยสามคอลัมน์แรกของตารางต่อไปนี้ คอลัมน์ที่เหลือแสดงค่าความจริงของสูตรย่อยของสูตรข้างต้น โดยจบลงด้วยคอลัมน์ที่แสดงค่าความจริงของสูตรดั้งเดิมภายใต้ค่าแต่ละค่า

⁠${\displaystyle A}$⁠	⁠${\displaystyle B}$⁠	⁠${\displaystyle C}$⁠	${\displaystyle A\land B}$	${\displaystyle (A\land B)\to C}$	${\displaystyle B\to C}$	${\displaystyle A\to (B\to C)}$	${\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}$
ที	ที	ที	ที	ที	ที	ที	ที
ที	ที	เอฟ	ที	เอฟ	เอฟ	เอฟ	ที
ที	เอฟ	ที	เอฟ	ที	ที	ที	ที
ที	เอฟ	เอฟ	เอฟ	ที	ที	ที	ที
เอฟ	ที	ที	เอฟ	ที	ที	ที	ที
เอฟ	ที	เอฟ	เอฟ	ที	เอฟ	ที	ที
เอฟ	เอฟ	ที	เอฟ	ที	ที	ที	ที
เอฟ	เอฟ	เอฟ	เอฟ	ที	ที	ที	ที

เนื่องจากแต่ละแถวในคอลัมน์สุดท้ายแสดงค่าTจึงยืนยันได้ว่าประโยคดังกล่าวเป็นสัจนิรันดร์

นอกจากนี้ ยังสามารถกำหนดระบบนิรนัย (เช่น ระบบพิสูจน์) สำหรับตรรกศาสตร์เชิงประพจน์ได้ โดยเป็นรูปแบบที่ง่ายกว่าของระบบนิรนัยที่ใช้ในตรรกศาสตร์อันดับหนึ่ง (ดู Kleene 1967, Sec 1.9 สำหรับระบบดังกล่าวระบบหนึ่ง) การพิสูจน์สัจนิรันดร์ในระบบนิรนัยที่เหมาะสมอาจสั้นกว่าตารางความจริงที่สมบูรณ์มาก (สูตรที่มี ตัวแปรเชิงประพจน์ nตัว ต้องใช้ตารางความจริงที่มี 2 ^ⁿ บรรทัด ซึ่งจะทำได้ยากอย่างรวดเร็วเมื่อnเพิ่มขึ้น) ระบบพิสูจน์ยังจำเป็นสำหรับการศึกษา ตรรกศาสตร์เชิงประพจน์แบบ สัญชาตญาณนิยมซึ่งไม่สามารถใช้วิธีตารางความจริงได้ เนื่องจากไม่ถือว่ามีกฎของสิ่งที่ไม่รวมอยู่ตรงกลาง

กล่าวได้ว่าสูตรR บ่งชี้สูตรS โดยปริยาย ถ้าทุกค่าที่ทำให้Rเป็นจริงจะทำให้Sเป็นจริงด้วย สถานการณ์นี้เรียกว่า${\displaystyle R\models S}$มันเทียบเท่ากับสูตร${\displaystyle R\to S}$เป็นคำกล่าวซ้ำซ้อน (Kleene 1967 หน้า 27)

ตัวอย่างเช่น สมมติว่า${\displaystyle S}$เป็น${\displaystyle A\land (B\lor \lnot B)}$. แล้ว${\displaystyle S}$ไม่ใช่การกล่าวซ้ำซ้อน เพราะการประเมินค่าใดๆ ที่ทำให้${\displaystyle A}$เท็จจะทำให้${\displaystyle S}$เท็จ แต่การประเมินมูลค่าใดๆ ที่ทำให้${\displaystyle A}$ความจริงจะทำให้${\displaystyle S}$จริง เพราะ${\displaystyle B\lor \lnot B}$เป็นสัจพจน์ ให้${\displaystyle R}$เป็นสูตร${\displaystyle A\land C}$. แล้ว${\displaystyle R\models S}$เพราะการประเมินค่าใดๆ ที่ตรงตามเงื่อนไข${\displaystyle R}$จะทำให้${\displaystyle A}$เป็นความจริง—และด้วยเหตุนี้จึงทำให้${\displaystyle S}$จริง.

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

มีขั้นตอนทั่วไปที่เรียกว่ากฎการแทนที่ซึ่งช่วยให้สามารถสร้างสัจนิรันดร์เพิ่มเติมจากสัจนิรันดร์ที่กำหนดให้ (Kleene 1967 ส่วนที่ 3) สมมติว่าS เป็นสัจนิรันดร์ และสำหรับตัวแปรเชิงประพจน์ Aแต่ละตัวในS จะมีการเลือก ประโยคคงที่S หนึ่งประโยค จากนั้นประโยคที่ได้จากการแทนที่ตัวแปรA แต่ละตัว ในSด้วยประโยคS ที่สอดคล้องกันนั้น ก็เป็นสัจนิรันดร์เช่นกัน

ตัวอย่างเช่น ให้Sเป็นสัจนิรันดร์:

${\displaystyle (A\land B)\lor \lnot A\lor \lnot B}$.

ให้S เป็น${\displaystyle C\lor D}$และให้S เป็น${\displaystyle C\to E}$.

จากกฎการแทนที่ จะได้ประโยคดังนี้:

${\displaystyle ((C\lor D)\land (C\to E))\lor \lnot (C\lor D)\lor \lnot (C\to E)}$

เป็นการกล่าวซ้ำซ้อนเช่นกัน

ระบบสัจพจน์จะสมบูรณ์ก็ต่อเมื่อสัจพจน์ทุกข้อเป็นทฤษฎีบท (ที่สามารถอนุมานได้จากสัจพจน์) ระบบสัจพจน์จะถูกต้องก็ต่อเมื่อทฤษฎีบททุกข้อเป็นสัจพจน์

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

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

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

ปัญหาของการพิจารณาว่ามีค่าใดที่ทำให้สูตรเป็นจริงหรือไม่ คือปัญหาความสามารถในการทำให้เป็นจริงของบูลีนปัญหาของการตรวจสอบสัจนิรันดร์นั้นเทียบเท่ากับปัญหานี้ เพราะการตรวจสอบว่าประโยคSเป็นสัจนิรันดร์นั้นเทียบเท่ากับการตรวจสอบว่าไม่มีค่าใดที่ทำให้สูตรเป็นจริง${\displaystyle \lnot S}$ปัญหาความพึงพอใจของบูลีนเป็นปัญหาNP-completeและด้วยเหตุนี้ สัจนิรันดร์จึงเป็นปัญหาco-NP-completeเป็นที่เชื่อกันอย่างกว้างขวางว่า (เทียบเท่ากับปัญหา NP-complete ทั้งหมด) ไม่มีอัลกอริทึมเวลาพหุนาม ใด ที่สามารถแก้ปัญหาความพึงพอใจได้ แม้ว่าอัลกอริทึมบางตัวจะทำงานได้ดีกับสูตรบางประเภท หรือยุติการทำงานอย่างรวดเร็วกับหลายกรณี^{[ 8 ]}

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

สัจนิรันดร์ในตรรกศาสตร์ลำดับที่หนึ่ง คือประโยคที่ได้มาจากการนำสัจนิรันดร์ของตรรกศาสตร์เชิงประพจน์มาแทนที่ตัวแปรเชิงประพจน์แต่ละตัวด้วยสูตรลำดับที่หนึ่งอย่างสม่ำเสมอ (หนึ่งสูตรต่อตัวแปรเชิงประพจน์หนึ่งตัว) ตัวอย่างเช่น เนื่องจาก${\displaystyle A\lor \lnot A}$เป็นสัจพจน์ของตรรกศาสตร์เชิงประพจน์${\displaystyle (\forall x(x=x))\lor (\lnot \forall x(x=x))}$เป็นสัจนิรันดร์ในตรรกศาสตร์อันดับหนึ่ง ในทำนองเดียวกัน ในภาษาตรรกศาสตร์อันดับหนึ่งที่มีสัญลักษณ์ความสัมพันธ์เอกภาคR , S , Tประโยคต่อไปนี้เป็นสัจนิรันดร์:

${\displaystyle (((\exists xRx)\land \lnot (\exists xSx))\to \forall xTx)\Leftrightarrow ((\exists xRx)\to ((\lnot \exists xSx)\to \forall xTx)).}$

ได้มาจากการเปลี่ยน${\displaystyle A}$กับ${\displaystyle \exists xRx}$,${\displaystyle B}$กับ${\displaystyle \lnot \exists xSx}$, และ${\displaystyle C}$กับ${\displaystyle \forall xTx}$ในสัจนิรันดร์เชิงประพจน์:${\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}$.

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

${\displaystyle \neg \neg A\to A}$

• Bocheński, JM (1959) บทสรุปตรรกศาสตร์คณิตศาสตร์แปลจากฉบับภาษาฝรั่งเศสและเยอรมันโดย Otto Bird, Dordrecht , South Holland : D. Reidel .
• เอ็นเดอร์ตัน, เอชบี (2002) บทนำทางคณิตศาสตร์สู่ตรรกศาสตร์สำนัก พิมพ์ ฮาร์คอร์ต / สำนักพิมพ์วิชาการ ISBN 0-12-238452-0.
• Kleene, SC (1967) ตรรกศาสตร์ทางคณิตศาสตร์พิมพ์ซ้ำปี 2002 สำนักพิมพ์ Dover ISBN 0-486-42533-9.
• ไรเชนบัค, เอช. (1947). องค์ประกอบของตรรกศาสตร์เชิงสัญลักษณ์พิมพ์ซ้ำ 1980, โดเวอร์, ISBN 0-486-24004-5
• วิตเกนสไตน์, แอล. (1921). "Logisch-philosophiche Abhandlung", Annalen der Naturphilosophie (ไลพ์ซิก), v. 14, หน้า 185–262 พิมพ์ซ้ำในการแปลภาษาอังกฤษในชื่อTractatus logico-philosophicus , New York City and London , 1922

• "สัจพจน์" , สารานุกรมคณิตศาสตร์ , EMS Press , 2001 [1994]