Editing Propositional calculus (section)

=== Gentzen notation ===
If we assume that the validity of [[modus ponens]] has been accepted as an [[axiom]], then the same {{section link||Example argument}} can also be depicted like this:

:<math>\frac{P \to Q, P}{Q}</math>

This method of displaying it is [[Gerhard Gentzen|Gentzen]]'s notation for [[natural deduction]] and [[sequent calculus]].<ref name=":40"/> The premises are shown above a line, called the '''inference line''',<ref name=":3" /> separated by a '''comma''', which indicates ''combination'' of premises.<ref name=":34"/> The conclusion is written below the inference line.<ref name=":3" /> The inference line represents ''syntactic consequence'',<ref name=":3" /> sometimes called ''deductive consequence'',<ref name=":7"/>> which is also symbolized with ⊢.<ref name=":6"/><ref name=":7" /> So the above can also be written in one line as <math>P \to Q, P \vdash Q</math>.{{refn|group=lower-alpha|The turnstile, for syntactic consequence, is of lower [[Order of operations|precedence]] than the comma, which represents premise combination, which in turn is of lower precedence than the arrow, used for material implication; so no parentheses are needed to interpret this formula.<ref name=":34" />}}

Syntactic consequence is contrasted with ''semantic consequence'',<ref name="ms16"/> which is symbolized with ⊧.<ref name=":6" /><ref name=":7" /> In this case, the conclusion follows ''syntactically'' because the [[natural deduction]] [[Rule of inference|inference rule]] of [[modus ponens]] has been assumed. For more on inference rules, see the sections on proof systems below.