User talk:CBM

m:User:CBM

Please leave new comments at the bottom of the page, using the "new section" button at the top of the page.

I will respond on this page unless you request otherwise.

Archives

1	2	3	4	5	6
7	8	9	10	11	12
13	14	15	16	17	18

Bot issue

Hi Carl, the bot seems to be adding the peer reviews that are lists in reverse chronological order in the bottom section at WP:PR - please see Wikipedia_talk:Peer_review#Couple_of_problems.

I also wondered if User:PeerReviewBot/Logs/Archive might be a candidate for archiving by Miszabot - it is up to 175 entries. Thanks as always for all you do, Ruhrfisch _><>°^° 02:56, 24 October 2009 (UTC)[reply]

I fixed the lists issue. For the archive log, I just delete the old entries from time to time. They are still in the page history, and this is simpler than keeping a bunch of archives. — Carl (CBM · talk) 12:03, 24 October 2009 (UTC)[reply]

Thanks so much! Ruhrfisch _><>°^° 02:25, 25 October 2009 (UTC)[reply]

Ref for claim in Primitive recursive function?

Can you provide a reference for this? Specifically, I would like to know how Gödel's incompleteness theorem can be formalized into PRA. I think it would also be worth noting this in Primitive recursive arithmetic. Thanks, — sligocki (talk) 07:21, 25 October 2009 (UTC)[reply]

I know there are two citations in the article on the incompleteness theorems. If I remember correctly, Smoryński gives the usual syntactic proofs and discusses how they can be formalized into PRA, while Kukuchi and Tanaka discuss how the semantic proof can be formalized in WKL₀, which suffices to show that its conclusion is provable in PRA, because of a conservation result.

I think the hardest part is figuring out how to express the incompleteness theorems in PRA. Once that is done, the fact that they are provable in PRA comes by just mimicking the standard proofs within PRA. To see one way how things can be represented, let T be a computable theory with index e. Define a "coded proof" to be a sequence of the form

((a_{0},t_{0}),(a_{1},t_{1}),\ldots ,(a_{k},t_{k}),p_{0},p_{1},\ldots ,p_{m})

where:

For each i ≤ k, t_i is a computation sequence verifying that a_i is in the r.e. set with index e
The sequence $(p_{0},p_{1},\ldots ,p_{m})$ is a formal proof all of whose axioms are among $(a_{0},\ldots ,a_{k})$ .

Note there is a primitive recursive function F_T such that for all n, F_T(n) = 1 if and only if n is a coded proof in the sense just described. Moreover, there is a primitive recursive function G_T such that G_T(n) = 1 if and only if n is a coded proof whose conclusion is "0=1". Then the statement "Con(T)" is represented by this formula of PRA:

\forall n(F_{T}(n)=1\to G_{T}(n)\not =1)

One thing that may be confusing at first is that the literature uses "PRA" both to mean a quantifier-free theory and also to mean a theory that does have quantifiers but where the induction scheme is restricted to quantifier-free formulas. These are basically the same, but it is much more convenient to work in the latter, because then not as much coding is necessary. — Carl (CBM · talk) 12:52, 25 October 2009 (UTC)[reply]

First-order theories

I am pretty sure that every first-order formal system can be expressed as a first-order theory (precisely what you said... a set of sentences). This is to say that specifying a formal language, and a deductive system takes place within the form of a set of sentences in a metalanguage. Therefore it is a precise way to describe what is going on here (--as far as what is a type of what). I find this is consistent with what I have seen in several places. Stay cool C.Pontiff Greg Bard (talk) 23:21, 25 October 2009 (UTC)[reply]

P.S. is it possible to set up the mathematical logic assessment so that a list of popular pages can be generated? I have requested this for the task forces of WP:PHILO and was wishing it could also be done for math-logic. Thank Carl. -GB

"First order logic with equality" is not a first order theory; perhaps it is a framework in which one can study first order theories. Some examples of first-order theories are given at list of first-order theories. — Carl (CBM · talk) 00:46, 26 October 2009 (UTC)[reply]

Wikipedia:Naming conventions (Macedonia) has been marked as a guideline

Wikipedia:Centralized discussion/Macedonia/consensus no longer marked as a guideline

Wikipedia:Centralized discussion/Macedonia/consensus (edit | talk | history | links | watch | logs) has been edited so that it is no longer marked as a guideline. It was previously marked as a guideline. This is an automated notice of the change (more information). -- VeblenBot (talk) 02:00, 26 October 2009 (UTC)[reply]

Wikipedia:Naming conventions (categories)/Usage of American no longer marked as a guideline

Wikipedia:Naming conventions (categories)/Usage of American (edit | talk | history | links | watch | logs) has been edited so that it is no longer marked as a guideline. It was previously marked as a guideline. This is an automated notice of the change (more information). -- VeblenBot (talk) 02:00, 26 October 2009 (UTC)[reply]

Computable number reference

Carl, could you please correct the reference to "Bishop and Ridges, 1987" in Computable number? Probably "Bridges and Richman, 1987" or "Bishop and Bridges, 1985". 66.245.43.17 (talk) 07:42, 26 October 2009 (UTC)[reply]

That was strange. I must have meant Bridges and Richman, but why did I get the name and year wrong? I'll see if I can look up a page number later. — Carl (CBM · talk) 10:26, 26 October 2009 (UTC)[reply]

Thanks! 66.245.43.17 (talk) 16:44, 26 October 2009 (UTC)[reply]

Policy

This bot has recently informed incorrectly at the VillagePump that Wikipedia:CheckUser had been marked as policy, while it has always been so. The anounce was likely trigered by this edit, that did simple category work. Adding the category should indeed be taken into account by the bot, but not if the page had already the policy tag. MBelgrano (talk) 15:19, 26 October 2009 (UTC)[reply]

Actually, pages in Category:Wikipedia policies and guidelines are not "marked as policies"; that is the role of the category Category:Wikipedia policy. The former category is just a meta-category to gather up all the related categories. This is why, for example, Wikipedia:List of policies is in the former category, not the latter. Usually the {{policy}} template takes care of the categorization, but in this case a custom-written message is used instead, so this page was not (recently) already marked with the {{policy}} template. Whenever that template is used, the appropriate category is added automatically, so the bot has the effect of also tracking when the template is added.

I realize this sounds somewhat legalistic, but the entire point of the bot is to watch which pages are literally "marked as policies" by being placed into the corresponding category (which will always happen if the {{policy}} tag is added). In any case, now that the checkuser page is fixed, the bot won't report it again unless it is removed from the policy category for some reason. We can just delete the announcement from when the categorization was fixed. — Carl (CBM · talk) 15:41, 26 October 2009 (UTC)[reply]