On 12/3/2023 2:24 PM, olcott wrote:
> On 12/3/2023 1:03 PM, Jim Burns wrote:
>> On 12/3/2023 12:32 PM, olcott wrote:
>>> The version that you provided
>>
>> This one HOL.sentence
>> |
>> | HOL" preceded by its HOL.quotation
>> | is not HOL.provable "HOL
>> | preceded by its HOL.quotation
>> | is not HOL.provable.
>>
>
> Is rejected as semantically unsound
> on the basis that
> it forms a cycle in the directed graph of
> its evaluation sequence.
Say that a hundred more times,
and it still won't be true.
We need to be able to express two properties
in our language-of-the-day for HOL
Arithmetic is sufficient for this, but
we can go further, as long as
we can still express it.
Proves(y,x)
if
y represents a proof in HOL of
a formula in HOL which x represents
then
Proves(y,x) is true. Otherwise, false.
Subst(x,y,z)
if
x represents a formula A(u) with
one variable not bound by a quantifier (free)
and z represents A(y)
AKA A(u) with y substituted for
free occurrences of u in A(u)
then
Subst(x,y,z) is true. Otherwise, false.
Subst(x,y,z) doesn't get much attention,
I guess. It seems to me to be
pretty much guaranteed to exist
if predicate Proves(y,x) exists
But Subst(x,y,z) is how we get
"preceded by its quotation is not provable"
to be preceded by its quotation.
These numbers representing formulas
the same as quotations:
things representing speech acts.
∃y(Subst(x,x,y) ∧ ¬∃z:Proves(z,y)))
is the HOL.predicate meaning
| x represents
| a formula A(u) such that,
| for A(x), represented here by y
| no proof, represented here by z,
| exists
For convenience, refer to
∃y(Subst(x,x,y) ∧ ¬∃z:Proves(z,y)))
as G(x)
Represent (ie, quote) G(x) as a number g
G(g) is a certain long arithmetical formula
G(g) _means_
| HOL" preceded by its HOL.quotation
| is not HOL.provable "HOL
| preceded by its HOL.quotation
| is not HOL.provable.
If G(g) is true, G(g) is not provable,
and not all true sentence of HOL
are provable.
> "preceded by its HOL.quotation" is simply
> a way to indirectly refer to a sentence
> by its name.
No.
Your "proof" that that's so
is to
swap out G(g) and put something else in.
https://en.wikipedia.org/wiki/Straw_man