History edit

History: Skolem (1923) the first published version.

Say sth about the possibility of presenting PRA in a logic-free equation calculus? (Propositional connectives can be replaced with pr functions.) 131.111.8.102 09:07, 25 August 2007 (UTC)Reply

Left turn edit

Article takes a huge left turn at the logic-free calculus section, by using a formalism that is not explained, and apparently not even linked to the article. This is, indeed, a calculus which is free from logic! 70.247.164.231 (talk) 21:26, 28 August 2010 (UTC)Reply

Perhaps this helps? The big horizontal bar is the Rule of inference -- 67.198.37.16 (talk) 20:47, 8 July 2016 (UTC)Reply

From and , deduce , for any predicate edit

What do you mean by "predicate" here? You don't mention above, that in the language of PRA predicate symbols exist. Perhaps you mean "formula of PRA"? Eugepros (talk) 10:48, 21 July 2011 (UTC)Reply

Yeah, beats me, this looks like either a mistake or something that needs clarification and explanation. Or something. 67.198.37.16 (talk) 20:55, 8 July 2016 (UTC)Reply

Skolem arithmetic ? edit

Could anyone give a citation where PRA is called Skolem Arithmetic ? As far as I can tell, everytime I read "Skolem Arithmetic" in a mathematical article, it means the logic with multiplication on positive number, without addition.

Hence, this redirection seems really wrong to me. — Preceding unsigned comment added by Arthur MILCHIOR (talkcontribs) 12:18, 27 June 2012 (UTC)Reply

WP currently has this solution to this question: Skolem arithmetic (disambiguation). 67.198.37.16 (talk) 20:33, 8 July 2016 (UTC)Reply

Unfolding edit

It would be nice to add a discussion of unfolding (logic) and how it connects finitist arithmetic to PRA and non-finitist arithmetic to Peano arithmetic, as discussed by Feferman, Strahm Unfolding finitist arithmetic (2010) but as can be seen, the various red-links make this currently quite difficult. 67.198.37.16 (talk) 20:31, 8 July 2016 (UTC)Reply