# 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

```

• References:

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