Skip to content

First-Order Arithmetic

Formal first-order theories of natural-number arithmetic defined by a signature, axioms, models, and a specified induction scheme.

Version
v1 · 2026-09-28 · History
Domain-specific #
9472
Domain group
Formal Sciences
Origin domain
Mathematics
Subdomains
Mathematical Logic, Theories of Arithmetic → Mathematics
Aliases
First-order theories of arithmetic

Core Idea

First-order arithmetic comprises formal theories in a first-order language for natural-number structures, using symbols for zero, successor, arithmetic operations, and relations together with specified axioms and induction strength.

Peano arithmetic uses first-order axioms plus an induction scheme for formulas in its language. Robinson arithmetic keeps basic operation axioms but lacks full induction, illustrating a weaker theory.

Structural Signature

Sig role-phrases:

  • Signature — Lists zero, successor, operations, and relations. It is syntax. Counterfactual: Different signatures express different formulas.
  • Formulas — Build statements with first-order quantifiers. It is language. Counterfactual: Second-order set quantification changes the logic.
  • Axioms — Constrain intended arithmetic behavior. It is theory. Counterfactual: A language alone is not a theory.
  • Models — Interpret symbols in structures satisfying axioms. It is semantics. Counterfactual: Nonstandard models matter in first-order theories.
  • Induction scheme — Controls which formulas support induction. It is strength. Counterfactual: Removing or restricting it changes proof power.
  • Proof relation — Derives theorems by first-order rules. It is inference. Counterfactual: Truth in the standard model and provability are distinct.

What It Is Not

  • It is not ordinary arithmetic practice.
  • It is not automatically Peano arithmetic.
  • It is not second-order arithmetic.
  • It is not identical to all truths of the standard natural numbers.
  • Closest near-miss. Presburger arithmetic is a first-order arithmetic theory but omits multiplication as a full operation and has different strength.

Scope of Application

  • Logic. Studies theories and models.
  • Foundations. Formalizes elementary number reasoning.
  • Proof theory. Compares induction strength.
  • Model theory. Analyzes nonstandard arithmetic structures.

Clarity

Include first-order axiom systems intended to formalize natural-number arithmetic with a declared language and induction resources. Exclude elementary-school calculation, second-order Peano arithmetic, set theory used as a foundation, and the complete true arithmetic theory presented as computably axiomatizable.

Manages Complexity

First-order axioms target natural numbers yet admit other models. Stronger induction proves more but cannot capture all arithmetic truth effectively.

Abstract Reasoning

  1. Signature — Lists zero, successor, operations, and relations. Different signatures express different formulas.
  2. Formulas — Build statements with first-order quantifiers. Second-order set quantification changes the logic.
  3. Axioms — Constrain intended arithmetic behavior. A language alone is not a theory.
  4. Models — Interpret symbols in structures satisfying axioms. Nonstandard models matter in first-order theories.
  5. Induction scheme — Controls which formulas support induction. Removing or restricting it changes proof power.
  6. Proof relation — Derives theorems by first-order rules. Truth in the standard model and provability are distinct.

Knowledge Transfer

Signature–axiom–model analysis transfers across formal theories, but induction strength, decidability, and standard-model claims must be reproved for each arithmetic language.

Examples

Applied / In Practice

Peano arithmetic uses first-order axioms plus an induction scheme for formulas in its language.

Mapped back: logic → first order; domain → numbers; strength → induction scheme.

Applied / In Practice

Robinson arithmetic keeps basic operation axioms but lacks full induction, illustrating a weaker theory.

Mapped back: signature → arithmetic; induction → absent; status → weaker.

Structural Tensions

T1 — Standard Intent versus Nonstandard Models. First-order axioms target natural numbers yet admit other models.

Diagnostic: Is a claim semantic or standard-model specific?

T2 — Expressive Strength versus Axiomatizability. Stronger induction proves more but cannot capture all arithmetic truth effectively.

Diagnostic: Which theory and metatheory are used?

Structural–Framed Character

Lists zero, successor, operations, and relations. Build statements with first-order quantifiers. First-order axioms target natural numbers yet admit other models.

Structural Core vs. Domain Accent

Controls which formulas support induction. Derives theorems by first-order rules. The category changes when quantifiers range over sets or the intended subject is not number arithmetic.

This entry is a kind of Formal Theory.

  • Approved root. The frozen graph retains first-order arithmetic without a parent edge.

  • Related — Peano arithmetic and True arithmetic. One major theory in the family. All first-order truths of the standard model.

Relationships to Other Abstractions

Local relationship map for First-Order ArithmeticParents appear above the current abstraction, mutual partners to the right, and children below. Node labels state whether each abstraction is prime or domain-specific; colors identify relation types.First-OrderArithmeticDOMAINDomain-specific abstraction: Formal Theory — is a kind ofFormal TheoryDOMAIN

Current abstraction First-Order Arithmetic Domain-specific

Parents (1) — more general patterns this builds on

  • First-Order Arithmetic is a kind of Formal Theory Domain-specific

    First-Order Arithmetic is a strict kind of Formal Theory: it is a first-order theory fixed by arithmetic signature, axioms, models, and proof system.

Hierarchy paths (2) — routes to 2 parentless roots

Neighborhood in Abstraction Space

First-Order Arithmetic sits in a crowded region of the domain-specific corpus (31st percentile for distinctiveness): several abstractions share nearly its structure, so a description that fits it tends to fit its neighbors too.

Family — Logical Connectives & Formal Systems (13 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With

  • Peano arithmetic. Tell: One major theory in the family.
  • True arithmetic. Tell: All first-order truths of the standard model.
  • Presburger arithmetic. Tell: Addition-only decidable arithmetic.
  • Second-order arithmetic. Tell: Allows set-of-number variables.

References

  • Frozen Wikipedia discovery revision: https://en.wikipedia.org/wiki/List_of_first-order_theories (revision 1358136878).
  • Preserved source candidate: https://books.google.com/books?id=edqwSVJ9GGQC&pg=PA265

The frozen Wikipedia revision is discovery provenance. The retained source set was reviewed for identity, formal or operational relation, and scope. The encyclopedia's structural synthesis is bounded to those claims; a thin authority surface is recorded as a nonblocking source-strengthening repair rather than concealed.