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.
I might be misunderstanding you, but it looks like you’re just describing fragments of infinitary logic which has a pretty solid amount of research behind it. Barwise actually developed a model theory for it, you can find a (slightly old) overview here (in part C).
Infinitary logic admits precisely what you’re talking about. For instance; it models sentences with universal and existential quantifiers in N using conjunctions and disjunctions (respectively) over the index ω.
As far as
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.
I don’t think the results of Gödel, Löb and Tarski are necessary to conclude that Platonism is at least pretty questionable. I don’t know where the “mathematics can’t really prove things” bit is coming from—we can prove things in mathematics, and I’ve never really seen people claim otherwise. Are you implicitly attributing something like Absolute Truth to proofs?
Anyway, I’ve been thinking about a naturalistic account of anti-realism for a little while. I’m not convinced it’s fruitful, but Platonism seems totally incomprehensible to me anymore. I can’t see a nice way for it to mesh with what I know about brains and how we form concepts—and the accounts I read can’t give any comprehensible account of what exactly the Platonic realm is supposed to be, nor how we access it. It looks like a nice sounding fiction with a big black box called the Platonic realm that everything we can’t really explain gets stuck into. Nor can I give any kind of real final account of my view of mathematics, because it would at least require some new neuroscience (which I mention in that link).
I will say that I don’t think that mathematics has any special connection with The Real Truth, and I also think that it’s a terrible mistake to think that this is a problem. Truth is evidence based, we figure out the truth by examining our environment. We have extremely strong evidence that math performs well as a framework for organizing information and for reasoning predictively and counterfactually—that it works extremely well in modelling the world around us. I definitely don’t think that it’s reasonable to think that math grants us license to epistemic certainty.
I wouldn’t mind being convinced otherwise, but I’d need an epistemically sound account of Platonism first. I don’t find Tegmark to be super convincing, though I do like that he restricts the MUH to computable structures—but I’m also not sure if that strictly qualifies as Platonism like you seem to be using it. At the very least it gives a moderately constructive account of exactly what is being claimed, which is something I would require from any Platonic theory.
Ha! Yeah, it seems that his name is pretty ubiquitous in mathematical logic, and he wrote or contributed to quite a number of publications. I had a professor for a sequence in mathematical logic who had Barwise as his thesis adviser. The professor obtained his doctoral degree from UW Madison when it still had Barwise, Kleene and Keisler so he would tell stories about some class he had with one or the other of them.
Barwise seems to have had quite a few interesting/powerful ideas. I’ve been wanting to read Vicious Circles for a while now, though I haven’t gotten around to it.
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.
I’ve read your post on Syntacticism and some of your replies to comments. I’m currently looking at the follow up piece (The Apparent Reality of Physics).
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.
I might be misunderstanding you, but it looks like you’re just describing fragments of infinitary logic which has a pretty solid amount of research behind it. Barwise actually developed a model theory for it, you can find a (slightly old) overview here (in part C).
Infinitary logic admits precisely what you’re talking about. For instance; it models sentences with universal and existential quantifiers in N using conjunctions and disjunctions (respectively) over the index ω.
As far as
I don’t think the results of Gödel, Löb and Tarski are necessary to conclude that Platonism is at least pretty questionable. I don’t know where the “mathematics can’t really prove things” bit is coming from—we can prove things in mathematics, and I’ve never really seen people claim otherwise. Are you implicitly attributing something like Absolute Truth to proofs?
Anyway, I’ve been thinking about a naturalistic account of anti-realism for a little while. I’m not convinced it’s fruitful, but Platonism seems totally incomprehensible to me anymore. I can’t see a nice way for it to mesh with what I know about brains and how we form concepts—and the accounts I read can’t give any comprehensible account of what exactly the Platonic realm is supposed to be, nor how we access it. It looks like a nice sounding fiction with a big black box called the Platonic realm that everything we can’t really explain gets stuck into. Nor can I give any kind of real final account of my view of mathematics, because it would at least require some new neuroscience (which I mention in that link).
I will say that I don’t think that mathematics has any special connection with The Real Truth, and I also think that it’s a terrible mistake to think that this is a problem. Truth is evidence based, we figure out the truth by examining our environment. We have extremely strong evidence that math performs well as a framework for organizing information and for reasoning predictively and counterfactually—that it works extremely well in modelling the world around us. I definitely don’t think that it’s reasonable to think that math grants us license to epistemic certainty.
I wouldn’t mind being convinced otherwise, but I’d need an epistemically sound account of Platonism first. I don’t find Tegmark to be super convincing, though I do like that he restricts the MUH to computable structures—but I’m also not sure if that strictly qualifies as Platonism like you seem to be using it. At the very least it gives a moderately constructive account of exactly what is being claimed, which is something I would require from any Platonic theory.
… up until now I thought “barwise” was a technical term.
Ha! Yeah, it seems that his name is pretty ubiquitous in mathematical logic, and he wrote or contributed to quite a number of publications. I had a professor for a sequence in mathematical logic who had Barwise as his thesis adviser. The professor obtained his doctoral degree from UW Madison when it still had Barwise, Kleene and Keisler so he would tell stories about some class he had with one or the other of them.
Barwise seems to have had quite a few interesting/powerful ideas. I’ve been wanting to read Vicious Circles for a while now, though I haven’t gotten around to it.
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.
Have you looked into Univalent foundations at all? There was an interesting talk on it a while ago and it seems as though it might be relevant to your pursuits.
I’ve read your post on Syntacticism and some of your replies to comments. I’m currently looking at the follow up piece (The Apparent Reality of Physics).