It might be worth being explicit that ⊢ has lower precedence than the other operators (which in some sense are part of a different language). I, like maybe Gurkenglas, spent some time wondering why (⊢□A)→(□□A) wasn’t just a special case of necessitation.
I’m confused by your use of the deduction theorem. It’s only used in the forward implication argument, and seems unnecessary to me. (The linked wiki article doesn’t mention it.) More precisely, it only seems necessary to move things left-to-right across a turnstyle, because you’ve previously moved them right-to-left in a way that isn’t obviously-to-me valid.
(I mean, it’s obvious to me that if we can prove that A implies B, then assuming A lets us prove B. But it would also be obvious to me that if assuming A lets us prove B, we can prove that A implies B, yet you dedicated a theorem to allowing that. And I don’t trust things that are obvious to me to be actually “true”, let alone valid moves here.)
We can just make the whole argument without doing that and it seems fine to me? Looking at it in more depth:
(This does require that we can do logic with the things we’ve proved. E.g. if we have ⊢x and ⊢x→y, we can conclude ⊢y. I think that’s okay, but seems worth being explicit about.)
□Ψ⊢□□Ψ by internal necessitation (□Ψ→□□Ψ).
This is just doing the thing I question.
□Ψ⊢□(□Ψ→p) using box distributivity on the assumption, with A=Ψ and B=□Ψ→p.
The assumption is ⊢Ψ↔(□Ψ→p), i.e. ⊢A↔B. Weaken it and use necessitation to get ⊢□(A→B). Box distributivity is ⊢□(A→B)→(□A→□B). From those two, we can get ⊢□A→□B. Expanding again, this is ⊢□Ψ→□(□Ψ→p).
□Ψ⊢□p from 1 and 2 by box distributivity.
Box distributivity lets us go from ⊢□(□Ψ→p) to ⊢□□Ψ→□p. So using 2, we have ⊢□Ψ→(□□Ψ→□p). And internal necessitation gives us ⊢□Ψ→□□Ψ, so combining those, ⊢□Ψ→□p.
It’s true that the deduction theorem is not needed, as in the Wikipedia proof. I just like using the deduction theorem because I find it intuitive (assume A, prove B, then drop the assumption and conclude A→B) and it removes the need for lots of parentheses everywhere.
I’ll add a note about the meaning of ⊢ so folks don’t need to look it up, thanks for the feedback!
It might be worth being explicit that ⊢ has lower precedence than the other operators (which in some sense are part of a different language). I, like maybe Gurkenglas, spent some time wondering why (⊢□A)→(□□A) wasn’t just a special case of necessitation.
I’m confused by your use of the deduction theorem. It’s only used in the forward implication argument, and seems unnecessary to me. (The linked wiki article doesn’t mention it.) More precisely, it only seems necessary to move things left-to-right across a turnstyle, because you’ve previously moved them right-to-left in a way that isn’t obviously-to-me valid.
(I mean, it’s obvious to me that if we can prove that A implies B, then assuming A lets us prove B. But it would also be obvious to me that if assuming A lets us prove B, we can prove that A implies B, yet you dedicated a theorem to allowing that. And I don’t trust things that are obvious to me to be actually “true”, let alone valid moves here.)
We can just make the whole argument without doing that and it seems fine to me? Looking at it in more depth:
(This does require that we can do logic with the things we’ve proved. E.g. if we have ⊢x and ⊢x→y, we can conclude ⊢y. I think that’s okay, but seems worth being explicit about.)
This is just doing the thing I question.
The assumption is ⊢Ψ↔(□Ψ→p), i.e. ⊢A↔B. Weaken it and use necessitation to get ⊢□(A→B). Box distributivity is ⊢□(A→B)→(□A→□B). From those two, we can get ⊢□A→□B. Expanding again, this is ⊢□Ψ→□(□Ψ→p).
Box distributivity lets us go from ⊢□(□Ψ→p) to ⊢□□Ψ→□p. So using 2, we have ⊢□Ψ→(□□Ψ→□p). And internal necessitation gives us ⊢□Ψ→□□Ψ, so combining those, ⊢□Ψ→□p.
No need for this, we already finished.
It’s true that the deduction theorem is not needed, as in the Wikipedia proof. I just like using the deduction theorem because I find it intuitive (assume A, prove B, then drop the assumption and conclude A→B) and it removes the need for lots of parentheses everywhere.
I’ll add a note about the meaning of ⊢ so folks don’t need to look it up, thanks for the feedback!
Thanks, that makes sense. And the added explanation helps a lot, I can see the argument for going from ⊢A→B to A⊢B now:
PA proves A→B;
So PA + A certainly proves A→B, since it can prove everything PA can;
Also, PA + A proves A;
So we have A⊢A∧(¬A∨B);
Which in turn gives us A⊢B.