• Top
  • Documentation
    • Xdoc
    • ACL2-doc
    • Recursion-and-induction
      • R-and-i-annotated-bibliography
      • R-and-i-definitions-revisited
      • R-and-i-terms
      • R-and-i-structural-induction
      • R-and-i-relations-between-recursion-and-induction
      • R-and-i-ordinals
      • R-and-i-inadequacies-of-structural-recursion
      • R-and-i-axioms
      • R-and-i-abbreviations-for-terms
      • R-and-i-terms-as-formulas
      • R-and-i-more-problems
      • R-and-i-still-more-problems
      • R-and-i-definitional-principle
      • R-and-i-function-definitions
      • R-and-i-introduction
      • R-and-i-table-of-contents
      • R-and-i-substitutions
      • R-and-i-arithmetic
        • R-and-i-ACL2-arithmetic
        • R-and-i-peano-arithmetic
      • R-and-i-induction-principle
      • R-and-i-data-types
      • R-and-i-more-inadequacies-of-the-definitional-principle
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Recursion-and-induction

R-and-i-arithmetic

Recursion and Induction: Arithmetic

We will next discuss arithmetic, in two steps. First, we'll challenge you to use what we have already got to define “natural numbers” (non-negative integers) and the elementary operations on them. This is called “Peano” arithmetic after the 19th century Italian mathematician Giuseppe Peano who first wrote down formal axioms describing the natural numbers.

After you've explored the foundations of arithmetic, we'll talk about briefly about the more familiar arithmetic of integers and rationals.

Next: Peano Arithmetic (or Table of Contents)

Subtopics

R-and-i-ACL2-arithmetic

Recursion and Induction: ACL2 Arithmetic

R-and-i-peano-arithmetic

Recursion and Induction: Peano Arithmetic