Editing Natural deduction (section)

==Propositional language syntax==
{{Main article|Propositional calculus#Syntax}}This section defines the [[formal syntax]] for a [[Propositional calculus#Language|propositional logic language]], contrasting the common ways of doing so with a Gentzen-style way of doing so.

=== Common definition styles ===
In [[classical logic|classical]] [[propositional calculus]] the [[formal language]] <math>\mathcal{L}</math> is usually defined (here: by [[recursive definition|recursion]]) as follows:{{sfn|Allen|Hand|2022|p=12}}

# Each [[propositional variable]] is a [[Well-formed formula|formula]].
# "<math>\bot</math>" is a formula.
# If <math>\varphi</math> and <math>\psi</math> are formulae, so are <math>(\neg\phi)</math>, <math>(\varphi \land \psi)</math>, <math>(\varphi \lor \psi)</math>, <math>(\varphi \to \psi)</math>, <math>(\varphi \leftrightarrow \psi)</math>.
# Nothing else is a formula.

[[Negation]] (<math>\neg</math>) is taken as a primitive [[logical connective]], meaning it is assumed as a basic operation and not defined in terms of other connectives. In some logical systems, especially [[minimal logic| minimal]], [[intuitionistic logic|intuitionistic]], or [[Hilbert system]]s, negation is defined as implication to [[False (logic)#False, negation and contradiction|falsity]]
:<math>\neg \phi \; \overset{\text{def}}{=} \; \phi \to \bot</math>,
where <math>\bot</math> (falsum) represents a contradiction or absolute falsehood.{{sfn|Prawitz|1965}}{{sfn|von Plato|2013|p=18}}{{sfn|Van Dalen|2013}} The language (here: in [[BNF grammar|BNF]]){{sfn|Hansson|Hendricks|2018|p=38}}{{sfn|Ayala-Rincón|de Moura|2017|pages=2,20}} is then
:<math>\phi ::= a_1, a_2, \ldots \mid \bot \mid (\phi \land\phi) \mid (\phi \lor \phi) \mid (\phi \to\phi) \mid (\phi \leftrightarrow \phi)</math>

Some authors, such as [[David Bostock (philosopher)|Bostock]], use <math>\bot</math> and <math>\top</math>, and also define <math>\neg</math> as primitives.{{sfn|Bostock|1997|p=21}}<ref>This is required in [[paraconsistent logic]]s that do not treat <math>\neg</math> and <math>(\phi \to \bot)</math> as equivalents.</ref>

This article focuses on the first approach.

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