2.5: Natural Deduction — Read

From LibreTexts, under CC BY, as the source states it; its equations are written in TeX, which the PDF shows typeset. This page at LibreTexts.

2.5.1: Rules and Derivations
Natural deduction proofs begin with assumptions. Inference rules are then applied. Assumptions are “discharged” by the \(\lnot\text{Intro}\), \({\rightarrow}\text{Intro}\), \(\lor\text{Elim}\) and \(\exists\text{Elim}\) inference rules.
2.5.2: Propositional Rules
Rules for ∧, ∨, →, ¬, and ⊥
2.5.3: Quantifier Rules
Rules for ∀ and ∃
2.5.4: Derivations
Each derivation either is an assumption on its own, or consists of one, two, or three derivations followed by a correct inference.
2.5.5: Examples of Derivations
Derivations of the sentences \((A \land B) \rightarrow A\) and \((\lnot A \lor B) \rightarrow (A \rightarrow B)\), and an example of the \(\bot_C\) rule
2.5.6: Derivations with Quantifiers
When dealing with quantifiers, we have to make sure not to violate the eigenvariable condition, and sometimes this requires us to play around with the order of carrying out certain inferences.
2.5.7: Proof-Theoretic Notions
Just as we’ve defined a number of important semantic notions (validity, entailment, satisfiability), we now define corresponding proof-theoretic notions.
2.5.8: Derivability and Consistency
We will now establish a number of properties of the derivability relation.
2.5.9: Derivability and the Propositional Connectives
2.5.10: Derivability and the Quantifiers
2.5.11: Soundness
A derivation system, such as natural deduction, is sound if it cannot derive things that do not actually follow.
2.5.12: Derivations with Identity predicate
Derivations with identity predicate require additional inference rules.
2.5.13: Soundness with Identity predicate
Natural deduction with rules for = is sound.
2.5.14: Summary

This page titled 2.5: Natural Deduction was last modified on Sun, 12 Sep 2021 15:29:32 GMT and is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .

Contents

Text