FOM: Goedel: truth and misinterpretations

[Matt Insall]

Professor Kanovei:
If T is assumed to be a mathematical statement then to have
meaning it has to be rewritten in accordance to mathematical
standards (and this is you who have to rewrite it), in particular,
I don't know how to interpret the ending
"this fact may not be provable" through any combination of
quantifiers.


Reply:
I did not state that T is assumed to be a mathematical statement,
but I shall attempt a reformulation for you.  In particular, I shall
introduce quantifiers that deal with my meaning of ``this fact may
not be provable'':

Even if the statement ``every even number greater than
2 is the sum of two primes'' is consistent relative to
ZFC, then perhaps there is no proof of this fact, and
perhaps there never will be written a proof of this fact.


Now, I will express this in an appropriate formal language:

\Diamond(Con(GC) & ~Prov(Con(GC)) & \Box(~Prov(Con(GC)))

Here

Con(GC) is a formal statement that represents
``Goldbach's Conjecture is consistent relative to ZFC''

Prov(p) is a formal statement that represents
``p is provable in L''

where L is a specific formal language in which these statements
may be expressed.  The modal language in which I have re-stated
T is the first-order modal language built over the formal first-order
language L by introducing the modal (temporal?) operators
\Box and \Diamond in the usual way.  There are various modal
systems in which one may consider the truth or falsity of this
statement.  One which comes to mind is frequently referred to
as S4, and includes the following axioms and inference rule:

\Box(p-->q)-->(\Box p--> \Box q)

(forall x)\Box p(x) --> \Box(forall x)p(x)

\Box p --> p

\Box p --> \Box\Box p

\Diamond p <--> ~\Box~p

p |-- \Box p


Is this the type of formalization which you prefer, Professor Kanovei?




Matt Insall