Gurkenglas comments on Open technical problem: A Quinean proof of Löb’s theorem, for an easier cartoon guide

Gurkenglas 27 Nov 2022 0:15 UTC
LW: 9 AF: 7
7
AF
Similarly:
```
löb = □ (□ A → A) → □ A
□löb = □ (□ (□ A → A) → □ A)
□löb -> löb:
  löb premises □ (□ A → A).
  By internal necessitation, □ (□ (□ A → A)).
  By □löb, □ (□ A).
  By löb's premise, □ A.
```
- Andrew_Critch 27 Nov 2022 2:33 UTC
  LW: 2 AF: 1
  0
  AF Parent
  Noice :)
  - Gurkenglas 28 Nov 2022 2:07 UTC
    2 points
    0
    Parent
    When disambiguating as far as possible, löb becomes □(□B → A) → □A, but □löb becomes □(□(□B → A) → □B). Perhaps Ψ has a universal property related to this?