> I should also say that I know the proofs of all statements with the exception of Day 20, about the reflection principle. I haven't been able to figure it out myself, and Boolos proves it with a different method (although he says that a usual proof "is not particularly difficult"), so I would be glad if someone shares the proof with me.
There you go: $( Day 20. Formula ` []. ph -> ph ` is called the reflection principle for ` ph ` , in particular, ~ ax-gl means that ` ph ` is provable if the reflection principle for ` ph ` is provable. The following result means that there's no single reflection principle which implies ` -. []. []. F. ` . See Boolos p. 63 for more context. $) norefl $p |- ( []. ( ( []. ph -> ph ) -> -. []. []. F. ) -> []. []. F. ) $= ( cbox wi wfal wn wa wo imor imbi1i jaob monrule distrconj axk4 ax-distrb syl sylbb con4 a1d ja 3syl pm2.21 pm2.24 com12 cdiam notnotr con3i df-diam kurbis biimpri imp monimpconj syl2anr sylbi ax-gl ) ABZACZDBZBZEZCZBUOEZUSCZAUSCZFZB ZURUQCZBZURUTVDUTVAAGZUSCVDUPVHUSUOAHIVAUSAJPKVEVBBZVCBZFVGVBVCLVJUOUSBZCZBZU RUOCZBVGVIVJVJBVMVCMVJVLAUSNKOVBVNUOURQKVLVNVFVLVNVFUOVKVNVFCVNVAVFURUOVAVFCU SVFVAURUQUARUOVFUBSUCVKVFVNVKUQURVKUQEZEZBZEZBVOUDZBUQUSVRVQURVPUQUQUEKUFKVRV SVSVRVOUGUIKVODUHTRRSUJUKULUMUQUNT $. I made this proof on my own. I almost completed the other ones too, but maybe I'll post them all together if I finish. In my opinion, this proof was a bit difficult (contrary to what Boolos says), especially since I've never heard of this logic before this challenge. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/7d6246a8-58b4-4a83-a9cf-0c6dffd48754n%40googlegroups.com.
