ec429

Karma: 133

ec429 Dec 31, 2011, 6:05 PM
0 points
in reply to: Zetetic’s comment on: So You Want to Save the World
Hmm, infinitary logic looks interesting (I’ll read right through it later, but I’m not entirely sure it covers what I’m trying to do). As for Platonism, mathematical realism, and Tegmark, before discussing these things I’d like to check whether you’ve read http://lesswrong.com/r/discussion/lw/7r9/syntacticism/ setting out my position on the ontological status of mathematics, and http://lesswrong.com/lw/7rj/the_apparent_reality_of_physics/ on my version of Tegmark-like ideas? I’d rather not repeat all that bit by bit in conversation.

ec429 Dec 28, 2011, 9:21 PM
0 points
in reply to: cousin_it’s comment on: So You Want to Save the World
The computer program ‘holds the belief that’ this way-powerful system exists; while it can’t implement arbitrary transfinite proofs (because it doesn’t have access to hypercomputation), it can still modify its own source code without losing a meta each time: it can prove its new source code will increase utility over its old, without its new source code losing proof-power (as would happen if it only ‘believed’ PA+n; after n provably-correct rewrites it would only believe PA, and not PA+1. Once you get down to just PA, you have a What The Tortoise Said To Achilles-type problem; just because you’ve proved it, why should you believe it’s true?

The trick to making way-powerful systems is not to add more and more Con() or induction postulates—those are axioms. I’m adding transfinite inference rules. As well as all the inference rules like modus ponens, we have one saying something like “if I can construct a transfinite sequence of symbols, and map those symbols to syntactic string-rewrite operations, then the-result-of the corresponding sequence of rewrites is a valid production”. Thus, for instance, w-inference is stronger than adding w layers of Con(), because it would take a proof of length at least w to use all w layers of Con().

This is why I call it metasyntax; you’re considering what would happen if you applied syntactic productions transfinitely many times.

I don’t know, in detail, how to express the notion that the program should “trust” such a system, because I don’t really know how a program can “trust” any system: I haven’t ever worked with/on automated theorem provers, nor any kind of ‘neat AI’; my AGI experiments to date have all been ‘scruffy’ (and I stopped doing them when I read EY on FAI, because if they were to succeed (which they obviously won’t, my neural net did nothing but talk a load of unintelligible gibberish about brazil nuts and tetrahedrite) they wouldn’t even know what human values were, let alone incorporate them into whatever kind of decision algorithm they ended up having).

I’m really as much discussing how human mathematicians can trust mathematics as I am how AIs can trust mathematics—when we have all that Gödel and Löb and Tarski stuff flying around, some people are tempted to say “Oh, mathematics can’t really prove things, therefore not-Platonism and not-infinities”, which I think is a mistake.

ec429 Dec 28, 2011, 7:00 PM
0 points
in reply to: cousin_it’s comment on: So You Want to Save the World

Can you explain more formally what you mean by “proves that it itself exists”?

The fundamental principle of Syntacticism is that the derivations of a formal system are fully determined by the axioms and inference rules of that formal system. By proving that the ordinal kappa is a coherent concept, I prove that PA+kappa is too; thus the derivations of PA+kappa are fully determined and exist-in-Tegmark-space.

Actually it’s not PA+kappa that’s ‘reflectively consistent’; it’s an AI which uses PA+kappa as the basis of its trust in mathematics that’s reflectively consistent, for no matter how many times it rewrites itself, nor how deeply iterated the metasyntax it uses to do the maths by which it decides how to rewrite itself, it retains just as much trust in the validity of mathematics as it did when it started. Attempting to achieve this more directly, by PA+self, runs into Löb’s theorem.

ec429 Dec 28, 2011, 6:52 PM
1 point
in reply to: cousin_it’s comment on: So You Want to Save the World
Well, I’m not exactly an expert either (though next term at uni I’m taking a course on Logic and Set Theory, which will help), but I’m pretty sure this isn’t the same thing as proof-theoretic ordinals.

You see, proofs in formal systems are generally considered to be constrained to have finite length. What I’m trying to talk about here is the construction of metasyntaxes in which, if A1, A2, … are valid derivations (indexed in a natural and canonical way by the finite ordinals), then Aw is a valid derivation for ordinals w smaller than some given ordinal. A nice way to think about this is, in (traditionally-modelled) PA the set of numbers contains the naturals, because for any natural number n, you can construct the n-th iterate of ⁺ (successor) and apply it to 0. However, the set of numbers doesn’t contain w, because to obtain that by successor application, you’d have to construct the w-th iterate of ⁺, and in the usual metasyntax infinite iterates are not allowed.

Higher-order logics are often considered to talk about infinite proofs in lower-order logics (eg. every time you quantify over something infinite, you do something that would take infinite proving in a logic without quantifiers), but they do this in a semantic way, which I as a Syntacticist reject; I am doing it in a syntactic way, considering only the results of transfinitely iterated valid derivations in the low-order logic.

As far as I’m aware, there has not been a great deal of study of metasyntax. It seems to me that (under the Curry-Howard isomorphism) transfinite-iteration metasyntax corresponds to hypercomputation, which is possibly why my kappa is (almost certainly) much, much larger than the Church-Kleene ordinal which (according to Wikipedia, anyway) is a strict upper bound on proof-theoretic ordinals of theories. w₁CK is smaller even than w₁, so I don’t see how it can be larger than kappa.

ec429 Dec 28, 2011, 6:32 PM
0 points
in reply to: bogdanb’s comment on: The Apparent Reality of Physics
I think that’s a very good summary indeed, in particular that the “unique non-ambiguous set of derivations” is what imbues the syntax with ‘reality’.

Symbols are indeed not defined, but the only means we have of duck-typing symbols is to do so symbolically (a symbol S is an object supporting an equality operator = with other symbols). You mention Lisp; the best mental model of symbols is Lisp gensyms (which, again, are objects supporting only one operator, equality).

conses of conses are indeed a common model of strings, but I’m not sure whether that matters—we’re interested in the syntax itself considered abstractly, rather than any representation of the syntax. Since ad-hoc infinite regress is not allowed, we must take something as primal (just as formal mathematics takes the ‘set’ as primal and constructs everything from set theory) and that is what I do with syntax.

As mathematics starts with axioms about sets and inference rules about sets, so I begin with meta-axioms about syntax and meta-inference rules about syntax. (I then—somewhat reflexively—consider meta²-axioms, then transfinitely induct. It’s a habit I’ve developed lately; a current project of mine is to work out how large a large ordinal kappa must be such that meta^kappa -syntax will prove the existence of ordinals larger than kappa, and then (by transfinite recursion shorter than kappa) prove the existence of [a given large cardinal, or the Von Neumann universe, or some other desired ‘big’ entity]. But that’s a topic for another post, I fear)

ec429 Dec 28, 2011, 6:07 PM
6 points
in reply to: [deleted]’s comment on: So You Want to Save the World
Now I see why TDT has been causing me unease—you’re spot on that the 5-and-10 problem is Löbbish, but what’s more important to me is that TDT in general tries to be reflective. Indeed, Eliezer on decision theory seems to be all about reflective consistency, and to me reflective consistency looks a lot like PA+Self.

A possible route to a solution (to the Löb problem Eliezer discusses in “Yudkowsky (2011a)”) that I’d like to propose is as follows: we know how to construct P+1, P+2, … P+w, etc. (forall Q, Q+1 = Q u {forall S, [](Q|-S)|-S}). We also know how to do transfinite ordinal induction… and we know that the supremum of all transfinite countable ordinals is the first uncountable ordinal, which corresponds to the cardinal aleph_1 (though ISTR Eliezer isn’t happy with this sort of thing). So, P+Ω won’t lose reflective trust for any countably-inducted proof, and our AI/DT will trust maths up to countable induction.

However, it won’t trust scary transfinite induction in general—for that, we need a suitably large cardinal, which I’ll call kappa, and then P+kappa reflectively trusts any proof whose length is smaller than kappa; we may in fact be able to define a large cardinal property, of a kappa such that PA+(the initial ordinal of kappa) can prove the existence of cardinals as large as kappa. Such a large cardinal may be too strong for existing set theories (in fact, the reason I chose the letter kappa is because my hunch is that Reinhardt cardinals would do the trick, and they’re inconsistent with ZFC). Nonetheless, if we can obtain such a large cardinal, we have a reflectively consistent system without self-reference: PA+w_kappa doesn’t actually prove itself consistent, but it does prove kappa to exist and thus proves that it itself exists, which to a Syntacticist is good enough (since formal systems are fully determined).

ec429 Dec 28, 2011, 2:46 AM
0 points
in reply to: bogdanb’s comment on: The Apparent Reality of Physics
Oh, I’m willing to admit variously infinite numbers of applications of the rules… that’s why transfinite induction doesn’t bother me in the slightest.

But, my objection to the existence of abstract points is: what’s the definition of a point? It’s defined by what it does, by duck-typing. For instance, a point in R² is an ordered pair of reals. Now, you could say “an ordered pair (x,y) is the set {x,{x,y}}”, but that’s silly, that’s not what an ordered pair is, it’s just a construction that exhibits the required behaviour: namely, a constructor from two input values, and an equality axiom “(a,b)==(c,d) iff a==c and b==d”. Yet, from a formal perspective at least, there are many models of those axiomata, and it’s absurd to claim that any one of those is what a point “is”—far more sensible to say that the point “is” its axiomata. Since those axiomata essentially consist of a list of valid string-rewriting rules (like (a,b)==(c,d) |- a==c), they are directly and explicitly syntactic.

Perhaps, indeed, there is a system more fundamental to mathematics than syntactics—but given that the classes of formal languages even over finite strings are “variously infinite” (since language classes are equivalent to computability classes, by something Curry-Howardesque), it seems to me that, by accepting variously infinite strings and running-times, one should find that all mathematical systems are inherently syntactic in nature.

Sadly this is difficult to prove, as all our existing formal methods are themselves explicitly syntactic and thus anything we can express formally by current means, we can express as syntax. If materialistic and mechanistic ideas about the nature of consciousness are valid, then in fact any mathematics conceivable by human thought are susceptible to syntactic interpretation (for, ultimately, there exists a “validity” predicate over mathematical deductions, and assuming that validity predicate is constant in all factors other than the mathematical deduction itself (which assumption I believe to hold, as I am a Platonist), that predicate has a syntactic expression though possibly one derived via the physics of the brain). This does not, however, rule out the possibility that there are things we might want to call ‘formal systems’ which are not syntactic in nature. It is my belief—and nothing more than that—that such things do not exist.

ec429 Dec 18, 2011, 6:10 PM
0 points
in reply to: bogdanb’s comment on: The Apparent Reality of Physics
The locus exists, as a mathematical object (it’s the string “{x \in R²: |x|=r}”, not the set {x \in R² : |x|=r}). The “circle” on the other hand is a collection of points. You can apply syntactic (ie. mathematical) operators to a mathematical object; you can’t apply syntactic operators to a collection of points. It is syntactic systems and their productions (ie. mathematical systems and their strings) which exist.

ec429 Dec 6, 2011, 9:01 PM
0 points
on: The mathematical universe: the map that is the territory
I have also (disappointingly/validatingly) thought of this and then read Tegmark. (It’s even more disappointing/validating than that, though, since as well as Tegmark, you appear to have invented Syntacticism. You even have all my arguments, like subverting the simulation hypothesis and talking about ‘closure’). However, I have one more thing to add, which may answer the problem of regularity. That one thing is what I call the ‘causality manifold’: Obviously by simulating a universe we have no causal effect upon it (if we are assuming the mathematical universe hypothesis); but it has a causal effect upon us, because it defines the results of our computation. I explore this theme somewhat in The Apparent Reality of Physics, a footnote to which mentions the problem of consistency when you have a closed loop of universes, and its putative solvability by loop unfolding / closure. Considering the ensemble of mathematical structures with the natural topology, we see that locally it’s either a graph or a manifold (almost everywhere), and it has this flow defined by the causal relations (with the flow in the opposite direction to simulation), which we can consider as being a flow of subjective probability (with some equilibrium state). Of course it contains both regular and irregular universes (hereonin RUs and IUs), because adding a delta function to a differential equation gives you, simply, a different DE (well, that’s ‘morally’ why it’s true; it’s more complicated in practice because not all mathematical structures are DEs; but any continuous mathematical structure can be continuously corrupted). IUs typically cannot simulate RUs, because any simulation is going to keep hitting the delta functions and being corrupted; RUs, on the other hand, can simulate both other RUs and IUs (a cosmic ray can turn your RU simulation into an IU simulation). Consequently, subjective probability flows from {IUs} to {RUs} much more strongly than the other way, so the equilibrium has most subjective probability on RUs. Thus, anthropics and cake for everyone :)

I should add that I haven’t yet been able to mathematically formalise the above argument, because I haven’t yet worked out the correct definitions/characterisation of the ‘causality manifold’ (which is, incidentally, not a manifold), and it’s possible that the small probability of an IU simulating a RU screws things up, and that we should (perhaps) expect to find ourselves in a Universe with some (say) Poisson-distributed degree of irregularity. Or something like that. But, at least it does allow for a mathematical universe in which anthropic experience can actually be given a probability distribution.

ec429 Dec 5, 2011, 10:30 PM
1 point
in reply to: lessdazed’s comment on: Counterfactual Mugging
Yes, it still works, because of the way the subjective probability flow on Tegmark-space works. (Think of it like PageRank, and remember that the s.p. flows from the simulated to the simulator)

It is technically possible that the differences between how much the two Universes simulate each other can, when combined with differences in how much they are simulated by other Universes, can cause the coupling between the two not to be strong enough to override some other couplings, with the result that the s.p. expectation of “giving Omega the $100” is negative. However, under my current state of logical uncertainty about the couplings, that outcome is rather unlikely, so taking a further expectation over my guesses of how likely various couplings are, the deal is still a good one.

Actually, in my own thinking I no longer call it “Tegmark-space”, instead I call it the “Causality Manifold” and I’m working on trying to find a formal mathematical expression of how causal loop unfolding can work in a continuous context. Also, I’m no longer worried about the “purer and more elegant version” of syntacticism, because today I worked out how to explain the subjective favouring of regular universes (over irregular ones, which are much more numerous). One thing that does worry me, though, is that every possible Causality Manifold is also an element of the CM, which means either stupidly large cardinal axioms or some kind of variant of the “No Gödels” argument from Syntacticism (the article).

ec429 Dec 4, 2011, 3:48 PM
2 points
on: Counterfactual Mugging
Under my syntacticist cosmology, which is a kind of Tegmarkian/Almondian crossover (with measure flowing along the seemingly ‘backward’ causal relations), the answer becomes trivially “yes, give Omega the $100” because counterfactual-me exists. In fact, since this-Omega simulates counterfactual-me and counterfactual-Omega simulates this-me, the (backwards) flow of measure ensures that the subjective probabilities of finding myself in real-me and counterfactual-me must be fairly close together; consequently this remains my decision even in the Almondian variety. The purer and more elegant version of syntacticism doesn’t place a measure on the Tegmark-space at all, but that makes it difficult to explain the regularity of our universe—without a probability distribution on Tegmark-space, you can’t even mathematically approach anthropics. However, in that version counterfactual-me ‘exists to the same extent that I do’, and so again the answer is trivially “give Omega the $100″.

Counterfactual problems can be solved in general by taking one’s utilitarian summation over all of syntax-space rather than merely one’s own Universe/hubble bubble/Everett branch. The outstanding problem is whether syntax-space should have a measure and if so what its nature is (and whether this measure can be computed).

ec429 Dec 4, 2011, 3:45 PM
0 points
in reply to: bogdanb’s comment on: The Apparent Reality of Physics
Indeed. Circles are merely a map-tool geometers use to understand the underlying territory of Euclidean geometry, which is precisely real vector spaces (which can be studied axiomatically without ever using the word ‘circle’). So, circles don’t exist, but {x \in R² : |x|=r} does. (Plane geometry is one model of the formal system)

ec429 Sep 24, 2011, 7:25 PM
0 points
in reply to: Zetetic’s comment on: Syntacticism

It doesn’t seem odd at all, we have an expectation of the calculator, and if it fails to fulfill that expectation then we start to doubt that it is, in fact, what we thought it was (a working calculator).

Except that if you examine the workings of a calculator that does agree with us, you’re much much less likely to find a wiring fault (that is, that it’s implementing a different algorithm).

if (a) [a reasonable human would agree implements arithmetic] and (b) [which disagrees with us on whether 2+2 equals 4] both hold, then (c) [The human decides she ve was mistaken and needs to fix the machine]. If the human can alter the machine so as to make it agree with 2+2 = 4, then and only then will the human feel justified in asserting that it implements arithmetic.

If the only value for which the machine disagrees with us is 2+2, and the human adds a trap to detect the case “Has been asked 2+2”, which overrides the usual algorithm and just outputs 4… would the human then claim they’d “made it implement arithmetic”? I don’t think so.

I’ll try a different tack: an implementation of arithmetic can be created which is general and compact (in a Solomonoff sense) - we are able to make calculators rather than Artificial Arithmeticians. Clearly not all concepts can be compressed in this manner, by a counting argument. So there is a fact-of-the-matter that “these {foo} are the concepts which can be compressed by thus-and-such algorithm” (For instance, arithmetic on integers up to N can be formalised in O(log N) bits, which grows strictly slower than O(N); thus integer arithmetic is compressed by positional numeral systems). That fact-of-the-matter would still be true if there were no humans around to implement arithmetic, and it would still be true in Ancient Rome where they haven’t heard of positional numeral systems (though their system still beats the Artificial Arithmetician).

I’ll look over it, but given what you say here I’m not confident that it won’t be an attempt at a resurrection of Platonism.

What’s wrong with resurrecting (or rather, reformulating) Platonism? Although, it’s more a Platonic Formalism than straight Platonism.

ec429 Sep 24, 2011, 7:07 PM
1 point
in reply to: ArisKatsaris’s comment on: The Apparent Reality of Physics

I don’t understand the meaning of the word “symbols” in the abstract, without a brain to interpret them with and map them onto reality.

Think in terms of LISP gensyms—objects which themselves support only one operation, ==. The only thing we can say about (rg45t) is that it’s the same as (rg45t) but not the same as (2qox), whereas we think we know what (forall) means (in the game of set theory) - in fact the only reason (forall) has a meaning is because some of our symbol-manipulating rules mention it.

ec429 Sep 24, 2011, 7:04 PM
0 points
in reply to: bogdanb’s comment on: The Apparent Reality of Physics

I think ec429 “sides” with the first intuition, and you tend more towards the second. I just noticed I am confused.

No, I’d say nearer the second—the mathematical expression of the world of P2 “exists” indifferently of us, and has just as much “existence” as we do. Rocks and trees and leptons, and their equivalents in P2-world, however, don’t “exist”; only their corresponding ‘pieces of math’ flowing through the equations can be said to “exist”.

ec429 Sep 24, 2011, 7:12 AM
0 points
in reply to: Zetetic’s comment on: Syntacticism

What is clear to me is that when we set up a physical system (such as a Von Neumann machine, or a human who has been ‘set up’ by being educated and then asked a certain question) in a certain way, some part of the future state of that system is (say with 99.999% likelihood) recognizable to us as output (perhaps certain patterns of light resonate with us as “the correct answer”)

But note that there are also patterns of light which we would interpret as “the wrong answer”. If arithmetic is implementation-dependent, isn’t it a bit odd that whenever we build a calculator that outputs “5″ for 2+2, it turns out to have something we would consider to be a wiring fault (so that it is not implementing arithmetic)? Can you point to a machine (or an idealised abstract algorithm, for that matter) which a reasonable human would agree implements arithmetic, but which disagrees with us on whether 2+2 equals 4? Because, if arithmetic is implementation-dependent, you should be able to do so.

Are we then to take computation as “more fundamental” than physics?

Yes! (So long as we define computation as “abstract manipulation-rules on syntactic tokens”, and don’t make any condition about the computation’s having been implemented on any substrate.)

ec429 Sep 24, 2011, 7:05 AM
0 points
in reply to: David_Allen’s comment on: Syntacticism

When you look at the statement 2+2=4 you think some form of “hey, that’s true”. When I look at the statement, I also think some form of “hey, that’s true”. We can then talk and both come to our own unique conclusion that the other person agrees with us.

I think your argument involves reflection somewhere. The desk calculator agrees that 2+2=4, and it’s not reflective. Putting two pebbles next to two pebbles also agrees.

Look at the discussion under this comment; I maintain that cognitive agents converge, even if their only common context is modus ponens—and that this implies there is something to be converged upon. At the least, it is ‘true’ that that-which-cognitive-agents-converge-on takes the value that it does (rather than any other value, like “1=0”).

These processes explain your observations and operate entirely within the physical universe. The concept of metaphysical existence is not needed.

Mathematical realism also explains my observations and operates entirely within the mathematical universe; the concept of physical existence is not needed. The ‘physical existence hypothesis’ has the burdensome detail that extant physical reality follows mathematical laws; I do not see a corresponding burdensome detail on the ‘mathematical realism hypothesis’. Thus by Occam, I conclude mathematical realism and no physical existence.

I am not sure I have answered your objections because I am not sure I understand them; if I do not, then I plead merely that it’s 8AM, I’ve been up all night, and I need some sleep :(

ec429 Sep 24, 2011, 6:51 AM
0 points
in reply to: [deleted]’s comment on: Syntacticism
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.

ec429 Sep 24, 2011, 4:51 AM
1 point
in reply to: [deleted]’s comment on: Syntacticism

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?

ec429 24 Sep 2011 4:38 UTC
0 points
in reply to: [deleted]’s comment on: Syntacticism

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.