Indukcja strukturalna

Indukcja strukturalna to dość powszechnie stosowany wariant indukcji matematycznej, w którym rozważa się pewien zbiór termów uporządkowany następującą relacją: jeden term jest mniejszy od drugiego wtedy i tylko wtedy, gdy jest jego podtermem.

Zasada indukcji strukturalnej głosi, co następuje. Jeśli udowodnimy, że pewną własność mają wszystkie termy atomowe (czyli takie, które nie zawierają żadnych właściwych podtermów) oraz że dla każdego n-arnego symbolu funkcyjnego $f$ z tego, że własność tę mają termy $x_1,\cdots,x_n$, wynika, że ma ją również term $f(x_1,\cdots,x_n)$, to mają ją wszystkie termy.