Delivery-Date:
Date: Thu, 27 Oct 94 12:31:45 +0100
From: dahn@mathematik.hu-berlin.de (Dahn)
Message-Id: <9410271131.AA03022@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: Freiling
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

jmc:
> 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