From 19b48e6e990dfc54e52082e1ec0d9fddc36473cc Mon Sep 17 00:00:00 2001 From: thomasabishop Date: Sun, 25 Dec 2022 15:30:05 +0000 Subject: [PATCH] Autosave: 2022-12-25 15:30:05 --- .../Formal_proofs_in_propositional_logic.md | 36 ++++++++++--------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/Logic/Proofs/Formal_proofs_in_propositional_logic.md b/Logic/Proofs/Formal_proofs_in_propositional_logic.md index ffd6fa6..3a7877d 100644 --- a/Logic/Proofs/Formal_proofs_in_propositional_logic.md +++ b/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)