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.

# What is a common infinite and decidable set of axioms? Question

a formal system is a system of axioms equipped with rules of inference, which allow one to generate new theorems. The set of axioms is required to be finite or at least decidable, i.e., there must be an algorithm (an effective method) which enables one to mechanically decide whether a given statement is an axiom or not. If this condition is satisfied, the theory is called “recursively axiomatizable”, or, simply, “axiomatizable”.

https://plato.stanford.edu/Entries/goedel-incompleteness/

What is a common example of an infinite but decidable set of axioms?

## 1 answer

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.

## 0 comment threads