Re: [isabelle] theoretical question



They may simply be referring to the fact that in most cases, once you have recursion, you can define enough number theory for GÃdelâs theorem to apply. The need for termination proofs is quite another matter: accepting a function definition such as f(n) = Suc(f(Suc n)) can easily lead to inconsistency.

Larry

> On 31 May 2016, at 10:37, Gergely Buday <gbuday at karolyrobert.hu> wrote:
> 
> Do I understand correctly that the above remark about adding recursion to a language makes any axiomatisation incomplete is true
> 
> for the same reason that makes it impossible to create a general function definition in a higher order logic of total functions, without the need to supply a termination proof in general?





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.