Do we all agree that Computer Science definitely should be formalized?
While the definitions of common terms (e.g. recursively enumerable) are
formal, the manipulations of these concepts (e.g. the derivation of
proofs) is not. Can anybody show a single example of a formal
derivation of a result from any branch of Computer Science? For
example:
1. Program Synthesis: The creation of a computer program based on only
its specifications.
2. The Theory of Computation: A formal derivation of Turing’s proof
of the unsolvability of the halting problem.
3. Recursion Theory: A formal proof that there is a program that
outputs itself, or of the Fixed Point theorem or the Recursion theorem.
4. Incompleteness in Logic: A formal derivation of Godel’s
Incompleteness theorems or Rosser’s improvement or Smullyan’s Dual
Form theorem.
Any formalization would include:
A. A formal statement of the theorem or result.
B. The meaning of any such statement.
C. How A corresponds to the statement of the theorem.
D. An algorithm for generating formal statements such as A.
E. A demonstration that D generates A.
F. A demonstration that D generates only true statements.
Curry-Howard, Manna/Waldinger, Boyer/Moore, Modal Logic, Prologue and
TPTP all attempt to do this, but nobody has ever shown any examples of
anything near A-F.
Would we say that formalization is the ultimate goal of every branch of
Computer Science? What problem is not enhanced when expressed
formally?
C-B
"Charlie-Boo" <shymath…@gmail.com> wrote:
> 3. Recursion Theory: A formal proof that there is a program that
> outputs itself…
I have in my possession a program that outputs itself. Therefore
there *is* such a program. Are you asking for a better proof
than that?
–
Alec McKenzie
usenet@<surname>.me.uk
Charlie-Boo wrote:
>Can anybody show a single example of a formal
> derivation of a result from any branch of Computer Science? For
> example:
> 4. Incompleteness in Logic: A formal derivation of Godel’s
> Incompleteness theorems
Well, we know that once the Hilbert-Bernays derivability conditions are
in place, there are easy formal derivation of Con_T –> not-Prov(#G_T),
using # for "the Gödel number of …).
And starting with Hilbert-Bernays there are textbook outlines of formal
proofs that the derivability conditions hold for theories with Sigma_1
induction. See e.g. Boolos’s book.
That looks like a formal derivation to me. What more do you want??
Alec McKenzie wrote:
> "Charlie-Boo" <shymath…@gmail.com> wrote:
> > 3. Recursion Theory: A formal proof that there is a program that
> > outputs itself…
> I have in my possession a program that outputs itself. Therefore
> there *is* such a program. Are you asking for a better proof
> than that?
1. That doesn’t prove the theorem, which must apply to all languages.
It only says it can be done in that language.
In the CBPL2 programming language, the special variable A is equal to
"W A" and W is the command to write a variable, so the program W A also
outputs itself. But does that prove it is so of all programming
languages?
2. Any single specific proof (such as a specific program to prove that
something is true of one language) is vastly improved if we have a
procedure to produce it and lots of other proofs automatically. Isn’t
that obvious?
You haven’t formalized a branch of Computer Science. These are at
opposite ends of the spectrum and is described in A-F that is missing
from your proof.
C-B
- Hide quoted text — Show quoted text -
> —
> Alec McKenzie
> usenet@<surname>.me.uk
Peter_Smith wrote:
> Charlie-Boo wrote:
> >Can anybody show a single example of a formal
> > derivation of a result from any branch of Computer Science? For
> > example:
> > 4. Incompleteness in Logic: A formal derivation of Godel’s
> > Incompleteness theorems
> Well, we know that once the Hilbert-Bernays derivability conditions are
> in place, there are easy formal derivation of Con_T –> not-Prov(#G_T),
> using # for "the Gödel number of …).
It looks like you’re talking aboiut Rosser’s result, but that doesn’t
really matter here.
> And starting with Hilbert-Bernays there are textbook outlines of formal
> proofs that the derivability conditions hold for theories with Sigma_1
> induction. See e.g. Boolos’s book.
> That looks like a formal derivation to me. What more do you want??
A to F:
A. A formal statement of the theorem or result.
B. The meaning of any such statement.
C. How A corresponds to the statement of the theorem.
D. An algorithm for generating formal statements such as A.
E. A demonstration that D generates A.
F. A demonstration that D generates only true statements.
C-B
"Charlie-Boo" <shymath…@gmail.com> wrote:
> Alec McKenzie wrote:
> > "Charlie-Boo" <shymath…@gmail.com> wrote:
> > > 3. Recursion Theory: A formal proof that there is a program that
> > > outputs itself…
> > I have in my possession a program that outputs itself. Therefore
> > there *is* such a program. Are you asking for a better proof
> > than that?
> 1. That doesn’t prove the theorem, which must apply to all languages.
> It only says it can be done in that language.
In which case you must have meant to say "A formal proof that in
every programming language there is a program that outputs
itself".
It seems clear to me that that cannot be true, so there can be
no proof of it, formal or not.
–
Alec McKenzie
usenet@<surname>.me.uk
Peter_Smith wrote:
> Charlie-Boo wrote:
> > 4. Incompleteness in Logic: A formal derivation of Godel’s
> > Incompleteness theorems
> Well, we know that once the Hilbert-Bernays derivability conditions are
> in place, there are easy formal derivation of Con_T –> not-Prov(#G_T),
> using # for "the Gödel number of …).
> And starting with Hilbert-Bernays there are textbook outlines of formal
> proofs that the derivability conditions hold for theories with Sigma_1
> induction. See e.g. Boolos’s book.
> That looks like a formal derivation to me. What more do you want??
This is an odd way of putting it. Godel’s original proof was a formal
derivation. Presumably he just wants it translated from the PM that
Godel had it in, into the 1st-order PA that we use today. But it
doesn’t
have to be translated directly. There are lots of newer better ways to
prove all that. The acutal problem is that that doesn’t initially
appear
to be a computer science result: that is a number theory result.
It is derived from axioms purporting to describe the arithmetic of the
natural numbers. Clearly, what C-B wants instead is for someone
to present a set of basic axioms defining computer science,
where the things in the universe are algorithms instead of sets.
Or where algorithms operate on strings instead of sets. I guess
strings would replace sets as the foundation, and then you could
represent algorithms by strings. That at least seems slightly more
natural and computational than representing them by sets.
But it is unnecessary; you Really Can represent EVERYthing by sets
(it’s just that sometimes it gets cumbersome, or you have to stop
short of your own total universe).
george wrote:
> Godel’s original proof was a formal derivation.
No it wasn’t. Gödel’s original proof was a bit of informal
mathematics. He *claimed* in 1931, at the end of his great paper, that
the informal reasoning could be carried out within the formal
type-theory he labels P. But he didn’t show it there. Tthe first formal
proof was given by Hilbert and Bernays some years later. (Gödel and
Bernays discussed how to do it on a transatlantic vogage. Kreisel has
apparently said that Gödel *dictated* the proof to Bernays.)
On 10 Sep 2006 11:55:26 -0700, Peter_Smith <ps…@cam.ac.uk> said:
> george wrote:
>> Godel’s original proof was a formal derivation.
> No it wasn’t. Gödel’s original proof was a bit of informal
> mathematics. He *claimed* in 1931, at the end of his great paper, that
> the informal reasoning could be carried out within the formal
> type-theory he labels P. But he didn’t show it there. The first formal
> proof was given by Hilbert and Bernays some years later.
Can that proof be found in their Grundlagen der Mathematik? If so, do
you happen to know which volume?
Chris Menzel wrote:
> Can that proof be found in their Grundlagen der Mathematik? If so, do
> you happen to know which volume?
Vol2, pp. 283-340.
Charlie-Boo wrote:
> Do we all agree that Computer Science definitely should be formalized?
What’s the merit in being completely formal, for any branch of
mathematics? Surely it’s enough to convince ourselves that we could
formalize it.
On 10 Sep 2006 14:29:13 -0700, Peter_Smith <ps…@cam.ac.uk> said:
> Chris Menzel wrote:
>> Can that proof be found in their Grundlagen der Mathematik? If so, do
>> you happen to know which volume?
> Vol2, pp. 283-340.
Thanks.
Alec McKenzie wrote:
> In which case you must have meant to say "A formal proof that in
> every programming language there is a program that outputs
> itself".
> It seems clear to me that that cannot be true
Why?
- Hide quoted text — Show quoted text -
> Alec McKenzie
> usenet@<surname>.me.uk
Rupert wrote:
> What’s the merit in being completely formal, for any branch of
> mathematics? Surely it’s enough to convince ourselves that we could
> formalize it.
The question is surely not so much about the merits
of that approach as the POSSIBLITY. People are not
computers. People in general just don’t communicate
in a "completely formal" way. But that does NOT change
the fact that MATH *is* BY DEFINITION *completely* formal;
that is what MAKES it math.
Peter_Smith wrote:
> george wrote:
> > Godel’s original proof was a formal derivation.
> No it wasn’t. Gödel’s original proof was a bit of informal
> mathematics.
The overall outline may have been informal
but this informal shell housed a huge formal
kernel. There is nothing whatsoever informal
about defining a whole bunch of predicates to
construct a Godel sentence. There is nothing
informal about an explicit Godel numbering.
george wrote:
> MATH *is* BY DEFINITION *completely* formal;
> that is what MAKES it math.
george also wrote:
> There is nothing whatsoever informal
> about defining a whole bunch of predicates to
> construct a Godel sentence. There is nothing
> informal about an explicit Godel numbering.
One contrast we might be interested in is fully formalized mathematics
(presented in a formalized language, with the deductions conducted
within some formalized deductive framework — conforming to the
Hilbertian ideal) versus "common-or-garden" mathematics of the kind you
find in typical text books. Now in terms of *that* contrast, it is
quite uncontroversial that lots of mathematics isn’t fully formalized,
and equally quite uncontroversial that e.g. Gödel’s paper is an
exercise in non-formalized mathmetics (it is *about* some fully
formalized mathematics, but it discusses it in a not fully formalized
way). Perhaps the more informal mathematics in some sense aspires to
the status of the fully formalized, but most mathematics plainly isn’t
formalized as it stands
Now if you want to use "completely formal" in some sense that covers
both fully formalized mathematics and common-or-garden mathematical
argument, then you owe us an account of what you mean. Perhaps the idea
is that all mathematics *could* be made fully formal if we put in the
effort? (Though it is far from clear either why that should be so.) But
thinking about the rights and wrongs of that view is running ahead of
ourselves. The question is: what could it mean to say that all
mathematics is *completely* formal just in virtue of being
mathematics. As I say, it is evident that it isn’t all fully formalized
as it stands — so what is being claimed???
> Alec McKenzie wrote [wrongly]:
> > you must have meant to say "A formal proof that in
> > every programming language there is a program that outputs
> > itself".
> > It seems clear to me that that cannot be true
C-B asks,
> Why?
Because there are a lot of simple easy-to-define
programming languages in which you OBVIOUSLY can’t do it,
that’s why. SOME programming languages are LAME.
But despite being right about that, Alec is still wrong in
general; you obviously didn’t mean "every" programming
language; you meant every REASONABLY rich programming
language. By analogy, not all recursive 1st-order theories
are subject to Godelian incompleteness. But all the adequately
powerful ones are.
- Hide quoted text — Show quoted text -
george wrote:
> Peter_Smith wrote:
> > Charlie-Boo wrote:
> > > 4. Incompleteness in Logic: A formal derivation of Godel’s
> > > Incompleteness theorems
> > Well, we know that once the Hilbert-Bernays derivability conditions are
> > in place, there are easy formal derivation of Con_T –> not-Prov(#G_T),
> > using # for "the Gödel number of …).
> > And starting with Hilbert-Bernays there are textbook outlines of formal
> > proofs that the derivability conditions hold for theories with Sigma_1
> > induction. See e.g. Boolos’s book.
> > That looks like a formal derivation to me. What more do you want??
> This is an odd way of putting it. Godel’s original proof was a formal
> derivation. Presumably he just wants it translated from the PM that
> Godel had it in, into the 1st-order PA that we use today. But it
> doesn’t
> have to be translated directly. There are lots of newer better ways to
> prove all that.
Yes! Have you ever seen anything as short as the CBL proof of Rosser
1936?
"If an axiomatic system is decidable and consistent, then its
refutable sentences coincide with its unprovable sentences, but the
former set is r.e while the latter is not." [CBL, 2006]
> The acutal problem is that that doesn’t initially
> appear
> to be a computer science result: that is a number theory result.
Ixnay. The Theory of Computation is a branch of CS. A set is
enumerable by a Turing Machine iff it is representable in Peano
Arithmetic. Godel’s and Turing’s results are related – although
nobody was able to show exactly how when I asked.
I asked what the relationship is between Godel 1931 and Turing 1937
because, to answer this question, you must formalize both of them. And
since it seems that nobody has even done that (without using CBL), that
could be tested by seeing if anyone can say the exact relationship.
The exact relationship is that each is a CBL theorem that uses
different sets of assumptions and rules being applied.
Godel’s 1st.based on soundness: -{ ~PR/TW , PR=>TW, TW=>PR }
1, – ~P/P Axiom (all Incompleteness proofs begin with this axiom.)
2. -{ ~P/P } Notational change
3. -{ ~PR/PR } SUB 2: The set of unprovable sentences is not
representable.
4. -{ ~PR/TW , PR=TW } SUB 3
5. -{ ~PR/TW , PR=>TW , TW=>PR } DEF 4
If unprovability is expressible, then the system is not both sound
and complete.
qed
We can go into further detail:
6. ~PR/TW + PR=>TW => -TW=>PR
If unprovability is expressible, then if sound the system is not
complete.
7. ~PR/TW + PR=>TW => TW(M) + ~PR(M)
If unprovability is expressible, then if sound there is a sentence that
is true and unprovable.
> It is derived from axioms purporting to describe the arithmetic of the
> natural numbers. Clearly, what C-B wants instead is for someone
> to present a set of basic axioms defining computer science,
Well yes, that would do. As it turns out, axioms are what is needed.
I didn’t make it come out that way. That’s just the way it is.
The use of axioms and rules of inferences pervades formal Computer
Science.
The primitive relation is expressed by P=Q(M) where P and Q are
relations and M is an individual element of the universal set,
expressed as M#P/Q in CBL because of variations that are needed such as
P/Q for (eM)M#P/Q and P for P/YES which is P is r.e.
> where the things in the universe are algorithms instead of sets.
> Or where algorithms operate on strings instead of sets.
Wait a minute. If algorithm replaces set, then when you say that
algorithms operate on strings, you are saying that sets operate on
strings. But sets don’t operate on things – functions do. Set just
set there – I mean, sit there.
> I guess
> strings would replace sets as the foundation,
That’s PA.
> and then you could
> represent algorithms by strings.
Fancy that!
> That at least seems slightly more
> natural and computational than representing them by sets.
> But it is unnecessary; you Really Can represent EVERYthing by sets
No. {x|~(xex)} is not a set.
(Its formalization in CBL shows this.)
> (it’s just that sometimes it gets cumbersome, or you have to stop
> short of your own total universe).
All of that is represented formally in CBL. Basically,
1. Computer Science should be formalized.
2. No published paper has formalized any of it. (Definitions alone do
not a formalization make.)
3. CBL formalizes almost all of Computer Science. In particular,
Program Synthesis, Theory of Computation, Recursion Theory and
Incompleteness in Logic are all axiomatized:
Program Synthesis: ADD(I,J,x)* + MUL(I, J,x)*
Theory of Computation: YIT(I,J,K)* + TRUE(x) + – ~YES(x,x) [Kleene,
Peano, Turing]
Recursion Theory: M#f(I) => s11(M,N)#f(N) + s11(I,J) + f(I,J) => f(I,I)
Incompleteness in Logic: -~P/P
(The Rules of Inference are the 8 rules that I describe in my ARXIV
paper.)
Then note the 3 levels of Computer Science displayed here:
1. Incompleteness in Logic: What properties of a formal system are
compatible?
2. Program Synthesis & Theory of Computation: What relations are
representable?
3. Recursion Theory: What relations have representations that have
certain properties?
C-B
Peter_Smith wrote:
> george wrote:
> > Godel’s original proof was a formal derivation.
> No it wasn’t. Gödel’s original proof was a bit of informal
> mathematics. He *claimed* in 1931, at the end of his great paper, that
> the informal reasoning could be carried out within the formal
> type-theory he labels P. But he didn’t show it there. Tthe first formal
> proof was given by Hilbert and Bernays some years later. (Gödel and
> Bernays discussed how to do it on a transatlantic vogage. Kreisel has
> apparently said that Gödel *dictated* the proof to Bernays.)
You’re going to have to define "formal proof" here. Can you present
A-F as I listed? Surely if something is formally proven, then there is
a formal representation of the theorem, a way of generating proofs, a
demonstration that the representation is generated, etc.
Are you suspicious of axiomatic systems that prove only one theorem?
C-B
Rupert wrote:
> Charlie-Boo wrote:
> > Do we all agree that Computer Science definitely should be formalized?
> What’s the merit in being completely formal, for any branch of
> mathematics? Surely it’s enough to convince ourselves that we could
> formalize it.
Why develop mathematics?
Why have people axiomatized branches of mathematics?
Is it better to have a single representation for a theorem rather than
many equivalent representations?
C-B
george wrote:
> Peter_Smith wrote:
> > george wrote:
> > > Godel’s original proof was a formal derivation.
> > No it wasn’t. Gödel’s original proof was a bit of informal
> > mathematics.
> The overall outline may have been informal
> but this informal shell housed a huge formal
> kernel. There is nothing whatsoever informal
> about defining a whole bunch of predicates to
> construct a Godel sentence. There is nothing
> informal about an explicit Godel numbering.
You have to tell in advance an exact algorithm that creates every
proof. You are saying that it can be formalized, but Godel didn’t.
BTW To formalize the results of Godel et. al., it helps to rearrange
the arguments into a "tree structure" of logic. If you formalize it
verbatim, then you have more or less a program that is being defined –
"take wff G. If it is provable, then . . . If it is not provable, then
consider . . ." Then you have to describe what these "programs" in
general accomplish – not so easy! But if you rearrange it so you see
that e.g. the result is showing that P=>Q and Q=>P and then that P==Q,
you can develop rules for constructing these tree structures. (That’s
how CBL does it.)
C-B
george wrote
> Godel’s original proof was a formal derivation.
I wrote
> No it wasn’t. Gödel’s original proof was a bit of informal
> mathematics. He *claimed* in 1931, at the end of his great paper, that
> the informal reasoning could be carried out within the formal
> type-theory he labels P. But he didn’t show it there. Tthe first formal
> proof was given by Hilbert and Bernays some years later.
C-B wrote
> You’re going to have to define "formal proof" here.
Why so? The situation is surely entirely clear and entirely well-known.
(i) Gödel in 1931 showed that a certain sentence is not formally
derivable within the formal system P (a simplified version of the type
theory of Principia). (ii) His argument for this is a bit of ordinary
unformalized mathematical reasoning, rendered as it happens in German,
not within P. (iii) However, there isa sentence of P’s formal language,
call it Th, which – via coding — expresses the result that he has
informally proved. (iv) In 1931, Gödel claimed, but didn’t show, that
there is in fact a formal derivation of this formal arithmetic sentence
Th within the formal theory P itself. (v) Hilbert and Bernays later
showed in considerable detail how to do the derivation within the
formal system P In other words, in the utterly standard textbook sense
of ‘formal proof’, they showed how to give a formal proof of Th in P.
(Well strictly, within variants of P, but the differing details don’t
matter here). No odd or unusual sense of "formal proof" that needs
special explanation is involved.
Charlie-Boo wrote:
> Alec McKenzie wrote:
>> In which case you must have meant to say "A formal proof that in
>> every programming language there is a program that outputs
>> itself".
>> It seems clear to me that that cannot be true
> Why?
Consider, for example, an XML-based Turing Machine description language
in which the tape alphabet is limited to {’0′,’1′,’ ‘}. No program’s
source code can appear on the tape, because every XML document contains
‘<’ etc., yet the language is Turing-complete.
Patricia
george wrote:
> Rupert wrote:
> > What’s the merit in being completely formal, for any branch of
> > mathematics? Surely it’s enough to convince ourselves that we could
> > formalize it.
> The question is surely not so much about the merits
> of that approach as the POSSIBLITY. People are not
> computers. People in general just don’t communicate
> in a "completely formal" way. But that does NOT change
> the fact that MATH *is* BY DEFINITION *completely* formal;
> that is what MAKES it math.
And we can’t communicate Math without being formal, can we?
If Math = Formal, then what does it mean to be formal?
C-B
That’s george, always hot on the trail of a new scoop.
Is physics formal?
Chris Menzel wrote:
> On 10 Sep 2006 14:29:13 -0700, Peter_Smith <ps…@cam.ac.uk> said:
> > Chris Menzel wrote:
> >> Can that proof be found in their Grundlagen der Mathematik? If so, do
> >> you happen to know which volume?
> > Vol2, pp. 283-340.
> Thanks.
I’m do impressed! I want you to write back and tell us all exactly
what it says and just what it means, ‘k?
I think it’s also in Gruntlonger dis Mathemydik Vol. 69 i. 812