Quantifier-free induction for lists

05/15/2023

∙

by   Stefan Hetzl, et al.

∙

0

∙

share

We investigate quantifier-free induction for Lisp-like lists constructed inductively from the empty list 𝑛𝑖𝑙 and the operation 𝑐𝑜𝑛𝑠, that adds an element to the front of a list. First we show that, for m ≥ 1, quantifier-free m-step induction does not simulate quantifier-free (m + 1)-step induction. Secondly, we show that for all m ≥ 1, quantifier-free m-step induction does not prove the right cancellation property of the concatenation operation on lists defined by left-recursion.