Dahn (
Thu, 27 Oct 94 12:31:45 +0100

> Nevertheless, Goedel believed that
> the continuum hypothesis was false and believed that someone would
> come up with more intuitive acceptable axioms and would then be able
> to prove it false.

RIGHT! It's a question of personal believe, not of mathematics.

I agree that Freiling's axiom is appealing and is an argument against the acceptance of the continuum hypothesis. But there are many things in mathematics that are accepted though they are counterintuitive. Gelbaum/Olmstedt "Counterexamples in Analysis" is a nice source for these. In the late 20th many natural subsets of the reals where shown to be either countable or of power continuum (without use of CH). This was considered as an argument in favour of CH.

Everybody is free to add more axioms to mathematics as Freiling did. To be fair, he should prove, that the new axiom will not introduce new inconsistencies into mathematics. If someone proves a useful theorem using Freiling's axiom - that's fine. And he will have shown, that his assertion is true in all models where Freiling's axiom holds. Whether this says something about truth - who knows?

It's my personal view that mathematics is a tool made by humans (ultimately to describe real phenomena). And humans are free to change it. If Freiling's axiom is convincing, you can add it. If CH is - it's also OK. But beware of inconsistencies - you cannot add both. And there is another QED-related aspect: If someone adds an axiom (or a rule of inference) that others don't find convincing, he will lose part of his audience.

After all, this philosophical discussion should not influence QED very much. If QED represents mathematics, there will be most theorems without reference to CH, some using CH and some may use Freiling's axiom. Using QED bookkeeping it should be easy for a user to find out, which QED theorems are proved on the basic of assumptions that he accepts.

> Exercise: Put the above discussionion into PRA. See if another PRA
> fan can figure out what the hell you are talking aobut from reading it.

Nobody - except the people debugging the PRA system - is supposed to understand a theorem from it's code in PRA. But Ken Kunen's paper "A Ramsey Theorem in Boyer-Moore Logic" shows that by use of appropriate tools - notably abbreviations - PRA proofs can be brought back to a level where they can be understood.

Ingo Dahn