On 12/13/2018 3:25 AM, Bruno Marchal wrote:
But that is the same as saying proof=>truth.
I don’t think so. It says that []p -> p is not provable, unless p is
proved.
So []([]p -> p) -> p or in other words Proof([]p -> p) => (p is true)
So in this case proof entails truth??
For example []f -> f (consistency) is not provable. It will belong to
G* \ G.
Another example is that []<>t -> <>t is false, despite <>t being true.
In fact <>t -> ~[]<>t.
Or <>t -> <>[]f. Consistency implies the consistency of inconsistency.
I'm not sure how to interpret these formulae. Are you asserting them
for every substitution of t by a true proposition (even though "true" is
undefinable)? Or are you asserting that there is at least one true
proposition for which []<>t -> <>t is false?
Nothing which is proven can be false,
Assuming consistency, which is not provable.
So consistency is hard to determine. You just assume it for
arithmetic. But finding that an axiom is false is common in argument.
which in tern implies that no axiom can ever be false.
Which is of course easily refuted.
Which makes my point that the mathematical idea of "true" is very
different from the common one.
“BBBBBBB” is true just in case it is the case that BBBBBBB.
But you can't know whether it is the case that 10^10000 + 1 is the
successor of 10^1000 independent of the axioms, i.e. you assume it.
Brent
I am not sure, but the point is that no machine can prove []p -> p in
general. And the machine can know that, making her “modest” (Löbian).
Bruno
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
