But you don't have to have unlimited resources, you just have to have X large but finite amount of resources, and you don't know how big X is.

Of course, in order to prove that your resources are sufficient to find the proof, without simply going ahead and trying to find the proof, you would need those resources to be unlimited - because you don't know how big X is. But you still know it's finite. "Feasibly computable" is not the same thing as "computable". "In principle" is, in principle, well defined. "In practice" is not well-defined, because as soon as you have X resources, it becomes possible "in practice" for you to find the proof.

I say again that I do not need to postulate infinities in order to postulate an agent which can find a given proof. For any provable theorem, a sufficiently (finitely) powerful agent can find it (by the above diagonal algorithm); equivalently, an agent of fixed power can find it given sufficient (finite) time. So, while such might be "unfeasible" (whatever that might mean), I can still use it as a step in a justification for the existence of infinities.

It's P(I will find a proof in time t) that is asking for the probability of a definite event. It's not that evaluating this number at large t is so problematic, it's that it doesn't capture what people usually mean by "provable in principle."

Suppose that a proof is a finite sequence of symbols from a finite alphabet (which supposition seems reasonable, at least to me). Suppose that you can determine whether a given sequence constitutes a proof, in finite time (not necessarily bounded). Then construct an ordering on sequences (can be done, it's the union over n in (countable) N of sequences of length n (finitely many), is thus countable), and apply the determination procedure to each one in turn. Then, if a proof exists, you will find it in finite time by this method; thus P(you will find a proof by time t) tends to 1 as t->infty if a proof exists, and is constant 0 forall t if no proof exists.

There's an obvious problem; we can't determine with P=1 that a given sequence constitutes a proof (or does not do so). But suppose becoming 1 bit more sure, when not certain, of the proof-status of a given sequence, can always be done in finite time. Then learn 1 bit about sequence 1, then sequence 1, then seq 2, then seq 1, then seq 2, then seq 3... Then for any sequence, any desired level of certainty is obtained in finite time.

If something is provable in principle, then (with a certain, admittedly contrived and inefficient search algorithm) the proof can be found in finite time with probability 1. No?

One can certainly compute the digits of pi, so that since (as non-intuitionists insist anyway) either the $n$th digit is even, or it is odd, we must have P($n$th digit is even) > P(axioms) or P($n$ digit is odd) > P(axioms).

I don't think that's valid - even if I know (P=1) that there is a fact-of-the-matter about whether the nth digit is even, if I don't have any information causally determined by whether the nth digit is even then I assign P(even) = P(odd) = ½. If I instead only believe with P=P(axioms) that a fact-of-the-matter exists, then I assign P(even) = P(odd) = ½ * P(axioms). Axioms ⇏ even. Axioms ⇒ (even or odd). P(axioms) = P(even or odd) = P(even)+P(odd) = (½ + ½) * P(axioms) = P(axioms), no problem. "A fact-of-the-matter exists for statement A" is (A or ¬A), and assuming that our axioms include Excluded Middle, P(A or ¬A) >= P(axioms).

Summary: P is about my knowledge; existence of a fact-of-the-matter is about, well, the fact-of-the-matter. As far as I can tell, you're confusing map and territory.

I am still arguing with you because I think your misstep poisons more than you have yet realized, not to get on your nerves.

I wasn't suggesting you were trying to get on my nerves. I just think we're talking past each other.

"A proof exists" is a much murkier statement and it is much more difficult to discuss its probability.

As a first approximation, what's wrong with "\lim_{t -> \infty} P(I can find a proof in time t)"?

Also, I don't see why the prior has to be oracular; what's wrong with, say, P(the 3^^^3th decimal digit of pi is even)=½? But then if the digit is X, then surely a proof exists that it is X (because, in principle, the digit can be computed in finitely many steps); it must be some X in [[:digit:]], so if it is even a proof exists that it is even; otherwise (sharp swerve) one does not, and P=½. Not sure about that sharp swerve; if I condition all my probabilities on |arithmetic is consistent) then it's ok. But then, assuming I actually need to do so, the probabilities would be different if conditioned on |arithmetic is inconsistent), and thus by finding a proof, you find evidence for or against the assertion that arithmetic is consistent. But things you can find evidence on, exist! (They are the sheep that determine your pebbles.) So where did I go wrong? (Did I slip a meta-level somewhere? It's possible; I was juggling them a bit.)

lengthiness is not expected to be the only obstacle to finding a proof

True; stick a ceteris paribus in there somewhere.

You are trying to reason about reality from the point of view of a hypothetical entity that has infinite resources.

Not so; I am reasoning about reality in terms of what it is theoretically possible we might conclude with finite resources. It is just that enumerating the collection of things it is theoretically possible we might conclude with finite resources requires infinite resources (and may not be possible even then). Fortunately I do not require an enumeration of this collection.

I am certainly not saying that feasible proofs cause things to be true. Our previous slow computer and our new fast computer cause exactly the same number of important things to be true: none at all. That is the formalist position, anyway.

So either things that are unfeasible to prove can nonetheless be true, or nothing is true. So why does feasibility matter again?

P(I will prove the negation of your theorem in fewer than m+1 minutes) = p

No, it is > p. P(I will prove 1=0 in fewer than m+1 minutes) = p + epsilon. P(I will prove 1+1=2 in fewer than m+1 minues) = nearly 1. This is because you don't know whether my proof was correct.

Paul Almond

To Minds, Substrate, Measure and Value Part 2: Extra Information About Substrate Dependence I make his Objection 9 and am not satisfied with his answer to it. I believe there is a directed graph (possibly cyclic) of mathematical structures containing simulations of other mathematical structures (where the causal relation proceeds from the simulated to the simulator), and I suspect that if we treat this graph as a Markov chain and find its invariant distribution, that this might then give us a statistical measure of the probability of being in each structure, without having to have a concept of a physical substrate which all other substrates eventually reduce to.

However, I'm not sure that any of this is essential to my OP claims; the measure I assign to structures for purposes of forecasting the future is a property of my map, not of the territory, and there needn't be a territorial measure of 'realness' attached to each structure, any more than there need be a boolean property of 'realness' attached to each structure. I note, though, that, being unable to explain why I find myself in an Everett branch in which experiments have confirmed the Born rule (even though in many worlds (without mangling) there should be a 'me' in a branch in which experiments have consistently confirmed the Equal Probabilities rule), I clearly do not have an intuitive grasp of probabilities in a possible-worlds or modal-realistic universe, so I may well be barking up the wrong giraffe.

EDIT: In part 3, Almond characterises the Strong AI Hypothesis thus:

A mind exists when the appropriate algorithm is being run on a physical system.

I characterise my own position on minds thus:

A mind exists when there is an appropriate algorithm, whether that algorithm is being run on a physical system or not. If the existence-of-mind inheres in the interpretative algorithm rather than the algorithm-that-might-be-run, then the interpretative algorithm is the appropriate one; but the mind still exists, whether the interpretative algorithm is being run on a physical system or not.

This is because the idea of a 'physical system' is an attachment to physical realism which I reject in the OP.

But then, how do you determine whether information exists-in-the-universe at all? Does the number 2 exist-in-the-universe? (I can pick up 2 pebbles, so I'm guessing 'yes'.) Does the number 3^^^3 exist-in-the-universe? Does the number N = total count of particles in the universe exist-in-the-universe? (I'm guessing 'yes', because it's represented by the universe.) Does N+1 exist-in-the-universe? (After all, I can consider {particles in the universe} union {{particles in the universe}}, with cardinality N+1) If you allow encodings other than unary, let N = largest number which can be represented using all the particles in the universe. But I can coherently talk about N+1, because I don't need to know the value of a number to do arithmetic on it (if N is even, then N+1 is odd, even though I can't represent the value of N+1). Does the set of natural numbers exist-in-the-universe? If so, I can induct - and therefore, by induction on induction itself, I claim I can perform transfinite induction (aka 'scary dots') in which case the first uncountable ordinal exists-in-the-universe, which is something I'd quite like to conclude.

So where does it stop being a heap?

I am aware it can be very small. The only sense in which I claimed otherwise was by a poor choice of wording. The use I made of the claim that "Agents implementing the same deduction rules and starting from the same axioms tend to converge on the same set of theorems" was to argue for the proposition that there is a fact-of-the-matter about which theorems are provable in a given system. You accept that my finding a proof causes you to update P(you can find a proof) upwards by a strictly positive amount - from which I infer that you accept that there is a fact-of-the-matter as to whether a proof exists. In which case, you are not arguing with my conclusion, merely with a step I used in deriving it - a step I have replaced - so does that not screen off my conclusion from that step - so why are you still arguing with me?

Your conclusion on truth is a physical state in your mind, generated by physical processes. The existence of a metaphysical truth is not required for you to come to that conclusion.

I think a meta- has gone missing here: I can't be certain that others tend to reach the same truth (rather than funny hats), and I can't be certain that 2+2=4. I can't even be certain that there is a fact-of-the-matter about whether 2+2=4. But it seems damned likely, given Occamian priors, that there is a fact-of-the-matter about whether 2+2=4 (and, inasmuch as a reflective mind can have evidence for anything, which has to be justified through a strange loop on the bedrock, I have strong evidence that 2+2 does indeed equal 4).

That "truth" in the map doesn't imply truth in the territory, I accept. That there is no truth in the territory, I vehemently reject. If two minds implement the same computation, and reach different answers, then I simply do not believe that they were really implementing the same computation. If you compute 2+2 but get struck by a cosmic ray that flips a bit and makes you conclude "5!", then you actually implemented the computation "2+2 with such-and-such a cosmic ray bitflip".

I am not able to comprehend the workings of a mind which believes arithmetic truth to be a property only of minds, any more than I am able to comprehend a mind which believes sheep to be a property only of buckets. Your conclusion on sheep is a physical state in your mind, generated by physical processes. But the sheep still exist outside of your mind.

A positive but minuscule amount.

Right - but if there were no 'fact-of-the-matter' as to whether a proof exists, why should it be non-zero at all?