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).
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).