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

Logic/Proofs/Formal_proofs_in_propositional_logic.md

@@ -20,8 +20,9 @@ $$
 \{ \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.
-For any given derivation of the form $\Gamma \vdash P$ there may be a number of ways of demonstrating the derivation (more than one application of the rules governing the system) but only one is sufficient to establish derivability.
+We would establish $\lnot F \lor D, F, D \rightarrow (G \land H)$ as primary assumptions and then, using the derivation rules of the system conclude with $G\land 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 an assumption belonging to a sub-derivation. Primary assumptions belong to the main derivation. For any given derivation of the form $\Gamma \vdash P$ there may be a number of ways of demonstrating the derivation (more than one application of the rules governing the system) but one alone is sufficient to establish derivability.
 
 > We will tend to use the terms _derivation_ and _proof_ interchangeably but we should note that there is a technical distinction in that a **proof is a derivation in which all of the assumptions have been discharged**
 
@@ -31,13 +32,14 @@ We place assumptions above derivations and mark them _A_ in the right-hand margi
 
 We divide assumptions from derivations with a horizontal line. We number each line and use this to refer to the line we are applying the derivation to. Sub-proofs follow this structure recursively.
 This is known as _Fitch notation_
-_Schematically_
 
-![proofs-drawio-Page-5.drawio.png](../img/proofs-drawio-Page-5.drawio.png)
+_Schematically_:
 
-_Applied example_
+![](/img/proofs-drawio-Page-5.drawio.png)
 
-![proofs-drawio-Page-6.drawio.png](../img/proofs-drawio-Page-6.drawio.png)
+_Applied example_:
+
+![](/img/proofs-drawio-Page-6.drawio.png)
 
 ## Sub-proofs
 
@@ -45,7 +47,7 @@ When a sub-proof is terminated, the assumption with which it starts is said to b
 
 ## Derivation rules
 
-Derivation rules are [syntactic](Syntax%20of%20sentential%20logic.md) rather than semantic. They are applied on the basis of their form rather than on the basis of the truth conditions of the sentences they are applied to.
+Derivation rules are [syntactic](/Logic/Propositional_logic/Syntax_of_sentential_logic.md) rather than semantic. They are applied on the basis of their form rather than on the basis of the truth conditions of the sentences they are applied to.
 
 > Derivation rules can be applied without having an interpretation of the symbols in mind. A derivation rule tells us that: given a group of symbols with a certain structure, we can write down another group of symbols with a certain structure.
 
@@ -53,13 +55,13 @@ Each of the main logical connectives has an associated derivation rule. The bina
 
 The main derivation rules:
 
-- [Negation Introduction](Negation%20Introduction.md)
-- [Negation Elimination](Negation%20Elimination.md)
-- [Conjunction Introduction](Conjunction%20Introduction.md)
-- [Conjunction Elimination](Conjunction%20Elimination.md)
-- [Disjunction Introduction](Disjunction%20Introduction.md)
-- [Disjunction Elimination](Disjunction%20Elimination.md)
-- [Conditional Introduction](Conditional%20Introduction.md)
-- [Disjunction Elimination](Disjunction%20Elimination.md)
-- [Biconditional Introduction](Biconditional%20Introduction.md)
-- [Biconditional Elimination](Biconditional%20Elimination.md)
+- [Negation Introduction](/Logic/Proofs/Negation_Introduction.md)
+- [Negation Elimination](/Logic/Proofs/Negation_Elimination.md)
+- [Conjunction Introduction](/Logic/Proofs/Conjunction_Introduction.md)
+- [Conjunction Elimination](/Logic/Proofs/Conditional_Elimination.md)
+- [Disjunction Introduction](/Logic/Proofs/Disjunction_Introduction.md)
+- [Disjunction Elimination](/Logic/Proofs/Disjunction_Elimination.md)
+- [Conditional Introduction](/Logic/Proofs/Conditional_Introduction.md)
+- [Disjunction Elimination](/Logic/Proofs/Disjunction_Elimination.md)
+- [Biconditional Introduction](/Logic/Proofs/Biconditional_Introduction.md)
+- [Biconditional Elimination](/Logic/Proofs/Biconditional_Elimination.md)