# FOM: true but not provable

V. Sazonov V.Sazonov at doc.mmu.ac.uk
Tue Oct 31 09:19:40 EST 2000

```William Tait wrote:
>
> Whether or not
>
> (1) A is true but not provable
>
> i.e.
>
> (1) A and {A is not provable)

Yes, this is a possible reading (or variation of?) (1)
(with using \not\exists x Proof(x,`A'))
which I did not take into account in my postings on this subject.
However, strictly speaking, I would not write here "i.e.".
I am not sure that for everybody "A is true" is just A.
For me "A is true" in some philosophical contexts is just
nonsense. In mathematical context it really seems the same
as A.

Anyway, we should appropriately transform a statement
of a natural language to make it mathematical. Moreover,
there may be various ways of such transformation.
What therefore means using natural language in mathematics
if we are often not very careful?

>
> is meaningful or not for a mathematical proposition A, it is
> certainly a useless proposition. To be warranted in asserting (1), we
> must be warranted in particular in asserting A (which, unlike `A is
> provable', is a mathematical proposition),

Strange! "Unlike", even if "provable" will be interpreted with
the help of Goedel's predicate Proof(x,y)? Of course this is also
called Metamathematics, what does not mean that it is not a
kind of Mathematics.

i.e. we must have a proof
> of A, thereby refuting (1).

That is a formal theory having

A and {A is not provable)

as an axiom or theorem is inconsistent. It seems to me that
(1) described above. Otherwise he would see immediately the
contradiction. I guess he considered some mysterious for me
Philosophical meaning of "A is true", and such a "meaning"
is the stumbling block of many discussions in FOM.

>
> Torkel Franzen wrote (Oct 27)
>
> >   As for your claim that it is "wrong and basically meaningless" to
> >say that there are true but unprovable sentences, I don't think I
> >understand it. You agree that it is a mathematical theorem that there
> >are true arithmetical sentences not provable in T, for any consistent
> >extension T of PA, but you seem to be saying that we must not take
> >this theorem at face value, but regard it from some purely formal
> >standpoint. Why is that?
>
> But clearly when whoever wrote that it is wrong and basically
> meaningless to say that there are true but unprovable sentences, he
> did not intend the proof predicate to refer to some particular formal
> system.

No, e.g. I meant (if not Goedel's formalized Prove_{PA}(x,y) predicate)
just "unprovability in PA" or in any other formal system like PA.
Even in this case the English word "unprovable" (in philosophical
context) seems to me too ambiguous until it will not be explained
by the author of such a phrase on unprovability, as I wrote in my
last postings.

For the extension T of PA in question, assuming it partially
> formalizes our mathematics, we can say that the Goedel sentence G for
> it is true, i.e. assert G, because we can prove it in the
> second-order extension of T.

But it is disprovable in also consistent T' = T + not G.
Why do you decide that G is true? It is true IN a theory,
but not just true. By the way, I do not understand this
"just true". On the other hand, we could discuss plausibility
of T, T' and other formalisms and decide that some of them are
more interesting for us (from some point of view) and then,
probably, so to speak, to "conclude" plausibility of G.
But this is not just saying that G is true.

(Here I am assuming, only for
> simplicity, that T is first-order.) So in the intended sense of
> provability, G is provable.
>
> The question is: what does `A is unprovable' mean? I suggested
> recently that, in the case of A = CH or any other presently
> undecidable sentence, it is best understood as a sociological

One more meaning of a sentence written in a natural language!
Philosophers of mathematics should be extremely careful.
What is better than mathematics where seemingly no SUCH problems
arise? However, we also need a philosophy which would say us
something very important about the nature of mathematics.
{"extraction_info": {"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.881156861782074, "perplexity": 2113.6293235222934}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2016-26/segments/1466783395560.69/warc/CC-MAIN-20160624154955-00110-ip-10-164-35-72.ec2.internal.warc.gz"}