[FOM] Notes on "Artemov Consistency"

[Richard Kimberly Heck]

> A brief correction, not a separate posting. I hope the esteemed moderator posts it. 
>
> >/T is "Artemov consistent" iff ∀n[Bew_T("~Pf(n,0=1)")] /
> Sadly, this is a misunderstanding, hence the whole analysis of this notion, though correct, is misplaced. 
>
> What is here called "Artemov consistency” was used in my PoC paper as a technical notion which was compared NEGATIVELY with the real consistency proposal, cf. Section 4.2 “Provability of CConPA in PA is not an answer either” (and many other comments throughout the paper). 
I had read section 4.2. The only complaint there is that the argument
assumes the soundness of PA. But the argument I gave certainly does not
assume the soundness of PA, since it can be formalized, for the case of
PA, in a constructive version of S^1_2.

> My real proposal was formulated for T=PA and it is different from ”Artemov consistency”, cf. section 5.  
The proof given there simply is an informal proof of the informal
analogue of CCon_PA, one that can be straightforwardly formalized (in
EFA) as a formal proof of CCon_PA.

Riki


-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190412/1a1859f2/attachment.html>