**Voting**

The Independent has a story reinforcing my recent comments about shady dealings in electronic voting. It's nice to see this story getting more widespread attention.

I have one nutty idea about how to maybe make a difference: take out
an ad in the IACREOT
newsletter. Unlike the NYT full-page ad idea that's
floating around in blogspace, it would only cost a few hundred bucks,
and it would give a good opportunity to roundly criticize election
officials for rolling over for corrupt corporate merchants of
tamper-friendly voting machines, and encourage them to clearly take
sides. I imagine that very few election officials actively *want*
to preside over one of the darkest eras in democracy facing this
country.

**Google failure**

A couple of followups on my piece on Google's vulnerability to DNS abuse. Charles Cox points out a WebmasterWorld post from a Google person this March that clearly points out that they're aware of the problem and are trying to fix it. I'm not sure exactly why they're still so vulnerable, then.

Also, Andrew Clausen sent me his draft
paper analyzing the attack-resistance of Google and its PageRank
algorithm. I haven't had a chance to study it in detail yet, but from
a skim it looks *very* good. If you're at all interested in trust
issues, it's a must-read

**Proofs**

Thanks, chalst, for your link to the Girard book. I will indeed study it, which should help clear up my ignorance of the finer points of consequence relations and consistency proofs.

I haven't been writing much about my thoughts on proof systems, but I
have been continuing to play with them quite a bit. I've been chipping
away at a prototype of the ideas I wrote about here. It's all based
very solidly on Metamath, but
adds a sound definitional framework (so that axioms and definitions
are clearly separated), and the outline of a modular system so that
individual proofs can import and export "interfaces", and then you can
just wire a big mesh (acyclic network) of these proofs my making the
interfaces match up. I *think* that my current design can do this,
but I'm never certain about things until I implement them.

And perhaps there my goal is a bit overly ambitious for my current
level of ability. I'm trying to cook up not just one set of axioms but
three (based on Z2, HOL, and ZFC, in order of increasing strength), so
that you can write individual proofs using the least powerful
axiomatization necessary, but then use those proofs in any system at
least as strong. Not only that, but I want the theorems proved to be
polymorphic. For example, some of the theorems most interesting to me
are over the structures induced by pairs and "options" (typically
defined as either None or Some *x*). These include sequences,
dictionaries, trees, graphs, and so on, in other words the usual space
of "data structures".

All the axiom systems listed above can easily support these data structures, but just proving your theorems in Z2 is not fully satisfying. If you prove a general theorem about trees, there's no reason it shouldn't work for, say, trees of transfinite ordinals, even though there's no way to represent transfinite ordinals in Z2. Most people designing proof systems just pick an axiomatization. That's part of the reason why it's traditionally difficult to port proofs from one system to another - there's no guarantee you can when the underlying axiomatizations differ. If I'm successful, then proof authors and proof users will be subject to a form of Postel's Law: be conservative in what axioms you need, but liberal in what axioms you can work with.

**Pairs and options in three axiomatizations**

I've never seen these all together like this, and I consider them pretty. They're particularly simple variants of functions that pair up primitive values, and set up option types. The specification of correctness is:

pair(a, b) = pair(a', b') <-> a = a' ^ b = b'

some(a) = some(a') <-> a = a'

some(a) != none().

- Z2:
- pair(a, b) = (a + b) * (a + b) + b * b
- some(a) = a + 1
- none() = 0

- HOL:
- pair(a, b) = \lambda x \lambda y. x = a ^ y = b
- some(a) = \lambda x. x = a
- none() = \lambda x. false

- ZFC:
- pair(a, b) = {{a}, {a, b}}
- some(a) = {a}
- none() = {}