Gustavo Lacerda

COOL!

From:

simrob.livejournal.com

It feels very much like you're approaching the way the type theorists understand classical logic's "A or not A" - in order to use this fact, you have to create two branches, one that assumes A is true and reasons from there, and another that assumes A is not true and reasons from there.

To "execute" (use) this A or not A fact, just assume A is false. Continue on your merry way - the only way you can ever use the fact "not A" is proving A and developing a contradiction. Okay, well you know what to do if A is true (the other branch!), go from there.

The first branch is the "continue on your merry way" approach. The problem is, I don't think it's sensible to say that, assuming you falsify your assumption, that you can pretend you haven't falsified that assumption - you have to prepare for the other contingency. The only way I would be willing to believe that "axioms that take a long time to be refuted tend to be less significant" would be if it took significantly longer than the time left in the universe to disprove - of course, how would you ever establish such a fact?

From:

I don't understand what special role Busy Beaver plays here. We could just take the Goldbach Conjecture itself as an axiom if we liked - but in both cases we risk finding a counterexample to our axiom in the future.

I am probably very biased by my own peculiar experiences doing math, but I don't see the role of mathematics as "solving problems" so much as "learning which entailments are provable".

If I start with ZFC plus some fact of busy beaver and I prove goldbach, it doesn't really matter whether I write this as

ZFC+BB |- GB

or

ZFG |- BB → GB

That is, I don't see any real difference between taking something as an axiom globally and taking it as an assumption during one proof. People prove statements taking the Riemann Hypothesis and P!=NP all the time.

Edited Date: 2008-04-27 03:02 pm (UTC)

From:

<< I don't understand what special role Busy Beaver plays here. We could just take the Goldbach Conjecture itself as an axiom if we liked >>

The advantage of the former is that all problems up to a certain size become solvable.

From:

Google is returning the favor!

From:

The disadvantage is that you need an axiom for every Turing Machine whose behavior you don't know. So the marginal number of axioms you need to add grows exponentially.

From:

But the ability to "solve" many problems all at once is hardly an advantage as far as I can see if each "solution" has a chance of being unsound and incorrect. The point isn't to increase the raw number of things an axiom system proves, but to increase the number of *correct* things it proves.

From:

Thank goodness physicists disagree with you.

From:

What??

What physicist prefers theories that predict false things?

From:

Maybe I can make my point clearer in the meantime.

Consider theory T that extends S with one more prediction.

If this prediction matches "the world" (be that the physical world or the "platonic realm of pure mathematics") then T is better than S

If it doesn't, T is worse than S.

Adding extremely high-consequence axioms like fixing the value of BB is not progress because for all we know it's adding a bunch of false predictions as well as a bunch of correct ones, without even enhancing our understanding the way an intuitively good (but materially incorrect) physical theory might.

From:

<< Adding extremely high-consequence axioms like fixing the value of BB is not progress because for all we know it's adding a bunch of false predictions as well as a bunch of correct ones, without even enhancing our understanding the way an intuitively good (but materially incorrect) physical theory might. >>

predictions that are false will eventually be refuted. When we are confronted with such a contradiction, we will be left with the problem of "debugging" our axioms: which of our assumptions are false?

if we never add axioms, there are truths that will *never* be recognized as such.

From:

truths that will *never* be recognized as such

are hardly truths at all.

From:

To me, axiom systems try to approximate the Platonic (but very concrete) realm of TMs, but due to Goedel's incompleteness, they never quite get there.

My understanding is you reject LEM here, which would lead me to think that statements about halting are not meaningful to you. If it's meaningful, it must be true or false (our ignorance is a different matter).

From:

1. I don't necessarily believe in a Platonic truth that we will never have access to -- what good is it to suppose a thing exists that we can never really observe? I see Godel's theorem as a statement about the unboundedness of expressive power in hierarchies of mathematical systems: it's not that some things are true but unprovable, but rather that there is always something unprovable which is provable in a stronger system. The important point of the matter is that this regress goes on forever -- and why talk of a Platonic truth if we know we can never achieve it?

2. I believe statements about halting are meaningful, but to me this does not entail believing they are either true or false. I am willing to accept that it is impossible for any statement to be neither true nor false -- so don't expect me to produce any counterexamples -- but i do not regard this as the same as every statement being either true or false. You may find it strange for me to say i accept "not not (A or not A)" while rejecting "A or not A", but i want my proofs to have computational content as constructive decision procedures. A classical tautology like "for every Turing machine M, either M halts or it doesn't" should be unprovable, because we know that the halting problem is undecidable.

3. To illustrate what my philosophy buys me, consider constructing an inference system (say for a logic, or a language -- whatever you like). If i work in an intuitionistic metalogic, then i can easily show my system to be decidable simply by proving that every judgement is either derivable or not -- the proof itself represents a decision procedure! In contrast, if i work classically then the theorem in question has a trivial proof, and if i want to actually show my system decidable, i have to code it up in terms of some computational model like Turing machines or lambda terms (or ... intuitionistic logic! *chuckle*), a vastly more involved enterprise.

4. As a proof theorist, i'd say i'm more interested in the relative strength of assertions than in their supposed absolute truth value. It's nice to be able to say things like, "I can prove first-order logic sound, and it requires only lexicographic induction over tuples of natural numbers", or "I can prove that one can dissect the unit ball into 5 pieces which translate and rotate into two copies of the unit ball, but only if i assume that all propositions are decidable". Are these things Platonically true, false, or meaningless? Who can say -- but at least i understand that the first rests on much simpler foundations. The name of the game is then determining how small a set of assumptions we need to demonstrate a fact, rather than determining how large a set of consequences we can derive if we assume more facts. Your desire to enlarge our provable set by assuming more axioms seems very counterintuitive given my goals -- at the end of the day, you may collect more truths than i, but only truths of a very weak character.

---

This comment is probably far more detailed than you care to read about, but it was a fun exercise anyway, challenging my philosophical assumptions :)

From:

<< why talk of a Platonic truth if we know we can never achieve it? >>

My procedure achieves it in the limit, but it will make temporary mistakes.

<< "I can prove that one can dissect the unit ball into 5 pieces which translate and rotate into two copies of the unit ball, but only if i assume that all propositions are decidable". Are these things Platonically true, false, or meaningless? Who can say -- but at least i understand that the first rests on much simpler foundations. >>

Like you, I am a formalist about questions of this type (because the axioms used are not computational). I am only a Platonist when it comes to TMs.

And frankly, why can't you intuitionists speak normal English and use a provability predicate to make your points? Isn't your meta-language classical already?

From:

Like you, I am a formalist about questions of this type (because the axioms used are not computational). I am only a Platonist when it comes to TMs.

isn't assuming all Turing machines halt or loop equivalent to assuming the excluded middle in general? granted, Banach-Tarski relies on choice, which is stronger than mere excluded middle, but to my mind, LEM is already non-computational enough.

And frankly, why can't you intuitionists speak normal English and use a provability predicate to make your points?

speaking for myself, i sometimes say "true" to mean "provable" because i consider them to mean the same thing. i'm happy to restrict myself to just saying "provable" if it will make things clearer -- is that all you're asking?

Isn't your meta-language classical already?

i'm not sure what you mean by this, but i'm going to have to go with "no" :P

From:

<< isn't assuming all Turing machines halt or loop equivalent to assuming the excluded middle in general? >>

First of all, I only assume that they either halt or don't halt. If all non-halting machines were looping, the halting problem would be easy to solve (proof: make a machine that detects when a TM enters a previous state).

<< i sometimes say "true" to mean "provable" because i consider them to mean the same thing >>

when talking about Turing machines halting, you have a ground truth before you have any axioms. The best you can do is work on your axioms so that they approximate the ground truth. So you shouldn't consider "true" and "provable" to be the same thing.

Edited Date: 2008-04-29 03:55 pm (UTC)

From:

First of all, I only assume that they either halt or don't halt.

we're still in agreement -- by "loop" i didn't mean "cycle to the same configuration".

when talking about Turing machines halting, you have a ground truth before you have any axioms.

i'm still not sure what that means -- like i said above, assuming all Turing machines halt or don't is equivalent to general LEM, since for first-order logic (and beyond), provability is reducible to the halting problem. so to someone who rejects general LEM, it's no more acceptable to say, "well just assume it for Turing machines halting..."

what does it mean to say that a particular Turing machine doesn't halt? if you can provide a proof that it doesn't halt, then i'll believe it, but we know from undecidability than there will be some machines which are neither provably halting nor provably non-halting, so in what sense is there a "ground truth" associated with halting?

(i see Turing machines as a red herring here -- since they enjoy computational universality, pretty much everything interesting can be reduced to Turing machines halting. so as a hypothetical "ground truth", it's no better than other infinitary notions of "truth", like validity in all models or what have you.. and really, it's this infinitary notion of Platonic truth that i object to -- an inaccessible "truth" that we can never know is useless to us. provability, though, i can get my hands on.)

From:

<< but we know from undecidability than there will be some machines which are neither provably halting nor provably non-halting, so in what sense is there a "ground truth" associated with halting? >>

Since "halting" implies "provably halting", the above machines are non-halting.

(In the same sense that a Gödel sentence is true. We say that the property of halting is verifiable but not refutable, i.e. like any Sigma_1 sentence)

From: