Welcome to the staging ground for new communities! Each proposal has a description in the "Descriptions" category and a body of questions and answers in "Incubator Q&A". You can ask questions (and get answers, we hope!) right away, and start new proposals.
Post History
Presburger arithmetic is a theory that is decidable, but includes an infinite set of axioms. The interesting part is the 5th point from the Wikipedia formulation: (P(0) ∧ ∀x(P(x) → P(x + 1))) →...
Answer
#1: Initial revision
[Presburger arithmetic](https://en.wikipedia.org/wiki/Presburger_arithmetic) is a theory that is decidable, but includes an infinite set of axioms. The interesting part is the 5th point from the Wikipedia formulation: > `(P(0) ∧ ∀x(P(x) → P(x + 1))) → ∀y P(y)` This is an induction schema representing infinitely many axioms. The goal is to state that for any claim `P(x)` about a number `x`, if `P(x)` being true also means `P(x+1)` true, then `P` is true for all numbers. To express this in first order logic, you have to essentially make one axiom for each number.