Discussion:
In summary
Add Reply
Pete Olcott
2017-06-08 15:45:01 UTC
Reply
Permalink
Raw Message
When you used a technique that had zero chance of
working, _listing the true sentences_ , you might as
well have admitted that you had no idea how MTT was
going to do these things you say.
I just have to complete more of my formal specification
so that you can directly see how MTT works.
Therefore, the correct answer to Peter Percival's question
would have been that you didn't know -- yet.
It's really more pleasant all around when you just say
that you don't know the things you don't know.
"I don't know" would be untruthful because I do know.
_What you said_ was a jaw-dropping-ly ignorant and/or
dishonest thing to say, because _it is not possible_
for you to adopt truths as axioms as a general rule
for incorporating truths into MTT. There are too many.
I am not adopting truths as axioms a general rule.
Of course that could not work. I am explicitly defining
the small set of the constituent parts from which all
truth is comprised.
Peter Percival's question was an attempt to get you to
tell us how MTT was going to get from that small set of
truths to the rest of the truths.
Making 7 > 3 an axiom was a dodge.
No it was an aspect of the required foundation. A machine is not even aware that characters are integers.
Instead of showing how MTT was going to get from the small
set of truths to his example, 7 > 3, you just put 7 > 3
in the set. As you say, _of course that could not work_ .
Nonetheless, that's what you did for 7 > 3.
----
I looked through what you've described below, and it
looks nicely capable. I'm looking especially at the control
structures that you plan to have.
However, that is beside the point if you can't formalize
your Big Claim: All sentences will be either provable
or refutable. How do you plan to implement that?
It is not (at least initially) as big as that. Initially it is simply (~Provable(X) & ~Refutable(X)) -> Incorrect(X).
----
Suppose this is a theorem of your formal system
(Ey)( ~Prov(y) & sub(b,[z],b) = y ) <-> ~Prov(sub(b,[z],b))
I will have to put the concept (besides finite string rewrite rules specified by axioms) substitution on a back burner for now. I am still striving diligently to specify the YACC BNF syntax for MTT.
for b = 287411460918262346019384610938410936864016324\
47287740229742074027478734924802984y20984208479872749\
20847080249827474878092748787294874774872734872399472,
as it may well be a theorem.
Does your system check to see
whether 287411460918262346019384610938410936864016324\
47287740229742074027478734924802984y20984208479872749\
20847080249827474878092748787294874774872734872399472
represents
(Ey)( ~Prov(y) & sub(x,[z],x) = y )
or not? (x is a free variable, b is a constant. This
is close to but not exactly the LHS above.)
If MTT checks, where does it do that?
If MTT does not check, how else is this apparent
true-iff-not-provable sentence of MTT formally excluded?
Will the formal system implemented by your software
be consistent when you're finished? Just _claiming_
it will be consistent is not enough.
----
I see below that you've stripped the numbers off of Kurt
Goedel's proof again. How is it that you get to use numbers,
but he doesn't?
He is only using numbers to make the pretense that he is actually talking about arithmetic seem more credible.

When this extraneous (Fred Brooks, inessential) complexity is stripped away understanding what is really going on is enormously simpler.
----
It might interest you to know that there are much simpler
formal systems with true-iff-not-provable sentences.
A very simple one (the simplest I know of) has three
axioms in addition to the logical axioms.
1. There is an _empty set_ .
2. Two sets are _equal_ iff they have the same elements.
3. If x and y are sets, then there exists a set w, the
_adjunction_ of x and y, whose members are just y and
the members of x. ( w = (x U {y}) )
John Burgess calls that theory ST.
-- Burgess, John, 2005. Fixing Frege. Princeton Univ. Press.
Set theory has too much incoherence. I will probably use proper classes or something similar instead.

<snip>
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Peter Percival
2017-06-08 16:12:24 UTC
Reply
Permalink
Raw Message
Post by Pete Olcott
---- It might interest you to know that there are much simpler
formal systems with true-iff-not-provable sentences. A very simple
one (the simplest I know of) has three axioms in addition to the
logical axioms. 1. There is an _empty set_ . 2. Two sets are
_equal_ iff they have the same elements. 3. If x and y are sets,
then there exists a set w, the _adjunction_ of x and y, whose
members are just y and the members of x. ( w = (x U {y}) )
John Burgess calls that theory ST.
-- Burgess, John, 2005. Fixing Frege. Princeton Univ. Press.
Set theory has too much incoherence. I will probably use proper
classes or something similar instead.
Your reply is hardly coherent. Theories of proper classes *are* set
theories. It might make a lot of sense to call NBG not a set theory but
a theory of sets and classes, or just a theory of classes (since every
set is a class) but long usage (since 1925?) has meant that it is called
a set theory nevertheless. Similarly Kelley-Morse is called a set
theory not a class theory. So for you to say that you will use proper
classes because set theory in incoherent is potty.
Post by Pete Olcott
<snip>
--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan
Jim Burns
2017-06-08 16:39:01 UTC
Reply
Permalink
Raw Message
Post by Pete Olcott
----
I looked through what you've described below, and it
looks nicely capable. I'm looking especially at the
control structures that you plan to have.
However, that is beside the point if you can't formalize
your Big Claim: All sentences will be either provable
or refutable. How do you plan to implement that?
It is not (at least initially) as big as that.
Initially it is simply
(~Provable(X) & ~Refutable(X)) -> Incorrect(X).
Then, initially, you haven't done anything to refute Goedel.
All you've done -- initially -- is change the name of
FormallyUndecidable(X) to Incorrect(X)

----
A teeny tiny problem you have here is that, if you
take Incorrect(X) as a reason to say X is not in your
language L(MTT), you won't know which sentences are and
are not in your language -- because, while Proves(x,y)
and Proves(x,not(y)) have terminating procedures defining
them, (Ex)Proves(x,y) and (ex)Proves(x,not(y)) do not.

Maybe it's just a matter of taste, and you find having
an undefined language more ... (Idaknow) than having
sentences with neither proofs nor refutations in the system.
Post by Pete Olcott
Will the formal system implemented by your software
be consistent when you're finished? Just _claiming_
it will be consistent is not enough.
NOTE: This is a Big F'ing Deal.
Post by Pete Olcott
----
I see below that you've stripped the numbers off of
Kurt Goedel's proof again. How is it that you get to
use numbers, but he doesn't?
He is only using numbers to make the pretense that he is
actually talking about arithmetic seem more credible.
This is one of your more bizarre statements.

Whether Kurt Goedel is talking _about_ arithmetic is
independent of whether he is _using_ arithmetic to do that.

One can use _Chinese_ to talk _about_ arithmetic.
He doesn't need to _use_ arithmetic to make it credible
that he is talking _about_ arithmetic -- which is good,
because _using_ arithmetic _doesn't_ make it more credible.
Arithmetic has many other uses.

What makes it credible that Kurt Goedel is _using_
arithmetic to talk _about_ arithmetic is _his proof_
wherein he does exactly that, in gory detail.
Pete Olcott
2017-06-08 17:46:10 UTC
Reply
Permalink
Raw Message
Post by Jim Burns
Post by Pete Olcott
----
I looked through what you've described below, and it
looks nicely capable. I'm looking especially at the
control structures that you plan to have.
However, that is beside the point if you can't formalize
your Big Claim: All sentences will be either provable
or refutable. How do you plan to implement that?
It is not (at least initially) as big as that.
Initially it is simply
(~Provable(X) & ~Refutable(X)) -> Incorrect(X).
Then, initially, you haven't done anything to refute Goedel.
All you've done -- initially -- is change the name of
FormallyUndecidable(X) to Incorrect(X)
----
A teeny tiny problem you have here is that, if you
take Incorrect(X) as a reason to say X is not in your
language L(MTT), you won't know which sentences are and
are not in your language -- because, while Proves(x,y)
and Proves(x,not(y)) have terminating procedures defining
them, (Ex)Proves(x,y) and (ex)Proves(x,not(y)) do not.
∀L ∈ Formal_Systems Provable(L, X) ( ∃Γ ⊂ L (Γ ⊢ X) )
∀L ∈ Formal_Systems Refutable(L, X) ( ∃Γ ⊂ L (Γ ⊢ ~X) )
∀L ∈ Formal_Systems (~Provable(L, X) ∧ ~Refutable(L, X)) → (X ∉ L)
<snip>
Post by Jim Burns
What makes it credible that Kurt Goedel is _using_
arithmetic to talk _about_ arithmetic is _his proof_
wherein he does exactly that, in gory detail.
It sure looks that way to those that don't know better. The one thing thing about the proof that is not even analogous to arithmetic is the key most important aspect of it: provability.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Peter Percival
2017-06-08 17:56:24 UTC
Reply
Permalink
Raw Message
Post by Pete Olcott
[...]
∀L ∈ Formal_Systems Provable(L, X) ( ∃Γ ⊂ L (Γ ⊢ X) )
∀L ∈ Formal_Systems Refutable(L, X) ( ∃Γ ⊂ L (Γ ⊢ ~X) )
∀L ∈ Formal_Systems (~Provable(L, X) ∧ ~Refutable(L, X)) → (X ∉ L)
Is it your belief that the third line above follows from the other two?
--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan
Jim Burns
2017-06-08 22:53:13 UTC
Reply
Permalink
Raw Message
Post by Pete Olcott
Post by Jim Burns
----
A teeny tiny problem you have here is that, if you
take Incorrect(X) as a reason to say X is not in your
language L(MTT), you won't know which sentences are and
are not in your language -- because, while Proves(x,y)
and Proves(x,not(y)) have terminating procedures defining
them, (Ex)Proves(x,y) and (ex)Proves(x,not(y)) do not.
∀L ∈ Formal_Systems
Provable(L, X) ( ∃Γ ⊂ L (Γ ⊢ X) )
∀L ∈ Formal_Systems
Refutable(L, X) ( ∃Γ ⊂ L (Γ ⊢ ~X) )
∀L ∈ Formal_Systems
(~Provable(L, X) ∧ ~Refutable(L, X)) → (X ∉ L)
<snip>
Tell you what, I'm in a good mood, I'll make you an offer.

If you tell me what you mean by those lines you just wrote,
I'll think about them.

One thing I *know* they do *NOT* mean is that
-- Provable X means there is a proof of X,
-- Refutable X means there is a proof of ~X, and
-- if X is neither provable nor refutable, X is
not in formal system L

The reason I *know* you don't mean that is that
you post this in response to me telling you why
that is a problem.

That would be like us having a conversation that goes:
Me: Whoops! You divide by 0 in step 3.
You: Yeah? Well, I divide by 0 in step 3!

Whatever other criticism might be possible of
where and when you posted those strings (formulas?),
it seems undeniable that you did not move the
conversation forward.

----
If, for whatever reason, you want to double down on
the thing I had just noted a problem with,
I refer you to my earlier post.
Pete Olcott
2017-06-09 03:22:50 UTC
Reply
Permalink
Raw Message
<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">On 6/8/2017 5:53 PM, Jim Burns wrote:<br>
</div>
<blockquote cite="mid:2c62988d-3f21-3777-b9fc-***@att.net"
type="cite">On 6/8/2017 1:46 PM, Pete Olcott wrote:
<br>
<blockquote type="cite">On 6/8/2017 11:39 AM, Jim Burns wrote:
<br>
</blockquote>
<br>
<blockquote type="cite">
<blockquote type="cite">----
<br>
A teeny tiny problem you have here is that, if you
<br>
take Incorrect(X) as a reason to say X is not in your
<br>
language L(MTT), you won't know which sentences are and
<br>
are not in your language -- because, while Proves(x,y)
<br>
and Proves(x,not(y)) have terminating procedures defining
<br>
them, (Ex)Proves(x,y) and (ex)Proves(x,not(y)) do not.
<br>
</blockquote>
<br>
∀L ∈ Formal_Systems
<br>
    Provable(L, X) ( ∃Γ ⊂ L (Γ ⊢ X) )
<br>
∀L ∈ Formal_Systems
<br>
    Refutable(L, X) ( ∃Γ ⊂ L (Γ ⊢ ~X) )
<br>
∀L ∈ Formal_Systems
<br>
    (~Provable(L, X) ∧ ~Refutable(L, X)) → (X ∉ L)
<br>
&lt;snip&gt;
<br>
<br>
</blockquote>
<br>
Tell you what, I'm in a good mood, I'll make you an offer.
<br>
<br>
If you tell me what you mean by those lines you just wrote,
<br>
I'll think about them.
<br>
<br>
One thing I *know* they do *NOT*  mean is that
<br>
-- Provable X means there is a proof of X,
<br>
-- Refutable X means there is a proof of ~X, and
<br>
-- if X is neither provable nor refutable, X is
<br>
   not in formal system L
<br>
<br>
The reason I *know* you don't mean that is that
<br>
you post this in response to me telling you why
<br>
that is a problem.
<br>
<br>
</blockquote>
<br>
Since <b>Provable(L, X)</b> and <b>Refutable(L, X)</b> are both
symbolized using conventional syntax that precisely specify the
exact the meaning of their English word predicate names<b> I do not
see how you can honestly deny this.</b> <br>
<br>
<font size="+1"><b>∀L ∈ Formal_Systems
Truth_Bearer(Provable(L, X) </b><b>∨
</b><b> Refutable(L, X)) → (X </b><b>∈
</b><b> L)</b><b><br>
</b></font>
<meta http-equiv="CONTENT-TYPE" content="text/html; charset=utf-8">
<title></title>
<meta name="GENERATOR" content="OpenOffice 4.1.3 (Win32)">
<meta name="CREATED" content="0;0">
<meta name="CHANGED" content="0;0">
<style type="text/css">
<!--
@page { margin: 0.79in }
P { margin-bottom: 0.08in }
A:link { so-language: zxx }
-->
</style>
<meta http-equiv="CONTENT-TYPE" content="text/html; charset=utf-8">
<title></title>
<meta name="GENERATOR" content="OpenOffice 4.1.3 (Win32)">
<meta name="CREATED" content="0;0">
<meta name="CHANGED" content="0;0">
<style type="text/css">
<!--
@page { margin: 0.79in }
P { margin-bottom: 0.08in }
A:link { so-language: zxx }
-->
</style><font size="+1"><b>∀L ∈ Formal_Systems
~Truth_Bearer(L, X)  → (X ∉ L)</b><b><br>
</b><b> </b></font><br>
I can understand why these two formulas would be more difficult to
accept. Accepting the first one depends on accepting philosophical
insights that have never been previously carefully examined or
sufficiently formalized. <br>
<br>
Although the definition of the meaning of <br>
<a class="moz-txt-link-freetext" href="https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)">https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)</a><br>
In mathematical logic, a sentence of a predicate logic is a
boolean-valued well-formed formula with no free variables. A
sentence can be viewed as expressing a proposition, something that
must be true or false.<br>
<br>
Require all of the members of formal systems to be truth bearers, <b>whether
or not the Truth_Bearer(L, X) precisely specifies the exact
necessary and sufficient conditions (criterion measure) of
Truth_Bearer(X) may be open to interpretation and debate. </b><br>
<br>
Although using the conventional English meaning of the word,
provable would seem to intuitively corresponding to true:
English.Provable → English.True. <br>
<br>
The other huge gap in understanding is that most people in Math and
English cannot quite get past the notion that Not(True) does not
always logically entail False.  <b>Sometimes Not(True) means
logically incoherent.</b> <br>
<br>
To accept this last formula would be to accept that the 1931
Incompleteness Theorem is definitely incorrect. I could see how this
would be extremely difficult because for ninety years no one has
successfully pointed out any error. <br>
<b><br>
</b>
<meta http-equiv="CONTENT-TYPE" content="text/html; charset=utf-8">
<p style="margin-bottom: 0in"><b><span style="background: #ffff00">Iff
Truth_Bearer(L, X) does precisely specify all of the necessary
and
sufficient conditions definitively determining whether or not
X is a
Truth Bearer then I have completely proven that the following
paraphrase of the 1931 Incompleteness Theorem has been
correctly
refuted. </span></b>
</p>
<title></title>
<meta name="GENERATOR" content="OpenOffice 4.1.3 (Win32)">
<style type="text/css">
<!--
@page { margin: 0.79in }
P { margin-bottom: 0.08in }
-->
</style><br>
<a class="moz-txt-link-freetext" href="https://plato.stanford.edu/entries/goedel-incompleteness/">https://plato.stanford.edu/entries/goedel-incompleteness/</a><br>
The first incompleteness theorem states that in any consistent
formal system F within which a certain amount of arithmetic can be
carried out, <b>there are statements of the language of F which can
neither be proved nor disproved in F. <br>
<br>
Copyright 2017 Pete Olcott<br>
</b><b><br>
</b>
<div class="moz-signature">-- <br>
<p class="western" style="margin-bottom: 0in"><b><font
face="Arial, sans-serif"><font style="font-size: 12pt"
size="2">(Γ
</font><font style="font-size: 12pt" size="2">⊨ </font><sub><font
style="font-size: 8pt" size="2">FS</font></sub><font
style="font-size: 12pt" size="2">
A) ≡ (</font><font style="font-size: 12pt" size="2">Γ </font><font
style="font-size: 12pt" size="2">⊢
</font><sub><font style="font-size: 8pt" size="2">FS</font></sub><font
style="font-size: 12pt" size="2">
A)</font></font></b></p>
<p class="western" style="margin-bottom: 0in"><br>
</p>
</div>
</body>
</html>

Peter Percival
2017-06-08 16:42:43 UTC
Reply
Permalink
Raw Message
He [Gödel] is only using numbers to make the pretense that he is
actually talking about arithmetic seem more credible.
Why do you think that Gödel is pretending to do anything? Do you think
he set out to deceive his readers? And if so, why?
--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan
Loading...