A Note on a Paramterized Version of the 
Well-Founded Induction Principle

Bernhard Gramlich
Fachbereich Informatik, Universitaet Kaiserslautern
D-67653 Kaiserslautern, GERMANY
E-mail: gramlich@informatik.uni-kl.de

Abstract
The well-known and powerful proof principle by well-founded
induction says that for verifying $\forall x : P(x)$ for
some property $P$ it suffices to show 
$\forall x : [ [ \forall y < x : P(y) ] \implies P(x) ]$,
provided $<$ is a well-founded partial ordering on the domain
of interest. Here we investigate a more general formulation
of this proof principle which allows for a kind of
parameterized partial orderings $<_x$ which naturally arises
in some cases. More precisely, we develop conditions under
which the parameterized proof principle 
$\forall x : [ [ \forall y <_x x : P(y) ] \implies P(x) ]$
is sound in the sense that  
$\forall x : [ [ \forall y <_x x  : P(y) ] \implies P(x) ] 
  \implies \forall x : P(x)$ holds, and give counterexamples
demonstrating that these conditions are indeed essential.  

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1995/
file: Gramlich.SR-95-08.ps.gz