Basic induction over natural numbers

[edit] Weak induction

The weak induction principles for predicates is supported by the static and dynamic contexts.

Introduce $P$ .

Assume $P(0)$ .

Assume for all $n \in \mathbb{N}$ , $P(n)$ implies $P(n+1)$ .

Assert for all $n \in \mathbb{N}$ , $P(n)$ .

The weak induction principles for sets is also supported by the static and dynamic contexts.

Introduce $S$ .

Assume $0 \in S$ .

Assume for all $n \in \mathbb{N}$ , $n \in S$ implies $n+1 \in S$ .

Assert for all $n \in \mathbb{N}$ , $n \in S$ .