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

Greetings,

`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:
`
https://en.wikipedia.org/wiki/Black_box

`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.
`
http://www-groups.dcs.st-and.ac.uk/history/Quotations/Gauss.html

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

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