FOM: True = provable? Was: Goedel: truth and misinterpretations

[Torkel Franzen]

Vladimir Sazonov says:

  >(*)    (A => Pr[T](`A')

  >where Pr[T](x) is arithmetically definable predicate of 
  >provability in T of a formula with Goedel number x and 
  >`A' is numeral (term SSS...S0) representing Goedel number 
  >of A. 
  >
  >Theorem 2. If T is consistent then it is consistent 
  >T* = T + the above axiom schema (*).

  As your proof essentially points out, (*) is consistent with T since
in fact the stronger statement "everything is provable in T" is consistent
with T.

  >Comment 1. Roughly speaking, Theorem 1 means that we can 
  >reasonably assume that 
  >	every true sentence is provable.

  This is a very mysterious comment, however. The mere fact that (*) is
consistent with T does not imply that it is at all reasonable to assume
(*), any more than the consistency of "PA is inconsistent" with PA means
that we can reasonably assume that PA is inconsistent.

  >Now consider a stronger schema 
  >(**)     (A <=> Pr[T](`A')
  >Let us call a theory T *strongly consistent* (PA is an example of 
  >such theory) if it does not proves ``pathologies'' as 
  >	~A <=> Pr[T](`A')
  >or any their finite disjunctions.

  This can't be quite what you mean, since PA is not "strongly
consistent" in this sense. ~A <=> Pr[T](`A') is provable in PA if
A is a Godel sentence for PA.
  
  >Theorem 2. If T is strongly consistent then it is consistent 
  >T** = T + the above axiom schema (**).

  Your proof of this is correct, but does not apply to PA, as noted above.
The schema (**) is incompatible with the diagonal lemma.
---

Torkel Franzen