From my point of view, → is a logic operator, which is defined by a truth table.
E.g. In propositional logic, an entailment operator (→) has a truth table of:web
| p | q | p→q |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | T |
| F | F | T |
You can definately define your own deduction logic under which T→T is F. That’s always fine.svg
⊢ is an assertion. It IS NOT necessarily correct and a specific deduction model must be given to make this assertion.
E.g. Sequent A, B ⊢ C, D means that under current deduction model, if both A and B are true, then either C or D is true. This assertion may be correct.
And under natural deduction, A ⊢ B and ⊢ A→B are the same.this
⊨ is a semantic entailment symbol used to check the relationship among certain variables under every logic model. It’s more like a universal version of ⊢, and it IS NOT necessarily correct as well.
E.g. I’ve just had my meal ⊨ Something just traveled to my stomach through my throat
This semantic entailment isn’t necessarily correct, for there might be some creature using other holes for eating instead of the one we called mouth.xml