Definition:Johansson's Minimal Logic/Axioms
Jump to navigation
Jump to search
This page has been identified as a candidate for refactoring of advanced complexity. In particular: Bring this into line (eventually) with the redesign of PropCalc axiom structure documentation Until this has been finished, please leave {{Refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code. |
Definition
Rule of Assumption
- An assumption $\phi$ may be introduced at any stage of an argument.
Rule of Conjunction
- If we can conclude both $\phi$ and $\psi$, we may infer the compound statement $\phi \land \psi$.
Rule of Simplification
- $(1): \quad$ If we can conclude $\phi \land \psi$, then we may infer $\phi$.
- $(2): \quad$ If we can conclude $\phi \land \psi$, then we may infer $\psi$.
Rule of Addition
- $(1): \quad$ If we can conclude $\phi$, then we may infer $\phi \lor \psi$.
- $(2): \quad$ If we can conclude $\psi$, then we may infer $\phi \lor \psi$.
Proof by Cases
- If we can conclude $\phi \lor \psi$, and:
- $(1): \quad$ By making the assumption $\phi$, we can conclude $\chi$
- $(2): \quad$ By making the assumption $\psi$, we can conclude $\chi$
- then we may infer $\chi$.
Modus Ponendo Ponens
- If we can conclude $\phi \implies \psi$, and we can also conclude $\phi$, then we may infer $\psi$.
Rule of Implication
- If, by making an assumption $\phi$, we can conclude $\psi$ as a consequence, we may infer $\phi \implies \psi$.
- The conclusion $\phi \implies \psi$ does not depend on the assumption $\phi$, which is thus discharged.
Principle of Non-Contradiction
- If we can conclude both $\phi$ and $\neg \phi$, we may infer a contradiction.
Proof by Contradiction
- If, by making an assumption $\phi$, we can infer a contradiction as a consequence, then we may infer $\neg \phi$.
- The conclusion $\neg \phi$ does not depend upon the assumption $\phi$.