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

EFA เป็นระบบตรรกะที่อ่อนแอมาก ซึ่งมีลำดับเชิงทฤษฎีการพิสูจน์คือแต่ก็ยังดูเหมือนจะสามารถพิสูจน์คณิตศาสตร์ทั่วไปส่วนใหญ่ที่สามารถกล่าวได้ในภาษาของเลขคณิต อันดับหนึ่งได้${\displaystyle \omega ^{3}}$

EFA เป็นระบบตรรกะลำดับที่หนึ่ง (ที่มีความเท่าเทียมกัน) ภาษาของระบบนี้ประกอบด้วย:

• ค่าคงที่สองค่า, ,${\displaystyle 0}$${\displaystyle 1}$
• การดำเนินการไบนารีสามอย่าง, , , ซึ่งโดยปกติจะเขียนเป็น,${\displaystyle +}$${\displaystyle \times }$${\displaystyle {\textrm {exp}}}$${\displaystyle {\textrm {exp}}(x,y)}$${\displaystyle x^{y}}$
• สัญลักษณ์ความสัมพันธ์แบบไบนารี(อันนี้ไม่จำเป็นจริงๆ เพราะสามารถเขียนในรูปของการดำเนินการอื่นๆ ได้ และบางครั้งก็ละเว้นไป แต่สะดวกสำหรับการกำหนดตัวบ่งปริมาณแบบมีขอบเขต)${\displaystyle <}$

ตัวบ่งปริมาณแบบมีขอบเขตคือตัวบ่งปริมาณที่มีรูปแบบและซึ่งเป็นตัวย่อของและในลักษณะปกติ ${\displaystyle \forall (x<y)}$${\displaystyle \exists (x<y)}$${\displaystyle \forall x(x<y)\rightarrow \ldots }$${\displaystyle \exists x(x<y)\land \ldots }$

หลักการพื้นฐานของ EFA คือ

• สัจพจน์ของเลขคณิตโรบินสันสำหรับ, , , ,${\displaystyle 0}$${\displaystyle 1}$${\displaystyle +}$${\displaystyle \times }$${\displaystyle <}$
• สัจพจน์สำหรับการยกกำลัง: , .${\displaystyle x^{0}=1}$${\displaystyle x^{y+1}=x^{y}\times x}$
• การอุปมานสำหรับสูตรที่มีตัวบ่งปริมาณทั้งหมดอยู่ในขอบเขตจำกัด (แต่สูตรอาจมีตัวแปรอิสระ )

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

ข้อความต้นฉบับของการคาดการณ์จากฟรีดแมน (1999)คือ:

"ทฤษฎีบททุกข้อที่ตีพิมพ์ในวารสารคณิตศาสตร์ซึ่งข้อความของทฤษฎีบทนั้นเกี่ยวข้องกับวัตถุทางคณิตศาสตร์ที่มีขอบเขตจำกัดเท่านั้น (กล่าวคือ สิ่งที่นักตรรกศาสตร์เรียกว่าข้อความทางเลขคณิต) สามารถพิสูจน์ได้ใน EFA (Electronic Functional Affect) EFA เป็นส่วนย่อยที่อ่อนแอของเลขคณิตของ Peanoโดยอาศัยสัจพจน์ที่ไม่มีตัวบ่งปริมาณตามปกติสำหรับ 0, 1, +, ×, exp พร้อมด้วยแผนการอุปนัยสำหรับสูตรทั้งหมดในภาษาที่มีตัวบ่งปริมาณทั้งหมดที่มีขอบเขตจำกัด"

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

กลุ่มความซับซ้อนในการคำนวณที่เกี่ยวข้องหลายกลุ่มมีคุณสมบัติคล้ายคลึงกับ EFA:

• เราสามารถละเว้นสัญลักษณ์ฟังก์ชันไบนารี exp จากภาษาได้ โดยใช้เลขคณิตของโรบินสันร่วมกับการอุปมานสำหรับสูตรทั้งหมดที่มีตัวบ่งปริมาณที่จำกัด และสัจพจน์ที่ระบุคร่าวๆ ว่าการยกกำลังเป็นฟังก์ชันที่นิยามได้ทุกที่ วิธีนี้คล้ายกับ EFA และมีความแข็งแกร่งทางทฤษฎีการพิสูจน์เช่นเดียวกัน แต่ใช้งานยากกว่า
• มีเศษส่วนที่อ่อนแอของเลขคณิตอันดับสองที่เรียกว่าและซึ่งอนุรักษ์ไว้เหนือ EFA สำหรับประโยค (เช่นประโยคใด ๆ ที่พิสูจน์โดยหรือได้รับการพิสูจน์โดย EFA แล้ว) ^{[ 2 ]}โดยเฉพาะอย่างยิ่ง พวกมันจะอนุรักษ์ไว้สำหรับข้อความที่สอดคล้องกัน บางครั้งเศษส่วนเหล่านี้ได้รับการศึกษาในคณิตศาสตร์ย้อนกลับ ( Simpson 2009 )${\displaystyle {\mathsf {RCA}}_{0}^{*}}$${\displaystyle {\mathsf {WKL}}_{0}^{*}}$${\displaystyle \Pi _{2}^{0}}$${\displaystyle \Pi _{2}^{0}}$${\displaystyle {\mathsf {RCA}}_{0}^{*}}$${\displaystyle {\mathsf {WKL}}_{0}^{*}}$
• เลขคณิตเวียนเกิดพื้นฐาน ( ERA ) เป็นระบบย่อยของเลขคณิตเวียนเกิดดั้งเดิม (PRA) ซึ่งการเวียนเกิดถูกจำกัดไว้เฉพาะผลบวกและผลคูณที่มีขอบเขตนอกจากนี้ยังมีประโยคเดียวกันกับ EFA ในแง่ที่ว่าเมื่อใดก็ตามที่ EFA พิสูจน์ได้ว่า ∀x∃y P ( x , y ) โดยที่Pไม่มีตัวบ่งปริมาณ ERA ก็จะพิสูจน์ได้ว่าสูตรเปิดP ( x , T ( x )) โดยที่Tเป็นเทอมที่สามารถนิยามได้ใน ERA เช่นเดียวกับ PRA ERA สามารถนิยามได้โดยไม่ต้องใช้ตรรกะใดๆ เลย โดยใช้เพียงกฎของการแทนที่และการอุปมาน และสมการนิยามสำหรับฟังก์ชันเวียนเกิดพื้นฐานทั้งหมด อย่างไรก็ตาม แตกต่างจาก PRA ฟังก์ชันเวียนเกิดพื้นฐานสามารถระบุลักษณะได้โดยการปิดภายใต้การประกอบและการฉายภาพของ ฟังก์ชันพื้นฐานจำนวน จำกัดดังนั้นจึงต้องการเพียงสมการนิยามจำนวนจำกัดเท่านั้น${\displaystyle \Pi _{2}^{0}}$

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