It seems important to clarify the difference between From ⊢A, conclude ⊢□A and ⊢□A→□□A. I don’t feel like I get why we don’t just set conclude := → and ⊢:=□.
Well, A→B is just short for ¬A∨B, i.e., “(not A) or B”. By contrast, A⊢B means that there exists a sequence of (very mechanical) applications of modus ponens, starting from the axioms of Peano Arithmetic (PA) with A appended, ending in B. We tried hard to make the rules of ⊢ so that it would agree with → in a lot of cases (i.e., we tried to design ⊢ to make the deduction theorem true), but it took a lot of work in the design of Peano Arithmetic and can’t be taken for granted.
For instance, consider the statement ¬□(1=0). If you believe Peano Arithmetic is consistent, then you believe that ¬□(1=0), and therefore you also believe that □(1=0)→(2=3). But PA cannot prove that ¬□(1=0) (by Gödel’s Theorem, or Löb’s theorem with p=(1=0)), so we don’t have ⊢□(1=0)→(2=3).
⊢ already is to □ as □ is to quoted □. If we redo the post one □ further in, we never need external necessitation. Not sure if that answers your question.
It seems important to clarify the difference between
From ⊢A, conclude ⊢□Aand⊢□A→□□A. I don’t feel like I get why we don’t just setconclude := →and⊢:=□.Well, A→B is just short for ¬A∨B, i.e., “(not A) or B”. By contrast, A⊢B means that there exists a sequence of (very mechanical) applications of modus ponens, starting from the axioms of Peano Arithmetic (PA) with A appended, ending in B. We tried hard to make the rules of ⊢ so that it would agree with → in a lot of cases (i.e., we tried to design ⊢ to make the deduction theorem true), but it took a lot of work in the design of Peano Arithmetic and can’t be taken for granted.
For instance, consider the statement ¬□(1=0). If you believe Peano Arithmetic is consistent, then you believe that ¬□(1=0), and therefore you also believe that □(1=0)→(2=3). But PA cannot prove that ¬□(1=0) (by Gödel’s Theorem, or Löb’s theorem with p=(1=0)), so we don’t have ⊢□(1=0)→(2=3).
To check, are you reading the second as (⊢□A)→(□□A)? It’s meant to be ⊢(□A→□□A).
Nah.
How would the semantics for that work out?
⊢ already is to □ as □ is to quoted □. If we redo the post one □ further in, we never need external necessitation. Not sure if that answers your question.