Autosave: 2022-12-25 15:00:05

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

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.

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)

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)

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)

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)

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)

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)

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)

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)

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.