I got lost while trying to follow this (at least in my case, you were very wrong about this being more comprehensible and intuitive than your previous post), and eventually I figured out that I didn’t even understand your notation.
Is #[stuff] just the inverse of repr? If so, why do you keep using “#[&stuff]” instead of just “stuff”? If not, what is it?
And in “For all x: If K>0, and PPT.3 |- #[&F](&x), then #[down(F(‘x’))]”, I assume that ” ‘x’ ” means something different from “&x”, “#[&x]”, or “x” because otherwise you just would have used whichever of those was appropriate. Later on, you say ” “#[down(F(‘x’))]” splices in a formula with free variable ‘x’ ”, but I’m not sure what you mean by that. ‘x’ obviously isn’t a free variable because it appears inside the quantifier “for all x: …”.
Thanks for your feedback, and for trying to follow the proof! Clearly I underestimated the inferential distance when I wrote that ”...” and #[...] work just like Lisp’s backquote and comma, and then more or less left it at that :-)
Let’s try whether some examples help—let’s introduce some functions for constructing Gödel numbers explicitly, and then see what the quote/splice notation desugars to. We already know repr(n), written &n, which returns the Gödel number of the representation of n as a unary numeral. Let ge(x,y) be a function taking the Gödel numbers of two expressions, and returning the formula saying that the first expression is >= the second expression. For example,
ge(&3, &7) = "3 >= 7".
Similarly, define plus(x,y) as taking the Gödel numbers of two expressions, and returning the Gödel number of another expression, so that
ge(plus(&2, &2), &3) = "(2+2) >= 3".
(I hope that made sense?) -- In both of these cases, the quotation on the right-hand side is actually syntactic sugar for the left-hand side.
Now, let’s look at an example of what a quoted expression with a splice desugars to.
"(2+2) >= #[x]" = ge(plus(&2, &2), x).
So, here x is the Gödel number of an expression that gets inserted on the right-hand side of the >=. For example, if you define a function f(x) := “(2+2) >= #[x]”, and then apply that to the value “1+1″ = plus(&1, &1), then you get
Now, sometimes you don’t want to insert an arbitrary expression, but you have a particular value you want to insert. Perhaps you have a number n, and you want to construct an expression saying that n is at least 7. Now what you do is to use & to turn n into the Gödel number of an expression, and then splice in that expression:
"#[&n] >= 7" = ge(&n, &7).
Does that help with the question of what #[...] means? This comment is getting long so I’ll move on to the second question, but please ask more if it’s still unclear.
In the F(e) notation, F is the Gödel number of an expression that may contain blanks, like F = “_ < 12”, and e is the Gödel number of some expression, like e = “2+2″. Then, F(e) is the Gödel number of the expression obtained by substituting e for the blanks: in the example, F(e) = “2+2 < 12”.
Let’s stick with our example F. ‘x’ is the Gödel number of the variable x, so F(‘x’) = “x < 12”. On the other hand, &x denotes the unary representation of the current value of x, so if x=17, then F(&x) = “17 < 12“. Back to the first hand, if x=17, then you still have F(‘x’) = “x < 12”, because ‘x’ is just a fixed Gödel number, it doesn’t depend on the value of the variable x. (Just as in Python, the string literal ‘x’ has the same value no matter what the variable x is bound to.) F(x) is only useful if the current value of x is the Gödel number of an expression; if x=”1+1“, then F(x) = “1+1 < 12”. Finally, F(#[&x]) wouldn’t make sense in this place, because the #[...] notation can only appear inside a string. Well, it may look as if the place you quoted is inside the string, but it actually appears inside another #[...]: consider the syntactically incorrect “#[#[&e]] >= 7”, which would have to be equal to ge(#[&e], &7), so you would have a #[...] appear without quotes around it, which is why it’s a syntax error.
Now, about the free variables question. Consider the formula A := “For all n: n >= 0”. That one does not have a free variable. However, it has the subformula B := “n >= 0“, and that one does have n as a free variable—which gets bound when the subexpression is inserted into the larger one. Note that we can write A as “For all n: #[B]”. Now let F := “_ >= 0”; then B = F(‘n’), and A = “For all n: #[F(‘n’)]”. So #[F(‘n’)] splices in the formula B, which has a free variable, which then gets bound, producing A, which doesn’t have a free variable—and qualitatively the same thing happens in the stuff you quoted.
-- Was that helpful? Is there something here I should expand on, or something else that would be helpful for me to try to explain? (And thanks again for taking the time to try to figure this out.)
Thanks. So it sounds like #[...] is the inverse operation of &..., but can only be used within quotes. So in
“#[&n] >= 7” = ge(&n, &7), why do you have “#[&n]” instead of just “n”? Is that to make it clear that you’re using the numeric value of n rather than the variable n?
Also, what does ”… #[&F](& #[&m]) …” mean? From my understanding, that would get unpacked as subst(repr(F), repr(#[repr(m)])), but that is a syntax error.
So it sounds like #[...] is the inverse operation of &..., but can only be used within quotes.
No, that doesn’t make sense to me. The inverse of & would be a computable function that takes the Gödel number of a unary numeral and returns the number represented by that numeral. #[...] is syntactic sugar somewhat similar to the $NAME in e.g. Perl’s “Hello, $NAME!”. But--
So in “#[&n] >= 7” = ge(&n, &7), why do you have “#[&n]” instead of just “n”? Is that to make it clear that you’re using the numeric value of n rather than the variable n?
Well, it’s because “n >= 7” would mean an expression that contains the variable n, rather than an expression containing the unary numeral representing the numeric value of n. (“n >= 7″ = ge(‘n’, &7) is a different Gödel number than “#[&n] >= 7” = ge(&n, &7).) Being able to distinguish between such meanings was the point of introducing the explicit notation, because in my original post it was unclear what I meant and I confused myself enough that I ended up with a buggy proof. Possibly we’re at least part-way there to understanding each other, but you’re conceptualizing things differently?
Also, what does ”… #&F …” mean? From my understanding, that would get unpacked as subst(repr(F), repr(#[repr(m)])), but that is a syntax error.
No, wait, that’s completely wrong. We need to distinguish between applying repr(.) to an argument and constructing the Gödel number of an expression in which repr(.) is applied to an argument. For example, in my earlier comment, plus(x,y) was not equal to (x+y): if x and y are the Gödel numbers of two expressions, then (x+y) would simply add those Gödel numbers (which isn’t useful), whereas plus(x,y) returns the Gödel number of an expression (namely the expression adding the expressions denoted by the Gödel numbers x and y). Do you see what I mean?
Perhaps it would be good to have a common prefix for functions that construct the Gödel numbers of expressions: replace plus(.,.) and ge(.,.) from the previous post by mkPlus(.,.) and mkGe(.,.), and add the function mkRepr(e), which constructs the expression that applies repr to the expression denoted by e, and mkSubst(e1,e2), which constructs the expression that applies subst to the expressions denoted by e1 and e2. Let’s also have mkEq(.) for equality. Then, we have
(I’ll continue to write the Gödel number of a variable by putting the variable in quotes, because it doesn’t seem helpful to introduce another notation for that.) As another example, we have
So the middle “&” gets translated to mkRepr, because it is inside the quotes; but the other two &’s are just repr(.), because they are inside the splice, which means that they are not quoted.
No, that doesn’t make sense to me. The inverse of & would be a computable function that takes the Gödel number of a unary numeral and returns the number represented by that numeral. #[...] is syntactic sugar somewhat similar to the $NAME in e.g. Perl’s “Hello, $NAME!”.
But “#[&7]” = “7″, and if you replace the 7s with some other number, it’s still true, right?
“n >= 7” would mean an expression that contains the variable n, rather than an expression containing the unary numeral representing the numeric value of n.
Got it.
No, wait, that’s completely wrong. We need to distinguish between applying repr(.) to an argument and constructing the Gödel number of an expression in which repr(.) is applied to an argument. For example, in my earlier comment, plus(x,y) was not equal to (x+y): if x and y are the Gödel numbers of two expressions, then (x+y) would simply add those Gödel numbers (which isn’t useful), whereas plus(x,y) returns the Gödel number of an expression (namely the expression adding the expressions denoted by the Gödel numbers x and y). Do you see what I mean?
Oh, I see. Everything after that paragraph, I’m going to have to think about for a while. Edit: got it (I think).
But “#[&7]” = “7″, and if you replace the 7s with some other number, it’s still true, right?
Ah! This is correct, but I would conceptualize it differently, as the combination of two distinct phenomena. First, #[...] is sort of the inverse of ”...”, which makes more sense to me because both of these are kinds of syntactic sugar—we have both “#[e]” = e and “x + #[‘y’]” = “x + y”.
Second, “7” is the Gödel number of the unary numeral 7, and repr(7) also returns this Gödel number. In other words, “7“ = &7. Putting the two together: “#[&7]” = &7 = “7”.
...although the mkStuff way of writing things is ugly in one way: it means that if you want to desugar quotes inside quotes, you may need to introduce mkMkStuff functions, as in,
(Recall that ‘a’ denotes the Gödel number of the variable a; repr(‘a’) is the Gödel number of an expression that evaluates to the Gödel number of a, which is what we need in that place.)
It would be better to introduce functions call(name,arg) and pair(x,y) such that
I got lost while trying to follow this (at least in my case, you were very wrong about this being more comprehensible and intuitive than your previous post), and eventually I figured out that I didn’t even understand your notation.
Is #[stuff] just the inverse of repr? If so, why do you keep using “#[&stuff]” instead of just “stuff”? If not, what is it?
And in “For all x: If K>0, and PPT.3 |- #[&F](&x), then #[down(F(‘x’))]”, I assume that ” ‘x’ ” means something different from “&x”, “#[&x]”, or “x” because otherwise you just would have used whichever of those was appropriate. Later on, you say ” “#[down(F(‘x’))]” splices in a formula with free variable ‘x’ ”, but I’m not sure what you mean by that. ‘x’ obviously isn’t a free variable because it appears inside the quantifier “for all x: …”.
The cornerstone of all good proofs of the impossible!
Thanks for your feedback, and for trying to follow the proof! Clearly I underestimated the inferential distance when I wrote that ”...” and #[...] work just like Lisp’s backquote and comma, and then more or less left it at that :-)
Let’s try whether some examples help—let’s introduce some functions for constructing Gödel numbers explicitly, and then see what the quote/splice notation desugars to. We already know repr(n), written &n, which returns the Gödel number of the representation of n as a unary numeral. Let ge(x,y) be a function taking the Gödel numbers of two expressions, and returning the formula saying that the first expression is >= the second expression. For example,
Similarly, define plus(x,y) as taking the Gödel numbers of two expressions, and returning the Gödel number of another expression, so that
(I hope that made sense?) -- In both of these cases, the quotation on the right-hand side is actually syntactic sugar for the left-hand side.
Now, let’s look at an example of what a quoted expression with a splice desugars to.
So, here x is the Gödel number of an expression that gets inserted on the right-hand side of the >=. For example, if you define a function f(x) := “(2+2) >= #[x]”, and then apply that to the value “1+1″ = plus(&1, &1), then you get
Now, sometimes you don’t want to insert an arbitrary expression, but you have a particular value you want to insert. Perhaps you have a number n, and you want to construct an expression saying that n is at least 7. Now what you do is to use & to turn n into the Gödel number of an expression, and then splice in that expression:
Does that help with the question of what #[...] means? This comment is getting long so I’ll move on to the second question, but please ask more if it’s still unclear.
In the F(e) notation, F is the Gödel number of an expression that may contain blanks, like F = “_ < 12”, and e is the Gödel number of some expression, like e = “2+2″. Then, F(e) is the Gödel number of the expression obtained by substituting e for the blanks: in the example, F(e) = “2+2 < 12”.
Let’s stick with our example F. ‘x’ is the Gödel number of the variable x, so F(‘x’) = “x < 12”. On the other hand, &x denotes the unary representation of the current value of x, so if x=17, then F(&x) = “17 < 12“. Back to the first hand, if x=17, then you still have F(‘x’) = “x < 12”, because ‘x’ is just a fixed Gödel number, it doesn’t depend on the value of the variable x. (Just as in Python, the string literal ‘x’ has the same value no matter what the variable x is bound to.) F(x) is only useful if the current value of x is the Gödel number of an expression; if x=”1+1“, then F(x) = “1+1 < 12”. Finally, F(#[&x]) wouldn’t make sense in this place, because the #[...] notation can only appear inside a string. Well, it may look as if the place you quoted is inside the string, but it actually appears inside another #[...]: consider the syntactically incorrect “#[#[&e]] >= 7”, which would have to be equal to ge(#[&e], &7), so you would have a #[...] appear without quotes around it, which is why it’s a syntax error.
Now, about the free variables question. Consider the formula A := “For all n: n >= 0”. That one does not have a free variable. However, it has the subformula B := “n >= 0“, and that one does have n as a free variable—which gets bound when the subexpression is inserted into the larger one. Note that we can write A as “For all n: #[B]”. Now let F := “_ >= 0”; then B = F(‘n’), and A = “For all n: #[F(‘n’)]”. So #[F(‘n’)] splices in the formula B, which has a free variable, which then gets bound, producing A, which doesn’t have a free variable—and qualitatively the same thing happens in the stuff you quoted.
-- Was that helpful? Is there something here I should expand on, or something else that would be helpful for me to try to explain? (And thanks again for taking the time to try to figure this out.)
Thanks. So it sounds like #[...] is the inverse operation of &..., but can only be used within quotes. So in “#[&n] >= 7” = ge(&n, &7), why do you have “#[&n]” instead of just “n”? Is that to make it clear that you’re using the numeric value of n rather than the variable n?
Also, what does ”… #[&F](& #[&m]) …” mean? From my understanding, that would get unpacked as subst(repr(F), repr(#[repr(m)])), but that is a syntax error.
No, that doesn’t make sense to me. The inverse of & would be a computable function that takes the Gödel number of a unary numeral and returns the number represented by that numeral. #[...] is syntactic sugar somewhat similar to the $NAME in e.g. Perl’s “Hello, $NAME!”. But--
Well, it’s because “n >= 7” would mean an expression that contains the variable n, rather than an expression containing the unary numeral representing the numeric value of n. (“n >= 7″ = ge(‘n’, &7) is a different Gödel number than “#[&n] >= 7” = ge(&n, &7).) Being able to distinguish between such meanings was the point of introducing the explicit notation, because in my original post it was unclear what I meant and I confused myself enough that I ended up with a buggy proof. Possibly we’re at least part-way there to understanding each other, but you’re conceptualizing things differently?
No, wait, that’s completely wrong. We need to distinguish between applying repr(.) to an argument and constructing the Gödel number of an expression in which repr(.) is applied to an argument. For example, in my earlier comment, plus(x,y) was not equal to (x+y): if x and y are the Gödel numbers of two expressions, then (x+y) would simply add those Gödel numbers (which isn’t useful), whereas plus(x,y) returns the Gödel number of an expression (namely the expression adding the expressions denoted by the Gödel numbers x and y). Do you see what I mean?
Perhaps it would be good to have a common prefix for functions that construct the Gödel numbers of expressions: replace plus(.,.) and ge(.,.) from the previous post by mkPlus(.,.) and mkGe(.,.), and add the function mkRepr(e), which constructs the expression that applies repr to the expression denoted by e, and mkSubst(e1,e2), which constructs the expression that applies subst to the expressions denoted by e1 and e2. Let’s also have mkEq(.) for equality. Then, we have
(I’ll continue to write the Gödel number of a variable by putting the variable in quotes, because it doesn’t seem helpful to introduce another notation for that.) As another example, we have
Now, the example you quote:
So the middle “&” gets translated to mkRepr, because it is inside the quotes; but the other two &’s are just repr(.), because they are inside the splice, which means that they are not quoted.
But “#[&7]” = “7″, and if you replace the 7s with some other number, it’s still true, right?
Got it.
Oh, I see. Everything after that paragraph, I’m going to have to think about for a while. Edit: got it (I think).
Ah! This is correct, but I would conceptualize it differently, as the combination of two distinct phenomena. First, #[...] is sort of the inverse of ”...”, which makes more sense to me because both of these are kinds of syntactic sugar—we have both “#[e]” = e and “x + #[‘y’]” = “x + y”.
Second, “7” is the Gödel number of the unary numeral 7, and repr(7) also returns this Gödel number. In other words, “7“ = &7. Putting the two together: “#[&7]” = &7 = “7”.
:-) Thanks again for sticking with it!
...although the mkStuff way of writing things is ugly in one way: it means that if you want to desugar quotes inside quotes, you may need to introduce mkMkStuff functions, as in,
(Recall that ‘a’ denotes the Gödel number of the variable a; repr(‘a’) is the Gödel number of an expression that evaluates to the Gödel number of a, which is what we need in that place.)
It would be better to introduce functions call(name,arg) and pair(x,y) such that
etc. Then we can apply the desugaring recursively--
HTH more than it confuses :-/