> > On 2008-01-28, in sci.logic, R. Srinivasan wrote:

> > > It takes a lot of *coding* to put all of this into primitive recursive
> > > arithmetic, which only deals with numbers as objects. Your claim that
> > > Godel's proof is finitary is dependent on the fact that the said proof
> > > can be encoded into PRA. But I on the other hand, insist that the
> > > notion of  "all primitive recursive functions" is *essentially*
> > > infinitary and *cannot* be encoded via any finitary process into
> > > PRA.

> > We can just talk about, say, extensions of Q, as outlined by Rupert in
> > an another post. As to all the tedious coding, you'll find the details
> > in any number of texts, such as Girard's _Proof Theory and Logical
> > Complexity_. As to NAFL, of which I'm entirely ignorant, it might or
> > might not be that Godel's proof goes through. That's entirely
> > irrelevant to the observation that Godel's proof is perfectly finitary
> > in the ordinary sense of the word.

> > > But strictly speaking, to show that (1) would entail consistency of
> > > PRA, one would have to also use ex falso quodlibet (from a
> > > contradiction P&~P, an arbitrary propostion Q can be deduced).

> > If we define inconsistency as proving every sentence ex falso
> > quadlibet is indeed required. However, as outlined in a post of mine
> > /A recursion theoretic look at incompleteness/ we can formulate the
> > first incompleteness theorem in a 'logic-agnostic' form, making no
> > assumptions about the underlying logic of the theory. The second
> > incompleteness theorem has no such formulation, and does depend on the
> > properties of the rules of inference.

> I wish to define consistency of a theory T by the requirement that
> *every* sentence of the form P&~P (i.e. every contradiction) in the
> language of T should be unprovable in T. Therefore my definition of
> inconsistency of T is the provability in T of at least one
> contradiction. By ex falso quodlibet, the consistency of T can be
> reduced to the unprovability of a single sentence (say, "0=1") and
> this is seemingly a finitary concept. What I was trying to get at was
> that this latter assertion requires ex falso quodlibet if it were to
> really represent consistency, and that the inference from ex falso
> quodlibet (that T proves every contradiction in its language if T
> proves one contradiction) cannot really be expressed finitarily.
> Please see my comments below.

> > > 'A proof of  any sentence of the form P&~P in PRA implies that every
> > > sentence in the language of PRA is deducible in PRA'        (2)

> > That is trivially provable in PRA. However, I wonder why you're
> > talking about PRA here? What was at issue was PRA proving the
> > incompleteness theorems, not what PRA proves of itself. (It does, of
> > course, prove that the incompleteness theorems apply to PRA).

> The reason I am talking about PRA is that it is considered as the
> formal system that correctly captures finitism. Presumably you are
> asserting that the reasoning used by Godel is finitary because that
> reasoning can be formalized within PRA.

> Now I do not agree with your assertion that the sentence (2) above is
> trivially provable *in* PRA. We can indeed infer that PRA will prove
> every sentence in its language if it proves a contradiction. But that
> inference is not made *within* PRA, it is a metamathematical fact
> *about* PRA. For the sentences of PRA are about numbers and no
> sentence of PRA can ever tell you something about all of its
> sentences, at least not without the kind of coding employed by Godel.