I was under the impression that the only reason we use the syntax (A → B) in classical logic is that it mimics a rule of inference, and including the symbol makes it more intuitive (A ∧ (A → B) → B vs A ∧ (¬A ∨ B) → B). Given that there no longer is a modus ponens for → to refer to semantically, why bother using it as a symbol at all instead of restricting LP to the ¬A ∨ B syntax?
I was under the impression that the only reason we use the syntax (A → B) in classical logic is that it mimics a rule of inference, and including the symbol makes it more intuitive (A ∧ (A → B) → B vs A ∧ (¬A ∨ B) → B). Given that there no longer is a modus ponens for → to refer to semantically, why bother using it as a symbol at all instead of restricting LP to the ¬A ∨ B syntax?