this suggests that you’re going to be hard-pressed to do any self-reference without routing through the nomal machinery of löb’s theorem, in the same way that it’s hard to do recursion in the lambda calculus without routing through the Y combinator
If by “the normal machinery”, you mean a clever application of the diagonal lemma, then I agree. But I think we can get away with not having the self-referential sentence, by using the same y-combinator-like diagonal-lemma machinery to make a proof that refers to itself (instead of a proof about sentences that refer to themselves) and checks its own validity. I think I if or someone else produces a valid proof like that, skeptics of its value (of which you might be one; I’m not sure) will look at it and say “That was harder and less efficient than the usual way of proving Löb using the self-referential sentence Ψ and no self-validation”. I predict I’ll agree with that, and still find the new proof to be of additional intellectual value, for the following reason:
Human documents tend to refer to the themselves a lot, like bylaws.
Human sentences, on the other hand, rarely refer to themselves. (This sentence is an exception, but there aren’t a lot of naturally occurring examples.)
Therefore, a proof of Löb whose main use of self-references involves the entire proof referring to itself, rather than a sing sentence referring to itself, will be more intuitive to humans (such as lawyers) who are used to thinking about self-referential documents.
The skeptic response to that will be to say that those peoples’ intuitions are the wrong way to think about y-combinator manipulation, and to that I’ll be like “Maybe, but I’m not super convinced their perspective is wrong, and in any case I don’t mind meeting them where they’re at, using a proof that they find more intuitive.”.
Summary: I’m pretty confident the proof will be valuable, even though I agree it will have to use much of the same machinery as the usual proof, plus some extra machinery for helping the proof to self-validate, as long as the proof doesn’t use sentences that are basically only about their own meaning (the way the sentence Ψ is basically only about its own relationship to the sentence C, which is weird).
This sentence is an exception, but there aren’t a lot of naturally occurring examples.
No strong claim either way, but as a datapoint I do somewhat often use the phrase “I hereby invite you to <event>” or “I hereby <request> something of you” to help move from ‘describing the world’ to ‘issuing an invitation/command/etc’.
True! “Hereby” covers a solid contingent of self-referential sentences. I wonder if there’s a “hereby” construction that would make the self-referential sentence Ψ (from the Wikipedia poof) more common-sense-meaningful to, say, lawyers.
which self-referential sentence are you trying to avoid?
it keeps sounding to me like you’re saying “i want a λ-calculus combinator that produces the fixpoint of a given function f, but i don’t want to use the Y combinator”.
do you deny the alleged analogy between the normal proof of löb and the Y combinator? (hypothesis: maybe you see that the diagonal lemma is just the type-level Y combinator, but have not yet noticed that löb’s theorem is the corresponding term-level Y combinator?)
if you follow the analogy, can you tell me what λ-term should come out when i put in f, and how it’s better than (λ s. f (s s)) (λ s. f (s s))?
or (still assuming you follow the analogy): what sort of λ-term representing the fixpoint of f would constitute “referring to itself (instead of being a term about types that refer to themselves)”? in what sense is the term (λ s. f (s s)) (λ s. f (s s)) failing to “refer to itself”, and what property are you hoping for instead?
(in case it helps with communication: when i try myself to answer these questions while staring at the OP, my best guess is that you’re asking “instead of the Y combinator, can we get a combinator that goes like f ↦ f ????”, and the two obvious ways to fill in the blanks are f ↦ f (Y f) and f ↦ f (f (f (.... i discussed why both of those are troublesome here, but am open to the possibility that i have not successfully understood what sort of fixpoint combinator you desire.)
(ETA: also, ftr, in the proof-sketch of löb’s theorem that i gave above, the term "g "g"" occurs as a subterm if you do enough substitution, and it refers to the whole proof of löb’s theorem. just like how, in the version of the Y combinator given above, the term g g occurs as a subterm if you do enough β-reduction, and it refers to the whole fixpoint. which i note b/c it seems to me that you might have misunderstood a separate point about where the OP struggles as implying that the normal proof isn’t self-referring.)
((the OP is gonna struggle insofar as it does the analog of asking for a λ-term x that is literally syntactically identical to f x, for which the only solution is f (f (f (... which is problematic. but a λ-term y that β-reduces pretty quickly to f y is easy, and it’s what the standard constuction produces.))
At this point I’m more interested in hashing out approaches that might actually conform to the motivation in the OP. Perhaps I’ll come back to this discussion with you after I’ve spent a lot more time in a mode of searching for a positive result that fits with my motivation here. Meanwhile, thanks for thinking this over for a bit.
well, in your search for that positive result, i recommend spending some time searching for a critch!simplified alternative to the Y combinator :-p.
not every method of attaining self-reference in the λ-calculus will port over to logic (b/c in the logical setting lots of things need to be quoted), but the quotation sure isn’t making the problem any easier. a solution to the OP would yield a novel self-reference combinator in the λ-calculus, and the latter might be easier to find (b/c you don’t need to juggle quotes).
if you can lay bare the self-referential property that you’re hoping for in the easier setting of λ-calculus, then perhaps others will have an easier time understanding what you want and helping out (and/or you’ll have an easier time noticing why your desires are unsatisfiable).
(and if it’s still not clear that löb’s theorem is tightly connected to the Y combinator, such that any solution to the OP would immediately yield a critch!simplified self-reference combinator in the λ-calculus, then I recommend spending a little time studying the connection between the Y combinator, löb’s theorem, and lawvere’s fixpoint theorem.)
If by “the normal machinery”, you mean a clever application of the diagonal lemma, then I agree. But I think we can get away with not having the self-referential sentence, by using the same y-combinator-like diagonal-lemma machinery to make a proof that refers to itself (instead of a proof about sentences that refer to themselves) and checks its own validity. I think I if or someone else produces a valid proof like that, skeptics of its value (of which you might be one; I’m not sure) will look at it and say “That was harder and less efficient than the usual way of proving Löb using the self-referential sentence Ψ and no self-validation”. I predict I’ll agree with that, and still find the new proof to be of additional intellectual value, for the following reason:
Human documents tend to refer to the themselves a lot, like bylaws.
Human sentences, on the other hand, rarely refer to themselves. (This sentence is an exception, but there aren’t a lot of naturally occurring examples.)
Therefore, a proof of Löb whose main use of self-references involves the entire proof referring to itself, rather than a sing sentence referring to itself, will be more intuitive to humans (such as lawyers) who are used to thinking about self-referential documents.
The skeptic response to that will be to say that those peoples’ intuitions are the wrong way to think about y-combinator manipulation, and to that I’ll be like “Maybe, but I’m not super convinced their perspective is wrong, and in any case I don’t mind meeting them where they’re at, using a proof that they find more intuitive.”.
Summary: I’m pretty confident the proof will be valuable, even though I agree it will have to use much of the same machinery as the usual proof, plus some extra machinery for helping the proof to self-validate, as long as the proof doesn’t use sentences that are basically only about their own meaning (the way the sentence Ψ is basically only about its own relationship to the sentence C, which is weird).
No strong claim either way, but as a datapoint I do somewhat often use the phrase “I hereby invite you to <event>” or “I hereby <request> something of you” to help move from ‘describing the world’ to ‘issuing an invitation/command/etc’.
True! “Hereby” covers a solid contingent of self-referential sentences. I wonder if there’s a “hereby” construction that would make the self-referential sentence Ψ (from the Wikipedia poof) more common-sense-meaningful to, say, lawyers.
which self-referential sentence are you trying to avoid?
it keeps sounding to me like you’re saying “i want a λ-calculus combinator that produces the fixpoint of a given function f, but i don’t want to use the Y combinator”.
do you deny the alleged analogy between the normal proof of löb and the Y combinator? (hypothesis: maybe you see that the diagonal lemma is just the type-level Y combinator, but have not yet noticed that löb’s theorem is the corresponding term-level Y combinator?)
if you follow the analogy, can you tell me what λ-term should come out when i put in
f, and how it’s better than(λ s. f (s s)) (λ s. f (s s))?or (still assuming you follow the analogy): what sort of λ-term representing the fixpoint of f would constitute “referring to itself (instead of being a term about types that refer to themselves)”? in what sense is the term
(λ s. f (s s)) (λ s. f (s s))failing to “refer to itself”, and what property are you hoping for instead?(in case it helps with communication: when i try myself to answer these questions while staring at the OP, my best guess is that you’re asking “instead of the Y combinator, can we get a combinator that goes like
f ↦ f ????”, and the two obvious ways to fill in the blanks aref ↦ f (Y f)andf ↦ f (f (f (.... i discussed why both of those are troublesome here, but am open to the possibility that i have not successfully understood what sort of fixpoint combinator you desire.)(ETA: also, ftr, in the proof-sketch of löb’s theorem that i gave above, the term
"g "g""occurs as a subterm if you do enough substitution, and it refers to the whole proof of löb’s theorem. just like how, in the version of the Y combinator given above, the termg goccurs as a subterm if you do enough β-reduction, and it refers to the whole fixpoint. which i note b/c it seems to me that you might have misunderstood a separate point about where the OP struggles as implying that the normal proof isn’t self-referring.)((the OP is gonna struggle insofar as it does the analog of asking for a λ-term
xthat is literally syntactically identical tof x, for which the only solution isf (f (f (...which is problematic. but a λ-termythat β-reduces pretty quickly tof yis easy, and it’s what the standard constuction produces.))At this point I’m more interested in hashing out approaches that might actually conform to the motivation in the OP. Perhaps I’ll come back to this discussion with you after I’ve spent a lot more time in a mode of searching for a positive result that fits with my motivation here. Meanwhile, thanks for thinking this over for a bit.
well, in your search for that positive result, i recommend spending some time searching for a critch!simplified alternative to the Y combinator :-p.
not every method of attaining self-reference in the λ-calculus will port over to logic (b/c in the logical setting lots of things need to be quoted), but the quotation sure isn’t making the problem any easier. a solution to the OP would yield a novel self-reference combinator in the λ-calculus, and the latter might be easier to find (b/c you don’t need to juggle quotes).
if you can lay bare the self-referential property that you’re hoping for in the easier setting of λ-calculus, then perhaps others will have an easier time understanding what you want and helping out (and/or you’ll have an easier time noticing why your desires are unsatisfiable).
(and if it’s still not clear that löb’s theorem is tightly connected to the Y combinator, such that any solution to the OP would immediately yield a critch!simplified self-reference combinator in the λ-calculus, then I recommend spending a little time studying the connection between the Y combinator, löb’s theorem, and lawvere’s fixpoint theorem.)