Re: [isabelle] The presentation of Goedel's First Incompleteness Theorem by Lawrence C. Paulson (and others)


There's a very narrow purpose to this email. I accomplish that purpose by what I say in the first few sentences, which is not intended to create any debate.

Picking a nice number, 50, I'll say that at least 50% of what I've said in the past, on technical matters, has been wrong. But taking a position can be the first step in working out ideas, though one person working out an idea can be everybody else getting spammed.

While not technically wrong, since close enough can be good enough, "monolithic logic" wasn't the right choice. A better choice would "black box logic". It's based on a hardware perspective, which I believe is the correct "ultimate view of things" for mechanized proofs. Hex was my friend when looking at address and data buses with a logic analyzer. There's Wikipedia, even when no one needs it:

Related to my "minimal black box interpretation", for an overall view, is my "minimal syntactic interpretation", for logic as strings of characters. For things like this:

  term "THE x. x \<in> {}" (*Do not think beyond the string.*)

lemma "EX! y. y = (THE x. x \<in> {})" (*Totalitarianism. HOL is a tyrant.*)
    by(rule HOL.ex1_eq(1))

Asking no one in particular, I ask and say, "Do you know how annoying it is to read Isabelle list emails on the web archive? Graphical symbols, for \<Rightarrow> and \<Longrightarrow>, get converted to funny looking 'a' symbols."

There is always this open question for me: Do I know enough to do a major disconnect? Being connected can result in more sophistication, but there also should be a fixed foundation. People have been working off of ZFC, for how many years?

Here's a polymorphic vector:

  datatype ('a,'size) vD = vC (vG: "'a list")

The problem of length reflects the general problem of HOL functions being total, and that domains aren't easily restricted, by defining new types. What I have in mind is fixing the problem, in general, by working in null space, which will get lifted to option space. You heard it here first.

The sophistication comes from its use with 'CARD(n)', thanks to a pointer by Manuel Eberl.

I do pull from 'src/HOL/Library', but I stick it all in one file. 'CARD' is thanks to 'Phantom_Type' by Andreas Lochbihler, 'Cardinality' by Brian Huffman & Andreas Lochbihler, and 'Numeral_Type' by Brian Huffman. Lars Noschinski deserves thanks for some other things.

With the new datatype, thanks to Blanchette and Traytel, and whoever else I'm missing, I guess Popescu, there are so many possibilities they become uninteresting, due to the shear number of them.

The 'datatype' keyword itself encapsulates what can be a beautiful form of math, a statement so devoid of detail, it's hard to get the meaning.

The vector is above. Here, possibly, are nested countable and nested finite sets:

  datatype 'a csetD = Atom 'a | csetC "'a csetD cset"

  datatype 'a fsetD = Atom 'a | fsetC "'a fsetD fset"

Here is a possible generalization of nested multisets (using lists):

  datatype 'a msetD = Atom "'a * nat" | msetD "'a msetD list"

Here is what I'm really interested in. Nested sum sets and factor sets combined:

datatype 'a sumfacD = Atom 'a | sumC "'a sumfacD list" | facC "'a sumfacD list"

It uses lists, but why use sets when I can use lists with an equivalence relation, which may lead back to using sets. I don't care about sets anymore, unless I need to. I care about lists, to be used as finite sets.

What's it all worth? Nothing much in an email. The definitions might need to be tweaked, and the devil is in the details.

Consider a quote from Carl Friedrich Gauss:

I confess that Fermat's Theorem as an isolated proposition has very little interest for me, because I could easily lay down a multitude of such propositions, which one could neither prove nor dispose of.

Finishing up unfinished business while the gettin' is good, to put it in amongst a collective gettin'.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.