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

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

ทีนี้ลองพิจารณาแบบจำลองของภาษาเชิงรูปธรรม โดยที่ชนิดTและUถูกจำลองโดยเซต [ T ] และ [ U ] และสัญลักษณ์X แต่ละตัว ของชนิดTถูกจำลองโดยองค์ประกอบ [ X ] ใน [ T ] จากนั้นFสามารถจำลองได้ด้วยเซต

${\displaystyle [F]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \}},}$

ซึ่งเป็นเพียงฟังก์ชันที่มีโดเมน [ T ] และโคโดเมน [ U ] เป็นข้อกำหนดของแบบจำลองที่สอดคล้องกันว่า [ F ( X )] = [ F ( Y )] เมื่อใดก็ตามที่ [ X ] = [ Y ]

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

นอกจากนี้ เรายังได้สัญลักษณ์ฟังก์ชันบางอย่างโดยอัตโนมัติ ในตรรกะที่ไม่ระบุประเภท จะมีตัวบ่งชี้เอกลักษณ์ id ที่สอดคล้องกับ id( X ) = XสำหรับทุกXในตรรกะที่ระบุประเภท เมื่อกำหนดประเภทT ใดๆ จะมีตัวบ่งชี้เอกลักษณ์ idT _ที่มีโดเมนและโคโดเมนเป็นประเภทTซึ่งจะสอดคล้องกับ idT ₍ X ) = XสำหรับทุกXที่มีประเภทTในทำนองเดียวกัน ถ้าTเป็นประเภทย่อยของUก็จะมีตัวบ่งชี้การรวมที่มีโดเมนเป็นประเภทTและโคโดเมนเป็นประเภทUที่สอดคล้องกับสมการเดียวกัน นอกจากนี้ยังมีสัญลักษณ์ฟังก์ชันเพิ่มเติมที่เกี่ยวข้องกับวิธีการอื่นๆ ในการสร้างประเภทใหม่จากประเภทเก่า

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

สำหรับX ทุกตัว ที่เป็นประเภทTและสำหรับY บางตัวที่ไม่ซ้ำกัน ที่เป็นประเภทU , P ( X , Y )

จากนั้นคุณสามารถแนะนำสัญลักษณ์ฟังก์ชันFที่มีประเภทโดเมนTและประเภทโคโดเมนUที่ตรงตามเงื่อนไขต่อไปนี้:

สำหรับX ทุกตัว ที่เป็นประเภทTและสำหรับY ทุกตัว ที่เป็นประเภทU , P ( X , Y ) ก็ต่อเมื่อY = F ( X ) เท่านั้น

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

โดยเฉพาะอย่างยิ่ง ถ้าFมีประเภทโดเมนTและประเภทโคโดเมนUแล้ว มันสามารถแทนที่ด้วย述语Pที่มีประเภท ( T , U ) ได้ โดยสัญชาตญาณแล้วP ( X , Y ) หมายถึงF ( X ) = Yดังนั้น เมื่อใดก็ตามที่F ( X ) ปรากฏในประโยค คุณสามารถแทนที่ด้วยสัญลักษณ์ใหม่Yที่มีประเภทUและรวมประโยคอื่นP ( X , Y ) เข้าไปด้วย เพื่อให้สามารถทำการอนุมานแบบเดียวกันได้ คุณจำเป็นต้องมีข้อเสนอเพิ่มเติม:

สำหรับX ทุกตัว ที่เป็นประเภทTสำหรับY บางตัว ที่ไม่ซ้ำกัน ที่เป็นประเภทU , P ( X , Y )

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

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

ลองพิจารณาแบบแผนสัจพจน์ของการแทนที่ในทฤษฎีเซตของ Zermelo–Fraenkel เป็นตัวอย่าง (ตัวอย่างนี้ใช้สัญลักษณ์ทางคณิตศาสตร์ ) แบบแผนนี้ระบุไว้ (ในรูปแบบหนึ่ง) สำหรับตัวบ่งชี้เชิงฟังก์ชันF ใดๆ ในตัวแปรเดียวว่า:

${\displaystyle \forall A,\exists B,\forall C,C\in A\rightarrow F(C)\in B.}$

ขั้นแรก เราต้องแทนที่F ( C ) ด้วยตัวแปรอื่นD :

${\displaystyle \forall A,\exists B,\forall C,C\in A\rightarrow D\in B.}$

แน่นอนว่าข้อความนี้ไม่ถูกต้องDต้องถูกกำหนดปริมาณหลังจากC :

${\displaystyle \forall A,\exists B,\forall C,\forall D,C\in A\rightarrow D\in B.}$

เรายังคงต้องแนะนำPเพื่อป้องกันการกำหนดปริมาณนี้:

${\displaystyle \forall A,\exists B,\forall C,\forall D,P(C,D)\rightarrow (C\in A\rightarrow D\in B).}$

นี่เกือบถูกต้องแล้ว แต่ใช้ได้กับเงื่อนไขมากเกินไป สิ่งที่เราต้องการจริงๆ คือ:

${\displaystyle (\forall X,\exists !Y,P(X,Y))\rightarrow (\forall A,\exists B,\forall C,\forall D,P(C,D)\rightarrow (C\in A\rightarrow D\in B)).}$

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

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

ตัวอย่างเช่น ฟังก์ชันที่ไม่ได้รับการตีความสำหรับSMT-LIBหากป้อนข้อมูลนี้ให้กับตัวแก้ปัญหา SMT :

(ประกาศฟังก์ชัน f (Int) Int) (ยืนยัน (= (f 10) 1)) 

ตัวแก้ปัญหา SMT จะส่งคืน "อินพุตนี้สามารถหาคำตอบได้" เนื่องจากfเป็นฟังก์ชันที่ไม่ได้รับการตีความ (กล่าวคือ สิ่งที่ทราบเกี่ยวกับfฟังก์ชันมี เพียงแค่รูปแบบการแสดงผล เท่านั้น) ดังนั้นจึงเป็นไปได้ที่f(10) = 1แต่เมื่อใช้ข้อมูลอินพุตด้านล่าง:

(ประกาศฟังก์ชัน f (Int) Int) (ยืนยัน (= (f 10) 1)) (ยืนยัน (= (f 10) 42)) 

ตัวแก้ปัญหา SMT จะส่งคืนข้อความ "ไม่สามารถหาคำตอบของอินพุตนี้ได้" เนื่องจากfเป็นฟังก์ชัน จึงไม่สามารถส่งคืนค่าที่แตกต่างกันสำหรับอินพุตเดียวกันได้

ปัญหาการตัดสินใจสำหรับทฤษฎีอิสระมีความสำคัญเป็นพิเศษ เนื่องจากทฤษฎีจำนวนมากสามารถลดทอนได้ด้วยทฤษฎีนี้^{[ 2 ]}

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

• ประเภทข้อมูลพีชคณิต
• พีชคณิตเบื้องต้น
• ตัวเชื่อมตรรกะ
• ค่าคงที่ตรรกะ
• พีชคณิตเทอม
• ทฤษฎีความเท่าเทียมบริสุทธิ์