diff --git a/Logic/General_concepts/Logical_equivalence.md b/Logic/General_concepts/Logical_equivalence.md index 7e70262..52bd848 100644 --- a/Logic/General_concepts/Logical_equivalence.md +++ b/Logic/General_concepts/Logical_equivalence.md @@ -17,7 +17,7 @@ Q: The pavement is not wet unless it is raining. ### Formal expression $$ -(P \rightarrow Q) \Leftrightarrow (\lnot P \lor Q) +(P \rightarrow Q) \longleftrightarrow (\lnot P \lor Q) $$ ### Truth-tables @@ -36,5 +36,3 @@ $$ Note that the property of equivalence stated in terms of derivablity above is identical to the derivation rule for the [material biconditional](/Logic/Proofs/Biconditional_Introduction.md): ![bi-intro.png](/img/bi-intro.png) - -//TODO: Add demonstration of this by deriving two equivalents from one of DeMorgan's Laws diff --git a/Logic/Laws_and_theorems.md/Corresponding_material_and_biconditional.md b/Logic/Laws_and_theorems.md/Corresponding_material_and_biconditional.md index b309db1..e6d79b6 100644 --- a/Logic/Laws_and_theorems.md/Corresponding_material_and_biconditional.md +++ b/Logic/Laws_and_theorems.md/Corresponding_material_and_biconditional.md @@ -36,4 +36,4 @@ We see above that the main connective, the material conditional returns true for We can use the corresponding material biconditional as a shorthand for demonstrating logical equivalence between two propositions. -For two putatively equivalent propositions $P$ and $Q$, $P$ and $Q$ are logically equivalent if the compound proposition $P \equiv Q$ is logically true. +For two putatively equivalent propositions $P$ and $Q$, $P$ and $Q$ are logically equivalent if the compound proposition $P \leftrightarrow Q$ is logically true. diff --git a/Logic/Proofs/Biconditional_Elimination.md b/Logic/Proofs/Biconditional_Elimination.md index 7b71ca5..b1f6111 100644 --- a/Logic/Proofs/Biconditional_Elimination.md +++ b/Logic/Proofs/Biconditional_Elimination.md @@ -1,9 +1,11 @@ --- categories: - - Mathematics -tags: [logic] + - Logic +tags: [derivation-rules] --- -Give that the biconditional means that if $P$ is the case, $Q$ is the case and if $Q$ is the case, $P$ must be the case, if we have $P \equiv Q$ and $P$, we can derive $Q$ and vice versa. +# Biconditional Elimination -![biconditional-elim.png](../img/biconditional-elim.png) +Give that the biconditional means that if $P$ is the case, $Q$ must be the case and if $Q$ is the case, $P$ must be the case, if we have $P \leftrightarrow Q$ and $P$, we can derive $Q$ and vice versa. + +![](/img/biconditional-elim.png) diff --git a/Logic/Proofs/Biconditional_Introduction.md b/Logic/Proofs/Biconditional_Introduction.md index e864f16..9802d3a 100644 --- a/Logic/Proofs/Biconditional_Introduction.md +++ b/Logic/Proofs/Biconditional_Introduction.md @@ -1,9 +1,11 @@ --- categories: - - Mathematics -tags: [] + - Logic +tags: [derivation-rules] --- -The biconditional means if $P$ is the case, $Q$ is the case and if $Q$ is the case, $P$ must be the case. Thus to introduce this operator we must demonstrate both that $Q$ follows from $P$ and that $P$ follows from $Q$. We do this via two sub-proofs. +# Biconditional introduction -![bi-intro.png](../img/bi-intro.png) +The biconditional means if $P$ is the case, $Q$ must be the case and if $Q$ is the case, $P$ must be the case. Thus to introduce this operator we must demonstrate both that $Q$ follows from $P$ and that $P$ follows from $Q$. We do this via two sub-proofs. + +![](/img/bi-intro.png) diff --git a/Logic/Proofs/Conditional_Elimination.md b/Logic/Proofs/Conditional_Elimination.md index 1a3672a..bd1c245 100644 --- a/Logic/Proofs/Conditional_Elimination.md +++ b/Logic/Proofs/Conditional_Elimination.md @@ -1,9 +1,11 @@ --- categories: - - Mathematics -tags: [logic] + - Logic +tags: [derivation-rules] --- +# Conditional elimination + If we have a conditional and we have independently derived its antecedent, we may invoke its consequent. This is often referred to as _Modus ponens_ (affirming the antecedent). -![cond-elim.png](../img/cond-elim.png) +![](/img/cond-elim.png) diff --git a/Logic/Proofs/Conditional_Introduction.md b/Logic/Proofs/Conditional_Introduction.md index c522575..5b552be 100644 --- a/Logic/Proofs/Conditional_Introduction.md +++ b/Logic/Proofs/Conditional_Introduction.md @@ -1,9 +1,11 @@ --- categories: - - Mathematics -tags: [logic] + - +tags: [derivation-rules] --- -If we can show that $Q$ follows from $P$ (typically via a subproof) than we can assert that P implies Q. This is also sometimes known as _Conditional Proof_ +# Conditional Introduction -![cond-intro.png](../img/cond-intro.png) +If we can show that $Q$ follows from $P$ (typically via a sub-proof) than we can assert that P implies Q. This is also sometimes known as _Conditional Proof_ + +![](/img/cond-intro.png) diff --git a/Logic/Proofs/Conjunction_Elimination.md b/Logic/Proofs/Conjunction_Elimination.md index 02ec5cf..6e866a6 100644 --- a/Logic/Proofs/Conjunction_Elimination.md +++ b/Logic/Proofs/Conjunction_Elimination.md @@ -1,9 +1,11 @@ --- categories: - - Mathematics -tags: [logic] + - Logic +tags: [derivation-rules] --- +# Conditional Elimination + If a conjunction exists, it means that both conjuncts are the case; therefore we can legitimately extract either one of them. Also known as _Simplification_. -![conjunc-elim.png](../img/conjunc-elim.png) +![](/img/conjunc-elim.png) diff --git a/Logic/Proofs/Conjunction_Introduction.md b/Logic/Proofs/Conjunction_Introduction.md index 1f48a31..31d2018 100644 --- a/Logic/Proofs/Conjunction_Introduction.md +++ b/Logic/Proofs/Conjunction_Introduction.md @@ -1,9 +1,9 @@ --- categories: - - Mathematics -tags: [logic] + - Logic +tags: [derivation-rules] --- If two conjuncts have each been independently derived then they can be conjoined. Also known more simply as _Conjunction_ -![conjunc-intro.png](../img/conjunc-intro.png) +![](/img/conjunc-intro.png) diff --git a/Logic/Proofs/Disjunction_Elimination.md b/Logic/Proofs/Disjunction_Elimination.md index abe8717..26ac386 100644 --- a/Logic/Proofs/Disjunction_Elimination.md +++ b/Logic/Proofs/Disjunction_Elimination.md @@ -1,18 +1,20 @@ --- categories: - - Mathematics -tags: [logic] + - Logic +tags: [derivation-rules] --- +# Disjunction Elimination + This rule is sometimes also referred to as _Constructive Dilemma_. This can be a bit tricky to understand because the goal is to derive or _introduce_ a new proposition separate from the disjunction you start out with. This may be disjunction, a single proposition or a proposition containing any other logical connective. You do this by constructing two sub-proofs, one for each of the disjuncts comprising the disjunction you start out with. If you can derive your target proposition as the conclusion of each subproof then you may invoke the conclusion in the main proof and take it to be derived. -![disjunc-elim.png](../img/disjunc-elim.png) +![](/img/disjunc-elim.png) _Here is an example where Disjunction Elimination is used to derive a new disjunction._ -![proofs-drawio-Page-6.drawio.png](../img/proofs-drawio-Page-6.drawio.png) +![](/img/proofs-drawio-Page-6.drawio.png) _Here are two further examples that use Disjunction Elimination to derive singular propositions_ -![ORelim1.png](../img/ORelim1.png) -![ORelim2.png](../img/ORelim2.png) +![](/img/ORelim1.png) +![](/img/ORelim2.png) diff --git a/Logic/Proofs/Disjunction_Introduction.md b/Logic/Proofs/Disjunction_Introduction.md index d50e8b2..55f89f5 100644 --- a/Logic/Proofs/Disjunction_Introduction.md +++ b/Logic/Proofs/Disjunction_Introduction.md @@ -1,10 +1,12 @@ --- categories: - - Mathematics -tags: [logic] + - Logic +tags: [derivation-rules] --- +# Disjunction Introduction + This rule can seem a little odd: like we are randomly introducing an additional proposition without giving any justification. However this is just a consequence of the fact if $P$ is true, so is $P \lor Q$ since disjunction is not the same as conjunction: only one disjunct needs to be true for the compound disjunction to be true. This is represented in the context of [truth-trees](Truth-trees.md#disjunction-decomposition) by the fact that truth can pass up via either branch of a disjunction pattern. This rule is sometimes also referred to (confusingly) as _Addition_. -![disjunc-intro.png](../img/disjunc-intro.png) +![](/img/disjunc-intro.png) diff --git a/Logic/Proofs/Formal_proofs_in_propositional_logic.md b/Logic/Proofs/Formal_proofs_in_propositional_logic.md index 79c1be8..ffd6fa6 100644 --- a/Logic/Proofs/Formal_proofs_in_propositional_logic.md +++ b/Logic/Proofs/Formal_proofs_in_propositional_logic.md @@ -1,9 +1,11 @@ --- categories: - - Mathematics -tags: [logic] + - Logic +tags: [propositional-logic] --- +# Formal proofs in propositional logic + When we construct a formal proof in logic we are seeking to show that a certain proposition is **derivable** from other propositions. We use the words _derivation_ and _proof_ interchangeably. > A sentence $P$ is derivable in a system of propositional logic from a finite set of sentences if and only if there is a derivation in this system in which all and only the members of the set are **primary assumptions** and $P$ is the sentence on the last line. @@ -15,7 +17,7 @@ Derivability is therefore a property that a proposition can possess relative to For instance to demonstrate derivability for: $$ -{\sim F \lor D, F, D \supset (G & H)} \vdash G &H +\{ \lnot F \lor D, F, D \rightarrow (G \land H) \} \vdash G \land H $$ We would establish $\sim F \lor D, F, D \supset (G & H)$ as primary assumptions and then, using the derivation rules of the system conclude with $G&H$. Every sentence in the derivation is either a **primary assumption** or an **auxiliary** assumption or justified by the rules of the derivation. An auxiliary assumption is one belonging to a sub-derivation. The primary assumptions belong to the main derivation.