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.
Are you here to participate in a specific proposal? Click on the proposal tag (with the dark outline) to see only posts about that proposal and not all of the others that are in progress. Tags are at the bottom of each post.
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
by
matthewsnyder
·
2024-02-22T05:03:30Z (9 months ago)
[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.