tag:blogger.com,1999:blog-5240588941019541660.post4058223028661505884..comments2016-05-02T13:16:05.877-07:00Comments on Proof Theory Abridged: Goodman's theoremPaulo Olivahttps://plus.google.com/109371735093431500627noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-5240588941019541660.post-29563644010396954152013-04-17T14:43:17.744-07:002013-04-17T14:43:17.744-07:00Indeed, for a large class of formulas realizabilit...Indeed, for a large class of formulas realizability makes the formula stronger, so that "t realizes A" implies A. The "machinery" above deals with the cases where "t realizes A" does not imply A just in HAomega (but would imply with AC and IP). For a simple example of such a formula see Coquand's recent paper cited above.Paulo Olivahttp://www.blogger.com/profile/13839186395403550796noreply@blogger.comtag:blogger.com,1999:blog-5240588941019541660.post-32152386039714131762013-04-03T07:31:51.725-07:002013-04-03T07:31:51.725-07:00Isn't the result obvious for say, sigma0n form...Isn't the result obvious for say, sigma0n formulas? In this case modified realizability implies truth without choice. Is thus this bizzarre machinery used only to handle implication?Anonymousnoreply@blogger.com