User:Lord Farin/Archive/Natural Deduction Axioms
General note
The below page is a copy of the revision 96983 of Definition:Natural Deduction, accessible here.
Definition
Natural deduction is a proof system for propositional logic.
As such, it consists of certain axioms, which together constitute a collection of theorems.
This can be specified as follows.
 |
Work In Progress: The inevitable subpages (discuss) You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it. When this has been done, the template should be removed from the code. |
Notation
To indicate that a collection of WFFs $P$, the pool of assumptions, entails a particular WFF $p$, the conclusion, we agree to write a sequent:
- $P \vdash p$
To make exposition more natural, we also agree to omit the brackets of explicit set definition and use commas in a suggestive way, so that:
- $p, q \vdash p \land q$
- $P, Q \vdash p \land q$
- $P, p \vdash q$
are used instead of the formally more correct:
- $\left\{{p, q}\right\} \vdash p \land q$
- $P \cup Q \vdash p \land q$
- $P \cup \left\{{p}\right\} \vdash q$
Furthermore, in the last expression it is implicitly understood that $p \notin P$.
The $\Large\leadsto$ symbol indicates that given the sequent(s) on the left-hand side, the sequent on the right-hand side may be inferred.
Axioms
Natural deduction has the following twelve axioms, explained in more detail on their own pages:
| \(\text {(\mathrm{ND}:\mathrm A)}: \quad\) | \(\ds \) | \(\) | \(\ds q \vdash q\) | Rule of Assumption | ||||||||||
| \(\text {(\mathrm{ND}:\lor \mathcal I_1)}: \quad\) | \(\ds P \vdash p\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash p \lor q\) | Rule of Addition | ||||||||||
| \(\text {(\mathrm{ND}:\lor \mathcal I_2)}: \quad\) | \(\ds P \vdash q\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash p \lor q\) | Rule of Addition | ||||||||||
| \(\text {(\mathrm{ND}:\lor \mathcal E)}: \quad\) | \(\ds \left.{ \begin{align} P &\vdash p \lor q \\ Q, p &\vdash r \\ R, q &\vdash r \end{align} }\right\}\) | \(\, \Large\leadsto \,\) | \(\ds P, Q, R \vdash r\) | Proof by Cases | ||||||||||
| \(\text {(\mathrm{ND}:\land \mathcal I)}: \quad\) | \(\ds \left.{ \begin{align} P &\vdash p \\ Q &\vdash q \end{align} }\right\}\) | \(\, \Large\leadsto \,\) | \(\ds P, Q \vdash p \land q\) | Rule of Conjunction | ||||||||||
| \(\text {(\mathrm{ND}:\land \mathcal E_1)}: \quad\) | \(\ds P \vdash p \land q\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash p\) | Rule of Simplification | ||||||||||
| \(\text {(\mathrm{ND}:\land \mathcal E_2)}: \quad\) | \(\ds P \vdash p \land q\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash q\) | Rule of Simplification | ||||||||||
| \(\text {(\mathrm{ND}:\implies \mathcal I)}: \quad\) | \(\ds P, p \vdash q\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash p \implies q\) | Rule of Implication | ||||||||||
| \(\text {(\mathrm{ND}:\implies \mathcal E)}: \quad\) | \(\ds \left.{ \begin{align} P &\vdash p \implies q \\ Q &\vdash p \end{align} }\right\}\) | \(\, \Large\leadsto \,\) | \(\ds P, Q \vdash q\) | Modus Ponendo Ponens | ||||||||||
| \(\text {(\mathrm{ND}:\neg \mathcal I)}: \quad\) | \(\ds P, p \vdash \bot\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash \neg p\) | Proof by Contradiction | ||||||||||
| \(\text {(\mathrm{ND}:\neg \mathcal E)}: \quad\) | \(\ds \left.{ \begin{align} P &\vdash p \\ Q &\vdash \neg p \end{align} }\right\}\) | \(\, \Large\leadsto \,\) | \(\ds P, Q \vdash \bot\) | Principle of Non-Contradiction | ||||||||||
| \(\text {(\mathrm{ND}:\bot \mathcal E)}: \quad\) | \(\ds P \vdash \bot\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash p\) | Rule of Explosion |
extend background; this page may become a disambig if many similar systems are covered later on. Transclusion would make it too long to read
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information.
To discuss it in more detail, feel free to use the talk page.
If you are able to do this, then when you have done so you can remove this instance of {{Expand}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
Theorems
The theorems of natural deduction are those WFFs $p$ allowing a sequent $\vdash p$, i.e., that may be derived with an empty pool of assumptions.
Proofs
Although it is satisfying to find a (formal) proof of a theorem using the above rules, it is advisable to cast such a proof in a standard framework.
On ProofWiki, the framework chosen is that of a tableau proof, which most easily lends itself for a MediaWiki architecture.
However, many other notations exist and are used by various authors.
mention boolean interpretations via soundness/completeness; this is really after the fact, though
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information.
To discuss it in more detail, feel free to use the talk page.
If you are able to do this, then when you have done so you can remove this instance of {{Expand}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
Also see
There are many other proof systems for propositional logic, see here.
Sources
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems: $\S 1.2, \ \S 1.2.3$