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

แหล่งที่มาของส่วนนี้ รวมถึงเนื้อหาส่วนใหญ่ในบทความนี้ คือ Quine (1976) Quine เสนอ PFL (Protocol Logic Functional Logic) เป็นวิธีการแปลงตรรกะอันดับหนึ่ง ให้เป็นพีชคณิต ในลักษณะที่คล้ายคลึงกับวิธีที่พีชคณิตบูลีนแปลงตรรกะเชิงประพจน์ ให้เป็น พีชคณิต เขาออกแบบ PFL ให้มีพลังในการแสดงออกเท่ากับตรรกะอันดับหนึ่งที่มีเอกลักษณ์ดังนั้นเมตาคณิตศาสตร์ของ PFL จึงเหมือนกับตรรกะอันดับหนึ่งที่ไม่มีตัวอักษรภาคแสดงที่ตีความได้ กล่าวคือ ตรรกะทั้งสองมีความ ถูก ต้องสมบูรณ์และไม่สามารถตัดสินได้งานส่วนใหญ่ที่ Quine ตีพิมพ์เกี่ยวกับตรรกะและคณิตศาสตร์ในช่วง 30 ปีสุดท้ายของชีวิตเขาเกี่ยวข้องกับ PFL ในทางใดทางหนึ่ง

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

"คำว่าfunctorซึ่งมีความหมายทางไวยากรณ์แต่มีความหมายเชิงตรรกะ... เป็นสัญลักษณ์ที่เชื่อมต่อกับสำนวนหนึ่งหรือมากกว่านั้นที่มีประเภทไวยากรณ์ที่กำหนด เพื่อสร้างสำนวนที่มีประเภทไวยากรณ์ที่กำหนด" (Quine 1982: 129)

นอกจากวิธี PFL แล้ว วิธีการอื่นๆ ในการแปลงตรรกะอันดับหนึ่ง ให้เป็นพีชคณิต ได้แก่:

• พีชคณิตทรงกระบอกโดยอัลเฟรด ทาร์สกีและนักศึกษาชาวอเมริกันของเขา พีชคณิตทรงกระบอกแบบง่ายที่เสนอโดยเบอร์เนย์ส (1959) ทำให้ควินเขียนบทความที่มีการใช้คำว่า "ฟังก์ชันภาคแสดง" เป็นครั้งแรก
• พีชคณิตพหุแอดิกของพอล ฮาลมอสด้วยคุณสมบัติของพรีมิทีฟและสัจพจน์ ที่ประหยัด ทำให้พีชคณิตนี้คล้ายคลึงกับ PFL มากที่สุด
• พีชคณิตความสัมพันธ์เป็นการแปลงส่วนหนึ่งของตรรกะลำดับที่หนึ่งที่ประกอบด้วยสูตรที่ไม่มีสูตรอะตอมิกอยู่ในขอบเขตของตัวบ่งปริมาณ มากกว่าสามตัวให้เป็นรูปแบบพีชคณิต อย่างไรก็ตาม ส่วนนั้นเพียงพอสำหรับเลขคณิตของพีอาโนและทฤษฎีเซตเชิงสัจพจน์ZFCดังนั้น พีชคณิตความสัมพันธ์จึงไม่สามารถเติมเต็มได้ ต่างจาก PFL งานส่วนใหญ่เกี่ยวกับพีชคณิตความสัมพันธ์ตั้งแต่ประมาณปี 1920 เป็นต้นมานั้นดำเนินการโดยทาร์สกีและนักเรียนชาวอเมริกันของเขา พลังของพีชคณิตความสัมพันธ์ไม่ได้ปรากฏชัดจนกระทั่งมีการตีพิมพ์งานวิจัยของทาร์สกีและกิแวนต์ (1987) ซึ่งตีพิมพ์หลังจากบทความสำคัญสามฉบับที่เกี่ยวข้องกับ PFL ได้แก่ เบคอน (1985), คูห์น (1983) และไควน์ (1976)
• ตรรกศาสตร์เชิงการจัดเรียงสร้างขึ้นจากตัวจัดเรียง (combinators)ซึ่งเป็นฟังก์ชันลำดับสูงที่ มี โดเมนเป็นตัวจัดเรียงหรือฟังก์ชันอื่น และมีเรนจ์เป็นตัวจัดเรียงอีกตัวหนึ่ง ดังนั้นตรรกศาสตร์เชิงการจัดเรียงจึงก้าวข้ามตรรกศาสตร์ลำดับแรกไปได้ด้วยพลังการแสดงออกของทฤษฎีเซตซึ่งทำให้ตรรกศาสตร์เชิงการจัดเรียงมีความเสี่ยงต่อความขัดแย้งในทางกลับกัน ฟังก์ชันแสดงภาคแสดง (predicate functor) เพียงแค่แปลงภาคแสดง (หรือเรียกว่าเทอม ) ไปเป็นภาคแสดง

PFL อาจกล่าวได้ว่าเป็นรูปแบบที่ง่ายที่สุดในบรรดารูปแบบเหล่านี้ แต่ก็เป็นรูปแบบที่มีการเขียนถึงน้อยที่สุดเช่นกัน

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

• จนกระทั่งDana Scottเริ่มเขียนเกี่ยวกับทฤษฎีแบบจำลองของตรรกะเชิงการจัดเรียงในปลายทศวรรษ 1960 แทบจะมีเพียงHaskell Curryนักเรียนของเขา และRobert Feysในเบลเยียมเท่านั้นที่ทำงานเกี่ยวกับตรรกะดังกล่าว
• การกำหนดสูตรสัจพจน์ที่น่าพอใจของตรรกศาสตร์เชิงการจัดเรียงนั้นเกิดขึ้นอย่างช้าๆ ในช่วงทศวรรษ 1930 พบว่าสูตรบางอย่างของตรรกศาสตร์เชิงการจัดเรียงนั้นไม่สอดคล้องกันนอกจากนี้ เคอร์รียังค้นพบปรากฏการณ์ขัดแย้งของเคอร์รีซึ่งเป็นลักษณะเฉพาะของตรรกศาสตร์เชิงการจัดเรียง อีกด้วย
• แคลคูลัสแลมบ์ดาซึ่งมีพลังในการแสดงออกเทียบเท่ากับตรรกศาสตร์เชิงการจัดเรียงถูกมองว่าเป็นรูปแบบทางคณิตศาสตร์ที่เหนือกว่า

ไวยากรณ์ PFL , ฟังก์ชันพื้นฐาน และสัจพจน์ที่อธิบายไว้ในส่วนนี้ส่วนใหญ่เป็นผลงานของSteven Kuhn (1983) ความหมายของฟังก์ชันย่อยเป็นผลงานของ Quine (1982) ส่วนที่เหลือของบทความนี้ได้นำคำศัพท์บางส่วนมาจาก Bacon (1985)

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

ฟังก์ชันบ่งชี้แบบ "เชิงผสม" (คำนี้เป็นของ Quine) ซึ่งทั้งหมดเป็นแบบเอกภาคและเป็นเอกลักษณ์เฉพาะของ PFL ได้แก่Inv , inv , ∃ , +และpเทอมอาจเป็นเทอมอะตอมิก หรือสร้างขึ้นโดยกฎเวียนเกิดต่อไปนี้ ถ้า τ เป็นเทอมแล้วInv τ, inv τ, ∃ τ, + τ และp τ ก็เป็นเทอมเช่นกัน ฟังก์ชันที่มีตัวยกnโดยที่ nเป็นจำนวนธรรมชาติ > 1 หมายถึงการประยุกต์ใช้ (การวนซ้ำ) ของฟังก์ชันนั้นติดต่อกัน n ครั้ง

สูตรคือเทอมหรือถูกกำหนดโดยกฎเวียนเกิด: ถ้า α และ β เป็นสูตรแล้ว αβ และ ~(α) ก็เป็นสูตรเช่นกัน ดังนั้น "~" จึงเป็นฟังก์ชันเอกนามอีกตัวหนึ่ง และการเชื่อมต่อเป็นฟังก์ชันภาคแสดงทวินามเพียงอย่างเดียว Quine เรียกฟังก์ชันเหล่านี้ว่า "อาเลธิก" การตีความตามธรรมชาติของ "~" คือการปฏิเสธส่วนการเชื่อมต่อคือตัวเชื่อม ใดๆ ที่เมื่อรวมกับการปฏิเสธแล้ว จะสร้าง ชุดตัวเชื่อม ที่สมบูรณ์ในเชิงฟังก์ชัน ชุดที่สมบูรณ์ในเชิงฟังก์ชันที่ Quine ชื่นชอบคือการเชื่อมโยงและการปฏิเสธดังนั้นเทอมที่เชื่อมต่อกันจึงถือว่าเป็นการเชื่อมโยงกัน สัญลักษณ์+เป็นของ Bacon (1985) ส่วนสัญลักษณ์อื่นๆ เป็นของ Quine (1976; 1982) ส่วนอาเลธิกของ PFL นั้นเหมือนกับแบบแผนเทอมบูลีนของ Quine (1982)

ดังที่ทราบกันดี ฟังก์ชันเชิงตรรกะสองตัวสามารถแทนที่ด้วยฟังก์ชันเชิงคู่ตัวเดียวที่มีไวยากรณ์และความหมาย ดังต่อไปนี้ : ถ้า α และ β เป็นสูตรแล้ว (αβ) ก็เป็นสูตรที่มีความหมายว่า "ไม่ใช่ (α และ/หรือ β)" (ดูNANDและNOR )

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

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

ความหมายเชิงนามธรรมของ Quine (1982) สำหรับฟังก์ชันภาคแสดงแต่ละตัวจะระบุไว้ด้านล่างโดยใช้สัญลักษณ์การสร้างเซต (set builder notation) ตามด้วยสัจพจน์ที่เกี่ยวข้องจาก Kuhn (1983) หรือคำนิยามจาก Quine (1976) สัญลักษณ์นี้หมายถึงเซตของn -tupleที่สอดคล้องกับสูตรอะตอมิก${\displaystyle \{x_{1}\cdots x_{n}:Fx_{1}\cdots x_{n}\}}$${\displaystyle Fx_{1}\cdots x_{n}.}$

• อัตลักษณ์ ( I ) ถูกนิยามว่า:

${\displaystyle IFx_{1}x_{2}\cdots x_{n}\leftrightarrow (Fx_{1}x_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{2}\cdots x_{n}){\text{.}}}$

เอกลักษณ์นี้เป็นแบบสะท้อนกลับ ( Ixx ) สมมาตร ( Ixy → Iyx ) ถ่ายทอดได้ ( ( Ixy ∧ Iyz ) → Ixz ) และเป็นไปตามคุณสมบัติการแทนที่:

${\displaystyle (Fx_{1}\cdots x_{n}\land Ix_{1}y)\rightarrow Fyx_{2}\cdots x_{n}.}$

• การเพิ่มค่าว่าง (Padding) , + , จะเพิ่มตัวแปรทางด้านซ้ายของรายการอาร์กิวเมนต์ใดๆ

${\displaystyle \ +F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{0}x_{1}\cdots x_{n}:F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle +Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}\cdots x_{n}.}$

• การตัดขอบ (Cropping) , ∃ , จะลบตัวแปรซ้ายสุดในรายการอาร์กิวเมนต์ใดๆ ก็ตาม

${\displaystyle \exists F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:\exists x_{1}F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle Fx_{1}\cdots x_{n}\rightarrow \exists Fx_{2}\cdots x_{n}.}$

การตัดขอบช่วยให้สามารถใช้ฟังก์ชันที่กำหนดไว้สองแบบที่มีประโยชน์ได้:

• การสะท้อน , S :

${\displaystyle SF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:F^{n}x_{2}x_{2}\cdots x_{n}\}.}$

${\displaystyle SF^{n}\leftrightarrow \exists IF^{n}.}$

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

• ผลคูณคาร์ทีเซียน ,;${\displaystyle \times }$

${\displaystyle F^{m}\times G^{n}\leftrightarrow F^{m}\exists ^{m}G^{n}.}$

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

${\displaystyle F^{m}x_{1}\cdots x_{m}G^{n}x_{1}\cdots x_{n}\leftrightarrow (F^{m}\times G^{n})x_{1}\cdots x_{m}x_{1}\cdots x_{n}.}$

จัดเรียงลำดับรายการอาร์กิวเมนต์ที่ต่อกันใหม่ โดยย้ายตัวแปรที่ซ้ำกันสองตัวไปทางซ้ายสุด จากนั้นเรียกใช้ฟังก์ชันSเพื่อกำจัดตัวแปรที่ซ้ำกัน ทำซ้ำขั้นตอนนี้หลายครั้งตามที่ต้องการ จะทำให้ได้รายการอาร์กิวเมนต์ที่มีความยาวสูงสุดเท่ากับ max( m , n )

ฟังก์ชันสามตัวถัดไปนี้ช่วยให้สามารถจัดเรียงลำดับรายการอาร์กิวเมนต์ใหม่ได้ตามต้องการ

• การกลับลำดับตัวแปรหลัก(Inv ) จะหมุนตัวแปรในรายการอาร์กิวเมนต์ไปทางขวา เพื่อให้ตัวแปรตัวสุดท้ายกลายเป็นตัวแปรตัวแรก

${\displaystyle \operatorname {Inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{n}x_{1}\cdots x_{n-1}\}.}$

${\displaystyle \operatorname {Inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{n}x_{1}\cdots x_{n-1}.}$

• การสลับตำแหน่งย่อย (minor inversion ) หรือinvจะสลับตำแหน่งตัวแปรสองตัวแรกในรายการอาร์กิวเมนต์

${\displaystyle \operatorname {inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{2}x_{1}\cdots x_{n}\}.}$

${\displaystyle \operatorname {inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{1}\cdots x_{n}.}$

• การเรียงสับเปลี่ยน p จะหมุนตัวแปรตัวที่สองจากตัวสุดท้ายในรายการอาร์กิวเมนต์ไปทางซ้าย เพื่อให้ตัวแปรตัวที่สองกลายเป็นตัวสุดท้าย

${\displaystyle \ pF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{1}x_{3}\cdots x_{n}x_{2}\}.}$

${\displaystyle pFx_{1}\cdots x_{n}\leftrightarrow \operatorname {Inv} \operatorname {inv} Fx_{1}x_{3}\cdots x_{n}x_{2}.}$

เมื่อกำหนดรายการอาร์กิวเมนต์ที่ประกอบด้วย ตัวแปร nตัว ฟังก์ชันp จะถือว่าตัวแปร n −1 ตัว สุดท้ายเป็นเหมือนโซ่จักรยาน โดยแต่ละตัวแปรเป็นข้อต่อในโซ่ การใช้ฟังก์ชัน p หนึ่งครั้งจะ เลื่อนโซ่ไปหนึ่งข้อต่อ การใช้ฟังก์ชัน p ติดต่อกัน kครั้งกับF ⁿจะย้าย ตัวแปร k +1 ไปยังตำแหน่งอาร์กิวเมนต์ที่สองในF

เมื่อn = 2, Invและinv จะสลับตำแหน่งของ x ₁และx ₂เท่านั้นเมื่อn = 1, พวกมันจะไม่มีผลใดๆ ดังนั้นpจึงไม่มีผลเมื่อn < 3

Kuhn (1983) ถือว่าการผกผันหลักและการผกผันรองเป็นองค์ประกอบพื้นฐาน สัญลักษณ์pในงานของ Kuhn สอดคล้องกับinv ; เขาไม่มีสิ่งที่เทียบเคียงได้กับการเรียงสับเปลี่ยนดังนั้นจึงไม่มีสัจพจน์สำหรับมัน หากตาม Quine (1976) ถือว่า pเป็นองค์ประกอบพื้นฐานInvและinvสามารถนิยามได้ว่าเป็นการรวมกันที่ไม่ธรรมดาของ+ , ∃และpที่ ทำซ้ำ

ตารางต่อไปนี้สรุปว่าฟังก์ชันต่างๆ ส่งผลต่อระดับของอาร์กิวเมนต์อย่างไร

การแสดงออก	ระดับ
${\displaystyle p;\operatorname {Inv} ;\operatorname {inv} ;\ \lnot ;\ I}$	ไม่มีการเปลี่ยนแปลง
${\displaystyle +F^{n-1};\ \exists F^{n+1};\ SF^{n+1}}$	n
${\displaystyle \alpha ^{m}\beta ^{n};\ F^{m}\times G^{n}}$	สูงสุด( m , n )

ตัวอักษรแสดงภาคแสดงทุกตัวสามารถแทนที่ด้วยตัวอักษรแสดงภาคแสดงอื่นที่มีระดับเดียวกันได้โดยไม่กระทบต่อความถูกต้องกฎมีดังนี้:

• Modus ponens ;
• ให้αและβเป็นสูตร PFL ที่ไม่มี ปรากฏอยู่ ถ้าเป็นทฤษฎีบท PFL แล้ว ก็เป็นทฤษฎีบท PFL เช่นกัน${\displaystyle x_{1}}$${\displaystyle (\alpha \land Fx_{1}...x_{n})\rightarrow \beta }$${\displaystyle (\alpha \land \exists Fx_{2}...x_{n})\rightarrow \beta }$

แทนที่จะกำหนดสัจพจน์ให้กับ PFL นั้น Quine (1976) ได้เสนอข้อสันนิษฐานต่อไปนี้เป็นสัจพจน์ที่เป็นไปได้

${\displaystyle \exists I}$

การทำซ้ำ p ติดต่อกัน n −1 ครั้งจะคืนสถานะเดิมก่อนเกิดเหตุการณ์ :

${\displaystyle F^{n}\leftrightarrow p^{n-1}F^{n}}$

+และ∃หักล้างกันเอง:

${\displaystyle {\begin{cases}F^{n}\rightarrow +\exists F^{n}\\F^{n}\leftrightarrow \exists +F^{n}\end{cases}}}$

การปฏิเสธกระจายตัวเหนือ+ , ∃และp :

${\displaystyle {\begin{cases}+\lnot F^{n}\leftrightarrow \lnot +F^{n}\\\lnot \exists F^{n}\rightarrow \exists \lnot F^{n}\\p\lnot F^{n}\leftrightarrow \lnot pF^{n}\end{cases}}}$

+และpกระจายตัวเหนือการเชื่อมโยง:

${\displaystyle {\begin{cases}+(F^{n}G^{m})\leftrightarrow (+F^{n}+G^{m})\\p(F^{n}G^{m})\leftrightarrow (pF^{n}pG^{m})\end{cases}}}$

อัตลักษณ์มีความหมายที่น่าสนใจดังนี้:

${\displaystyle IF^{n}\rightarrow p^{n-2}\exists p+F^{n}}$

นอกจากนี้ Quine ยังตั้งข้อสันนิษฐานเกี่ยวกับกฎที่ว่า: ถ้าαเป็นทฤษฎีบท PFL แล้วpα , +αและ ก็เป็นทฤษฎีบท PFL เช่น กัน ${\displaystyle \lnot \exists \lnot \alpha }$

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

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

เบคอนยังมี:

• อภิปรายความสัมพันธ์ของ PFL กับตรรกศาสตร์เชิงคำศัพท์ของ Sommers (1982) และโต้แย้งว่าการปรับปรุง PFL โดยใช้ไวยากรณ์ที่เสนอในภาคผนวกของ Lockwood ใน Sommers จะทำให้ PFL อ่าน ใช้ และสอนได้ง่ายขึ้น
• กล่าวถึงโครงสร้างเชิงทฤษฎีกลุ่ม ของ Invและinv ;
• กล่าวถึงว่าตรรกศาสตร์ประโยค ตรรกศาสตร์ภาคแสดงเอกนามตรรกศาสตร์เชิงโมดอลS5และตรรกศาสตร์บูลีนของความสัมพันธ์ ที่ (ไม่) สลับตำแหน่ง ล้วน เป็นส่วนประกอบของ PFL

อัลกอริทึมต่อไปนี้ดัดแปลงมาจาก Quine (1976: 300–2) เมื่อกำหนดสูตรปิดของตรรกะลำดับที่หนึ่งแล้วให้ดำเนินการดังต่อไปนี้ก่อน:

• ให้ใส่ตัวเลขกำกับไว้ที่ตัวอักษรแสดงภาคแสดงทุกตัว เพื่อระบุระดับของภาคแสดงนั้น
• แปลง คำบ่งปริมาณสากลทั้งหมดให้เป็นคำบ่งปริมาณเชิงการมีอยู่และคำปฏิเสธ
• เขียน สูตรอะตอมทั้งหมดที่มีรูปแบบx = yใหม่เป็นIxy

ทีนี้ลองนำอัลกอริทึมต่อไปนี้ไปใช้กับผลลัพธ์ข้างต้น:

การแปลย้อนกลับจาก PFL ไปสู่ตรรกะลำดับที่หนึ่งนั้น มีการกล่าวถึงใน Quine (1976: 302–4)

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

• ตรรกศาสตร์เชิงพีชคณิต

• บทนำเกี่ยวกับตรรกศาสตร์เชิงฟังก์ชันภาคแสดง (ดาวน์โหลดด้วยคลิกเดียว ไฟล์ PS) โดย Mats Dahllöf (ภาควิชาภาษาศาสตร์ มหาวิทยาลัยอุปซาลา)