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

คำย่อwffออกเสียงว่า "woof" หรือบางครั้ง "wiff", "weff" หรือ "whiff" ^{[ 12 ]}

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

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

แม้ว่าคำว่า "สูตร" อาจใช้กับเครื่องหมายที่เขียน (เช่น บนกระดาษหรือกระดานดำ) แต่ความหมายที่แม่นยำกว่าคือลำดับของสัญลักษณ์ที่แสดงออกมา โดยเครื่องหมายเป็นเพียงตัวอย่างหนึ่งของสูตร ความแตกต่างระหว่างแนวคิดที่คลุมเครือของ "คุณสมบัติ" และแนวคิดที่กำหนดโดยการอุปนัยของสูตรที่มีรูปแบบดีนั้นมีรากฐานมาจากบทความของWeyl ในปี 1910 เรื่อง "Über die Definitionen der mathematischen Grundbegriffe" ^{[ 13 ]}ดังนั้นสูตรเดียวกันอาจถูกเขียนมากกว่าหนึ่งครั้ง และในทางทฤษฎีแล้วสูตรอาจยาวมากจนไม่สามารถเขียนได้เลยภายในจักรวาลทางกายภาพ

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

สูตรของแคลคูลัสเชิงประพจน์หรือที่เรียกว่า^สูตรเชิงประพจน์ [ ^{14 ]}เป็นนิพจน์เช่นนิยามของสูตรเริ่มต้นด้วยการเลือกเซตVของ ตัวแปรเชิงประพจน์โดยพลการ อักษรประกอบด้วยตัวอักษรในVพร้อมกับสัญลักษณ์สำหรับตัวเชื่อมเชิงประพจน์และวงเล็บ "(" และ ")" ซึ่งถือว่าไม่อยู่ในVสูตรจะเป็นนิพจน์บางอย่าง (นั่นคือสตริงของสัญลักษณ์) บนอักษรนี้ ${\displaystyle (A\land (B\lor C))}$

สูตรเหล่านี้ได้ รับการกำหนด แบบอุปนัยดังต่อไปนี้:

• ตัวแปรเชิงประพจน์แต่ละตัวนั้น ในตัวของมันเองเป็นสูตร
• ถ้า φ เป็นสูตรแล้ว ¬φ ก็เป็นสูตรเช่นกัน
• ถ้า φ และ ψ เป็นสูตร และ • เป็นตัวเชื่อมไบนารีใดๆ แล้ว ( φ • ψ) ก็เป็นสูตรเช่นกัน โดยที่ • อาจเป็น (แต่ไม่จำกัดเพียง) ตัวดำเนินการทั่วไป เช่น ∨, ∧, → หรือ ↔

นิยามนี้สามารถเขียนเป็นไวยากรณ์เชิงรูปธรรมในรูปแบบ Backus–Naur ได้เช่นกัน โดยมีเงื่อนไขว่าเซตของตัวแปรต้องมีจำนวนจำกัด:

< ชุดอัลฟา> ::= p | q | r | s | t | u | ... (เซตจำกัดของตัวแปรเชิงประพจน์ที่กำหนดขึ้นเอง) < รูปแบบ> ::= < ชุดอัลฟา> | ¬ < รูป แบบ> | ( < รูปแบบ> ∧ < รูปแบบ> ) | ( < รูปแบบ> ∨ < รูปแบบ> ) | ( < รูปแบบ> → < รูปแบบ> ) | ( < รูปแบบ> ↔ < รูปแบบ> ) 

เมื่อใช้ไวยากรณ์นี้ ลำดับของสัญลักษณ์

((( p → q ) ∧ ( r → s )) ∨ (¬ q ∧ ¬ s ))

เป็นสูตร เพราะถูกต้องตามหลักไวยากรณ์ ลำดับของสัญลักษณ์

(( p → q )→( qq )) p ))

ไม่ใช่สูตรสำเร็จ เพราะไม่สอดคล้องกับหลักไวยากรณ์

สูตรที่ซับซ้อนอาจอ่านยาก เช่น เนื่องจากมีวงเล็บจำนวนมาก เพื่อลดปัญหานี้ จึงมีการกำหนดกฎลำดับความสำคัญ (คล้ายกับลำดับการดำเนินการทางคณิตศาสตร์มาตรฐาน ) ระหว่างตัวดำเนินการ ทำให้ตัวดำเนินการบางตัวมีผลผูกพันมากกว่าตัวอื่น ตัวอย่างเช่น หากกำหนดลำดับความสำคัญ (จากมีผลผูกพันมากที่สุดไปน้อยที่สุด) คือ 1. ¬ 2. → 3. ∧ 4. ∨ ดังนั้นสูตรจะเป็นดังนี้

((( p → q ) ∧ ( r → s )) ∨ (¬ q ∧ ¬ s ))

อาจย่อได้ดังนี้

p → q ∧ r → s ∨ ¬ q ∧ ¬ s

อย่างไรก็ตาม นี่เป็นเพียงข้อตกลงที่ใช้เพื่อลดความซับซ้อนของการเขียนสูตรเท่านั้น หากสมมติว่าลำดับความสำคัญเป็นแบบสลับซ้ายขวา ตามลำดับดังนี้ 1. ¬ 2. ∧ 3. ∨ 4. → ​​แล้วสูตรเดียวกันข้างต้น (โดยไม่มีวงเล็บ) จะถูกเขียนใหม่เป็น

( p → ( q ∧ r )) → ( s ∨ (¬ q ∧ ¬ s ))

นิยามของสูตรในตรรกศาสตร์อันดับหนึ่ง นั้นสัมพันธ์กับลายเซ็นของทฤษฎีนั้นๆ ลายเซ็นนี้ระบุสัญลักษณ์ค่าคงที่ สัญลักษณ์ภาคแสดง และสัญลักษณ์ฟังก์ชันของทฤษฎีนั้นๆ รวมถึงจำนวนอาร์กิวเมนต์ของสัญลักษณ์ฟังก์ชันและสัญลักษณ์ภาคแสดงด้วย ${\displaystyle {\mathcal {QS}}}$

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

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

ขั้นตอนต่อไปคือการกำหนดสูตร อะตอม

1. ถ้าt ₁และt ₂เป็นเทอมแล้วt ₁ = t ₂จะเป็นสูตรอะตอม
2. ถ้าRเป็น สัญลักษณ์ภาคแสดงแบบ n -ary และt ₁ ,..., t _nเป็นเทอม แล้วR ( t ₁ ,..., t _n ) จะเป็นสูตรอะตอมิก

สุดท้ายนี้ เซตของสูตรจะถูกกำหนดให้เป็นเซตที่เล็กที่สุดที่บรรจุเซตของสูตรอะตอมิก โดยที่เงื่อนไขต่อไปนี้เป็นจริง:

1. ${\displaystyle \neg \phi }$เป็นสูตรเมื่อใดที่เป็นสูตร${\displaystyle \phi }$
2. ${\displaystyle (\phi \land \psi )}$และเป็นสูตรเมื่อและเป็นสูตร${\displaystyle (\phi \lor \psi )}$${\displaystyle \phi }$${\displaystyle \psi }$
3. ${\displaystyle \exists x\,\phi }$เป็นสูตรเมื่อเป็นตัวแปร และเป็นสูตร${\displaystyle x}$${\displaystyle \phi }$
4. ${\displaystyle \forall x\,\phi }$เป็นสูตรเมื่อเป็นตัวแปร และเป็นสูตร (หรืออาจนิยามได้ว่าเป็นตัวย่อของ)${\displaystyle x}$${\displaystyle \phi }$${\displaystyle \forall x\,\phi }$${\displaystyle \neg \exists x\,\neg \phi }$

ถ้าสูตรไม่มีการใช้หรือสำหรับตัวแปรใดๆเลย สูตรนั้นจะเรียกว่า${\displaystyle \exists x}$${\displaystyle \forall x}$${\displaystyle x}$สูตรเชิงการมีอยู่ (Existential formula ) คือสูตรที่เริ่มต้นด้วยลำดับของการระบุปริมาณเชิงการมีอยู่ ตามด้วยสูตรที่ปราศจากตัวบ่งปริมาณ

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

ตามศัพท์เฉพาะบางประการสูตรเปิดเกิดจากการรวมสูตรอะตอมโดยใช้ตัวเชื่อมตรรกะเท่านั้น โดยไม่รวมตัวบ่งปริมาณ^{[ 15 ]}ซึ่งไม่ควรสับสนกับสูตรที่ไม่ปิด

สูตรปิดหรือเรียกอีกอย่างว่าสูตรพื้นฐานหรือประโยคคือ สูตรที่ไม่มีการปรากฏอย่างอิสระของตัวแปร ใดๆ ถ้าAเป็นสูตรของภาษาลำดับที่หนึ่งซึ่งตัวแปรv ₁ , …, v _n มีการ ปรากฏ อย่างอิสระแล้วAที่นำหน้าด้วย∀ v ₁ ⋯ ∀ v _nจะเป็นการปิดแบบสากลของA

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

ในงานก่อนหน้านี้เกี่ยวกับตรรกะทางคณิตศาสตร์ (เช่น โดยChurch ^{[ 16 ]} ) สูตรต่างๆ หมายถึงสตริงของสัญลักษณ์ใดๆ และในบรรดาสตริงเหล่านี้ สูตรที่ถูกต้องคือสตริงที่ปฏิบัติตามกฎการสร้างสูตร (ที่ถูกต้อง)

ผู้เขียนหลายคนใช้คำว่าสูตรเฉยๆ^{[ 17 ] [ 18 ] [ 19 ] [ 20 ]}การใช้งานสมัยใหม่ (โดยเฉพาะในบริบทของวิทยาศาสตร์คอมพิวเตอร์กับซอฟต์แวร์ทางคณิตศาสตร์ เช่นตัวตรวจสอบแบบจำลอง ตัวพิสูจน์ทฤษฎีบทอัตโนมัติตัวพิสูจน์ทฤษฎีบทแบบโต้ตอบ ) มักจะคงแนวคิดของสูตรไว้เฉพาะในแง่ของพีชคณิต และปล่อยให้คำถามเกี่ยวกับความถูกต้องสมบูรณ์ กล่าวคือ การแสดงสูตรในรูปแบบสตริงที่เป็นรูปธรรม (การใช้สัญลักษณ์นี้หรือสัญลักษณ์นั้นสำหรับตัวเชื่อมและตัวบ่งปริมาณ การใช้ ข้อกำหนดการจัดวงเล็บนี้หรือข้อกำหนดนั้นการใช้ สัญกรณ์ แบบ Polishหรือinfixเป็นต้น) เป็นเพียงปัญหาด้านสัญกรณ์เท่านั้น

วลี "สูตรที่จัดทำอย่างดี" (WFF) ก็แทรกซึมเข้าสู่วัฒนธรรมสมัยนิยมเช่นกันWFFเป็นส่วนหนึ่งของการเล่นคำเชิงปรัชญาที่ใช้ในชื่อเกมวิชาการ " WFF 'N PROOF : The Game of Modern Logic" โดย Layman Allen ^{[ 21 ]}ซึ่งพัฒนาขึ้นขณะที่เขาอยู่ที่คณะนิติศาสตร์ มหาวิทยาลัยเยล (ต่อมาเขาเป็นศาสตราจารย์ที่มหาวิทยาลัยมิชิแกน ) ชุดเกมนี้ได้รับการออกแบบมาเพื่อสอนหลักการของตรรกะเชิงสัญลักษณ์แก่เด็ก ๆ (ในรูปแบบสัญกรณ์โปแลนด์ ) ^{[ 22 ]}ชื่อของมันเป็นเสียงสะท้อนของwhiffenpoofซึ่งเป็นคำที่ไม่มีความหมายที่ใช้เป็น คำ เชียร์ที่มหาวิทยาลัยเยลซึ่งได้รับความนิยมจากเพลง The Whiffenpoof SongและThe Whiffenpoofs ^{[ 23 ]}

• การแสดงออกบนพื้นดิน
• การแสดงออกที่ชัดเจน
• ภาษาทางการ
• อภิธานศัพท์ตรรกศาสตร์
• WFF 'N Proof

• สูตรสำเร็จรูปสำหรับตรรกศาสตร์ภาคแสดงอันดับแรก - พร้อมแบบทดสอบJava สั้นๆ
• สูตรสำเร็จรูปที่ ProvenMath