Wittgenstein's Uniqueness Rule as an Elimination Rule of Inductive Types:
Mitsuhiro Okada · Kagaku tetsugaku · 2021
We discuss the equational representations of the elimination rule of inductive types, with a focus on the type "natural number", in the context of the series of approaches to separating an equational calculus from logic.We go back to a source of the purely equational representation of the elimination rule, Wittgenstein's uniqueness rule.We analyze Wittgenstein's argument, in comparison with others', which gives supplementary remarks to Marion-Okada (2018).