Discussion:
Graham Cooper's 2012-05-16 reasoning seems similar to mine
(too old to reply)
Pete Olcott
2017-06-13 17:55:40 UTC
Permalink
Raw Message
<html>
<head>

<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p><font face="Segoe UI Symbol"><a class="moz-txt-link-freetext" href="https://groups.google.com/forum/#!original/">https://groups.google.com/forum/#!original/</a><b>comp.theory</b>/2-h0Q98BWr0/BgRbliY-jMkJ
<br>
From: <b>Graham Cooper</b> <a class="moz-txt-link-rfc2396E" href="mailto:***@gmail.com">&lt;***@gmail.com&gt;</a><br>
Newsgroups: comp.theory,sci.logic<br>
Subject: Re: The answer to the Halting Problem stored within
Permutations of<br>
 Internal States?<br>
Date: Wed, <b>16 May 2012</b> 23:04:47 -0700 (PDT)<br>
</font></p>
<p><font face="Segoe UI Symbol"><b>Here is my formula: </b><b><br>
</b>G( ~∃Γ ⊂ PM (Γ ⊢ G) )  // Incompleteness Theorem as a named
predicate <br> <b>In other words: G( ~Provable(PM, G) )</b><br> </font></p> <p><b>Here is Graham Cooper's way of saying it:</b><b><br> </b>PROOF(C) =3D C v (PROOF(A) ^ PROOF(B) ^ (A^B-&gt;C))<br>
<br>
THE PROOF PREDICATE GODEL PROVED DOESN'T EXIST!<br>
<br>
C is proven IF c is a theorem in the theory<br>
OR C is derived from other theorems (A^B) in the theory!<br>
<br>
It's slightly rearranged from the original specification, a dual
tail<br>
end <b>recursive directed acyclic graph of binary deductions</b>!<br>
</p>
-- <br>
<div class="moz-signature">
<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>
<b>
</b>
<p class="western" style="margin-bottom: 0in"><br>
</p>
</div>
</body>
</html>
Pete Olcott
2017-06-13 18:54:16 UTC
Permalink
Raw Message
https://groups.google.com/forum/#!original/comp.theory/2-h0Q98BWr0/BgRbliY-jMkJ
Newsgroups: comp.theory,sci.logic
Subject: Re: The answer to the Halting Problem stored within
Permutations of
Internal States?
Date: Wed, 16 May 2012 23:04:47 -0700 (PDT)
G( ~∃Γ ⊂ PM (Γ ⊢ G) ) // Incompleteness Theorem as a named
predicate
In this formula, the notation "PM" occurs. Does that string of symbols denote a set of well-formed formulas in some formal language? Or does it function in some other way?
https://en.wikipedia.org/wiki/Principia_Mathematica
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Pete Olcott
2017-06-13 20:06:44 UTC
Permalink
Raw Message
Post by Pete Olcott
https://groups.google.com/forum/#!original/comp.theory/2-h0Q98BWr0/BgRbliY-jMkJ
Newsgroups: comp.theory,sci.logic
Subject: Re: The answer to the Halting Problem stored within
Permutations of
Internal States?
Date: Wed, 16 May 2012 23:04:47 -0700 (PDT)
G( ~∃Γ ⊂ PM (Γ ⊢ G) ) // Incompleteness Theorem as a named
predicate
In this formula, the notation "PM" occurs. Does that string of symbols denote a set of well-formed formulas in some formal language? Or does it function in some other way?
https://en.wikipedia.org/wiki/Principia_Mathematica
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
I have certainly heard of Principia Mathematica, and I could have made an educated guess that PM stands for Principia Mathematica.
Is there any chance you could give some thought to the idea of simply answering my question? My question calls for a yes or no answer. You've given me a link to a Wikipedia article, but I still don't know if the answer to my question is yes or no. A yes or no answer would be really awesome, thanks.
Your question was ambiguous in several ways:
Are you asking:
(1) Does Principia Mathematica represent a string of symbols that are syntactically well formed?
(2) Does the expression that I provided represent a string of symbols that are syntactically well formed?
(3) Does the expression that I provided represent a string of symbols that are logically coherent?
(4) Does the expression that I provided represent a string of symbols from Principia Mathematica ?
On and on...

The string of symbols that I provided represents and expression from HOL that is equivalent to the 1931 Incompleteness Theorem in that G( ~Provable(G) ) is neither provable nor refutable for the same reason that the 1931 GIT is neither provable nor refutation.

G( ~Provable(G) ) is a simplistic way of saying: G( ~∃Γ ⊂ PM (Γ ⊢ G) )
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Pete Olcott
2017-06-13 21:17:35 UTC
Permalink
Raw Message
Post by Pete Olcott
The string of symbols that I provided represents and expression from HOL that is equivalent to the 1931 Incompleteness Theorem in that G( ~Provable(G) ) is neither provable nor refutable for the same reason that the 1931 GIT is neither provable nor refutation.
There quite a number of things wrong with this, it's a bit hard to know where to begin. For starters it is not the Gödel incompleteness theorem which is neither provable nor refutable, it's the Gödel sentence. And when you say "neither provable nor refutable", you have to specify in which formal system. Do you mean the formal system P of Gödel's 1931 paper, which is supposed to be a slightly different version of the system of Principia Mathematica?
https://plato.stanford.edu/entries/goedel-incompleteness/
The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F.

https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
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.

https://en.wikipedia.org/wiki/Truth-bearer
A truth-bearer is an entity that is said to be either true or false and nothing else.

G( ~Provable(G) ) is not a sentence in F because it is not a truth bearer.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Pete Olcott
2017-06-14 14:41:44 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by Pete Olcott
The string of symbols that I provided represents and expression from HOL that is equivalent to the 1931 Incompleteness Theorem in that G( ~Provable(G) ) is neither provable nor refutable for the same reason that the 1931 GIT is neither provable nor refutation.
There quite a number of things wrong with this, it's a bit hard to know where to begin. For starters it is not the Gödel incompleteness theorem which is neither provable nor refutable, it's the Gödel sentence. And when you say "neither provable nor refutable", you have to specify in which formal system. Do you mean the formal system P of Gödel's 1931 paper, which is supposed to be a slightly different version of the system of Principia Mathematica?
https://plato.stanford.edu/entries/goedel-incompleteness/
The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F.
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
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.
https://en.wikipedia.org/wiki/Truth-bearer
A truth-bearer is an entity that is said to be either true or false and nothing else.
G( ~Provable(G) ) is not a sentence in F because it is not a truth bearer..
You are using G to denote the Gödel sentence for the formal system P of Gödel's 1931 paper, and claiming that this sentence hasn't got a truth value?
It is more and less than that. We can (at least for the moment) skip whether or not it applies to the 1931 GIT and simply analyze this expression in isolation:

∀L ∈ Formal_Systems G <assign alias name> ( ~∃Γ ⊂ L (Γ ⊢ G) )

01 ∀ (2)(5)
02 ∈ (3)(4)
03 L
04 Formal Systems
05 ~ (6) // alias for G
06 ∃ (7)(10)
07 ⊂ (8)(3)
08 Γ
09 ⊢ (8)(5) // cycle indicate infinite evaluation loop

Since the above expression never terminates its evaluation with either satisfied or unsatisfied it is not a truth bearer. The expression's pathological self-reference specifies infinite recursion.

After G has been assigned as an alias for the RHS the name G and the expression on the RHS are considered to be identical. The name G is merely a short-hand way of saying the entire RHS.

Tarski confused this when he used the quoted expression as its name. He used names like computer science pointers that had to always be dereferenced prior to use. In Minimal Type Theory expressions are represented in directed acyclic graphs, thus their name is merely the root node of the expression. No dereferencing is ever needed.

Now for the first time ever the pathological self-reference error is formalized. No longer will we merely have some vague idea that self-reference sometimes causes the evaluation of expression to produce unexpected results. Now for the first time ever we can divide the error of pathological self-reference from self-reference that is not erroneous.

This shows five examples of Minimal Type Theory along with their graphs.
http://liarparadox.org/Provability_with_Minimal_Type_Theory.pdf
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Pete Olcott
2017-06-14 14:48:13 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by Pete Olcott
The string of symbols that I provided represents and expression from HOL that is equivalent to the 1931 Incompleteness Theorem in that G( ~Provable(G) ) is neither provable nor refutable for the same reason that the 1931 GIT is neither provable nor refutation.
There quite a number of things wrong with this, it's a bit hard to know where to begin. For starters it is not the Gödel incompleteness theorem which is neither provable nor refutable, it's the Gödel sentence. And when you say "neither provable nor refutable", you have to specify in which formal system. Do you mean the formal system P of Gödel's 1931 paper, which is supposed to be a slightly different version of the system of Principia Mathematica?
https://plato.stanford.edu/entries/goedel-incompleteness/
The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F.
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
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.
https://en.wikipedia.org/wiki/Truth-bearer
A truth-bearer is an entity that is said to be either true or false and nothing else.
G( ~Provable(G) ) is not a sentence in F because it is not a truth bearer.
You are using G to denote the Gödel sentence for the formal system P of Gödel's 1931 paper, and claiming that this sentence hasn't got a truth value?
How do you know Proof() means mathematical proof?
I am defining all of the details of the formalization of logical entailment as it applies to formal languages and natural languages. What-so-ever system that does not conform to this model is an erroneous system, and MTT can point out the exactly error and why it is erroneous.

With the Liar Paradox, the 1931 GIT, and the Truth Teller Paradox the error is that the expressions are infinitely recursive and thus never complete their evaluation. This prevents them from being truth bearers and thus logical sentences of any formal system.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Peter Percival
2017-06-14 14:51:17 UTC
Permalink
Raw Message
Post by Pete Olcott
I am defining all of the details of the formalization of logical
entailment as it applies to formal languages and natural languages.
What-so-ever system that does not conform to this model is an
erroneous system,
Who said that it's your job to lay the law down?
Post by Pete Olcott
and MTT can point out the exactly error and why it
is erroneous.
--
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
Peter Percival
2017-06-15 18:23:10 UTC
Permalink
Raw Message
Post by Pete Olcott
G( ~Provable(G) ) is a simplistic way of saying: G( ~∃Γ ⊂ PM (Γ ⊢ G) )
Neither is the neither-provable-nor-refutable statement of Gödel.
--
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
Pete Olcott
2017-06-14 03:05:08 UTC
Permalink
Raw Message
https://groups.google.com/forum/#!original/comp.theory/2-h0Q98BWr0/BgRbliY-jMkJ
Newsgroups: comp.theory,sci.logic
Subject: Re: The answer to the Halting Problem stored within
Permutations of
Internal States?
Date: Wed, 16 May 2012 23:04:47 -0700 (PDT)
G( ~∃Γ ⊂ PM (Γ ⊢ G) ) // Incompleteness Theorem as a named
predicate
In other words: G( ~Provable(PM, G) )
PROOF(C) =3D C v (PROOF(A) ^ PROOF(B) ^ (A^B->C))
THE PROOF PREDICATE GODEL PROVED DOESN'T EXIST!
C is proven IF c is a theorem in the theory
OR C is derived from other theorems (A^B) in the theory!
It's slightly rearranged from the original specification, a dual
tail
end recursive directed acyclic graph of binary deductions!
Dual Tail End Recursion is REALLY HARD!
especially a DUAL TAIL END RECURSION INTERPRETER (it needs a Dual Tail End Recursion Parsing Procedure)
My formula is actually EQUIVALENT to PROLOG HORN CLAUSES
HORN CLAUSE
(A & B & C & ... Y) -> Z
It looks like that is exactly the same thing as this: (Γ ⊢ G) because this Γ is a set of WFF that would seem to directly correspond to your (apparently sentential) variables.
predicateName ( VAR , VAR , VAR ) :-
tail1 ( VAR , VAR )
tail2 ( VAR )
to Satisfy tail2 you need to GO BACK AND TEST every possible VARIABLE INSTANCE in tail 1. Since PROLOG does this as part of its RUN CYCLE my formula was obsolete!
In my case each sentential variable would represent a relevant WFF of some formal system. When one is looking for a chain-of-inference one can quickly narrow down a sequence of relevant formula from a set of formula.

The relevant formula will be of a specific type. Finite-string transformation rules will simply be hooked together head to tail. If we run out of the right type of heads, we simply end with not provable.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Loading...