Is there an axiomatization of Peano arithmetic where the axiom schema contains fewer than 4 distinct occurrences of the metavariable? Ideally, as few as possible.
The immediate motivation is to come up with a special purpose tableau calculus for Peano arithmetic with dedicated rules to make it more convenient. (For example, adding rules for commutativity and associativity of addition and multiplication can make proofs shorter).
The induction scheme for Peano arithmetic is given below.
Let $V$ be a list of variables. Let $\alpha \land^x \beta$ bet $(\forall x \mathop. \alpha \land \beta)$ and let $\alpha \land_x \beta$ be $(\exists x \mathop. \alpha \land \beta)$.
Let $\varphi(x, V)$ be an arbitrary well-formed formula.
$\varphi(0, V) \land (\varphi(a, V) \to^a \varphi(1+a, V)) \to^V (\forall x \mathop. \varphi(x, V))$ is the axiom schema of induction.
However, this schema is difficult to use in a tableau setting because it splits into the following cases.
- $\lnot \varphi(0, V)$ -- the statement holds at $0$
- $\varphi(c, V) \land \lnot\varphi(1+c, V)$ -- the induction step fails somewhere.
- $\varphi(x, V)$ -- the statement is always true.
This is workable, we can arbitrarily insert instances of inference rules into a tableau if we're careful to avoid accidentally capturing variables. However, four separate versions of the induction hypothesis can quickly get unwieldy.
Yes. You can do this by looking at the statement of Noetherian induction and noticing that the predicate only appears twice. Noetherian induction generalizes structural induction (where the primitive closed sets are the downward closed sets using the substructure relation), which generalizes induction on the natural numbers. This question contains a brief explanation of Noetherian induction.
You can tweak the idea to look at the predecessor rather than all entities strictly less than the current one. Looking at all strictly smaller numbers gives you strong induction, which also works as an induction axiom.
This leaves you with the axiom schema $(y + 1 = x \to^y \varphi(x)) \to^x \varphi(y)$ where $\chi \to^x \psi$ abbreviates $\forall x (\chi \to \psi)$.
Or the strong inductive variant $(y < x \to ^y \varphi(x)) \to^x \varphi(y)$ with $y < x$ abbreviating $\exists z (y+1+z = x)$ or similar.