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

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