Editing Natural deduction (section)

==Notation==
Here is a table with the most common notational variants for [[Logical connective|logical connectives]].
{| class="wikitable"
|+ Notational variants of the connectives{{sfn|von Plato|2013|p=9}}{{sfn|Weisstein}}
|-
! Connective
! Symbol
|-
| [[Logical conjunction|AND]]
| <math>A \land B</math>, <math>A \cdot B</math>, <math>AB</math>, <math>A \& B</math>, <math>A \&\& B</math>
|-
| [[Logical biconditional|equivalent]]
| <math>A \equiv B</math>, <math>A \Leftrightarrow B</math>, <math>A \leftrightharpoons B</math>
|-
| [[Material conditional|implies]]
| <math>A \Rightarrow B</math>, <math>A \supset B</math>, <math>A \rightarrow B</math>
|-
| [[Sheffer stroke|NAND]]
| <math>A \overline{\land} B</math>, <math>A \mid B</math>, <math>\overline{A \cdot B}</math>
|-
| nonequivalent
| <math>A \not\equiv B</math>, <math>A \not\Leftrightarrow B</math>, <math>A \nleftrightarrow B</math>
|-
| [[Logical NOR|NOR]]
| <math>A \overline{\lor} B</math>, <math>A \downarrow B</math>, <math>\overline{A+B}</math>
|-
| [[Negation|NOT]]
| <math>\neg A</math>, <math>-A</math>, <math>\overline{A}</math>, <math>\sim A</math>
|-
| [[Logical disjunction|OR]]
| <math>A \lor B</math>, <math>A + B</math>, <math>A \mid B</math>, <math>A \parallel B</math>
|-
| [[XNOR gate|XNOR]]
| <math>A</math> XNOR <math>B</math>
|-
| [[Exclusive or|XOR]]
| <math>A \underline{\lor} B</math>, <math>A \oplus B</math>
|}

===Gentzen's tree notation===

[[Gerhard Gentzen|Gentzen]], who invented natural deduction, had his own notation style for arguments. This will be exemplified by a simple argument below. Let's say we have a simple example argument in [[Propositional calculus|propositional logic]], such as, "if it's raining then it's cloudly; it is raining; therefore it's cloudy". (This is in [[modus ponens]].) Representing this as a list of propositions, as is common, we would have:

:<math>1) ~ P \to Q</math>
:<math>2) ~ P</math>
:<math>\therefore ~ Q</math>

In Gentzen's notation,{{sfn|Pelletier|Hazen|2024}} this would be written like this:

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

The premises are shown above a line, called the '''inference line''',{{sfn|von Plato|2013|pp=9,32,121}}{{sfn|Sutcliffe}} separated by a '''comma''', which indicates ''combination'' of premises.{{sfn|Restall|2018}} The conclusion is written below the inference line.{{sfn|von Plato|2013|pp=9,32,121}} The inference line represents ''syntactic consequence'',{{sfn|von Plato|2013|pp=9,32,121}} sometimes called ''deductive consequence'',{{sfn|Magnus|Button|Trueman|Zach|2023|loc=CHAPTER 20, Proof-theoretic concepts|p=142}}{{sfn|Paseau|Leek}} which is also symbolized with ⊢.{{sfn|Paseau|Leek}} So the above can also be written in one line as <math>P \to Q, P \vdash Q</math>. (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.){{sfn|Restall|2018}}

Syntactic consequence is contrasted with ''semantic consequence'',{{sfn|Paseau|Pregel|2023}} which is symbolized with ⊧.{{sfn|Magnus|Button|Trueman|Zach|2023|loc=12.5 The double turnstile|p=82}}{{sfn|Paseau|Leek}} In this case, the conclusion follows ''syntactically'' because natural deduction is a [[Propositional_calculus#Syntactic_proof_systems|syntactic proof system]], which assumes [[inference rules]] [[Postulate|as primitives]].

Gentzen's style will be used in much of this article. Gentzen's discharging annotations used to internalise hypothetical judgments can be avoided by representing proofs as a tree of [[sequent]]s ''Γ ⊢A'' instead of a tree of judgments that A (is true).

=== Suppes–Lemmon notation ===
Many textbooks use [[Suppes–Lemmon notation]],{{sfn|Pelletier|Hazen|2024}} so this article will also give that – although as of now, this is only included for [[Propositional calculus|propositional logic]], and the rest of the coverage is given only in Gentzen style. A '''proof''', laid out in accordance with the [[Suppes–Lemmon notation]] style, is a sequence of lines containing sentences,{{sfn|Allen|Hand|2022}} where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence.{{sfn|Allen|Hand|2022}} Each '''line of proof''' is made up of a '''sentence of proof''', together with its '''annotation''', its '''assumption set''', and the current '''line number'''.{{sfn|Allen|Hand|2022}} The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers.{{sfn|Allen|Hand|2022}} The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence.{{sfn|Allen|Hand|2022}} Here's an example proof:
{| class="wikitable" style="margin:auto;"
|+Suppes–Lemmon style proof (first example)
!Assumption set
!Line number
!Sentence of proof
!Annotation
|-
|{{EquationRef|1}}
|{{EquationRef|1}}
|<math>P \to Q</math>
|A
|-
|{{EquationRef|2}}
|{{EquationRef|2}}
|<math>-Q</math>
|A
|-
|{{EquationRef|3}}
|{{EquationRef|3}}
|<math>P</math>
|A
|-
|{{EquationRef|1}}, {{EquationRef|3}}
|{{EquationRef|4}}
|<math>Q</math>
|{{EquationRef|1}}, {{EquationRef|3}} →E
|-
|{{EquationRef|1}}, {{EquationRef|2}}
|{{EquationRef|5}}
|<math>-P</math>
|{{EquationRef|2}}, {{EquationRef|4}} RAA
|}
This proof will become clearer when the inference rules and their appropriate annotations are specified – see {{section link||Propositional inference rules (Suppes–Lemmon style)}}.