Editing Natural deduction (section)

=== Gentzen-style definition ===
A syntax definition can also be given using {{section link||Gentzen's tree notation}}, by writing well-formed formulas below the inference line and any schematic variables used by those formulas above it.{{sfn|Ayala-Rincón|de Moura|2017|pages=2,20}} For instance, the equivalent of rules 3 and 4, from Bostock's definition above, is written as follows:

:<math>\frac{\varphi}{(\neg \varphi)} \quad \frac{\varphi \quad \psi}{(\varphi \lor \psi)} \quad \frac{\varphi \quad \psi}{(\varphi \land \psi)} \quad \frac{\varphi \quad \psi}{(\varphi \rightarrow \psi)} \quad \frac{\varphi \quad \psi}{(\varphi \leftrightarrow \psi)}</math>.

A different notational convention sees the language's syntax as a [[categorial grammar]] with the single category "formula", denoted by the symbol <math>\mathcal{F}</math>. So any elements of the syntax are introduced by categorizations, for which the notation is <math>\varphi : \mathcal{F}</math>, meaning "<math>\varphi</math> is an expression for an object in the category <math>\mathcal{F}</math>."{{sfn|von Plato|2013|pages=12–13}} The sentence-letters, then, are introduced by categorizations such as <math>P : \mathcal{F}</math>, <math>Q : \mathcal{F}</math>, <math>R : \mathcal{F}</math>, and so on;{{sfn|von Plato|2013|pages=12–13}} the connectives, in turn, are defined by statements similar to the above, but using categorization notation, as seen below:
{| class="wikitable"
|+ '''Connectives defined through a categorial grammar{{sfn|von Plato|2013|pages=12–13}}'''
|-
! style="text-align: center;" | '''Conjunction (&)'''
! style="text-align: center;" | '''Disjunction (∨)'''
! style="text-align: center;" | '''Implication (→)'''
! style="text-align: center;" | '''Negation (¬)'''
|-
| <math>\frac{A : \mathcal{F} \quad B : \mathcal{F}}{\&(A)(B) : \mathcal{F}}</math>
| <math>\frac{A : \mathcal{F} \quad B : \mathcal{F}}{\vee(A)(B) : \mathcal{F}}</math>
| <math>\frac{A : \mathcal{F} \quad B : \mathcal{F}}{\supset(A)(B) : \mathcal{F}}</math>
| <math>\frac{A : \mathcal{F}}{\neg(A) : \mathcal{F}}</math>
|}
In the rest of this article, the <math>\varphi : \mathcal{F}</math> categorization notation will be used for any Gentzen-notation statements defining the language's grammar; any other statements in Gentzen notation will be inferences, asserting that a sequent follows rather than that an expression is a well-formed formula.