================================================================================ UTF-8-file qedeq_formal_logic_v1 Generated from http://www.qedeq.org/0_04_07/doc/math/qedeq_formal_logic_v1.xml Generated at 2013-05-24 07:36:47.570 ================================================================================ If the characters of this document don't display correctly try opening this document within a webbrowser and if necessary change the encoding to Unicode (UTF-8) Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.2 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. Formal Predicate Calculus ═════════════════════════ Michael Meyling The source for this document can be found here: http://www.qedeq.org/0_04_07/doc/math/qedeq_formal_logic_v1.xml Copyright by the authors. All rights reserved. If you have any questions, suggestions or want to add something to the list of modules that use this one, please send an email to the address mime@qedeq.org The authors of this document are: Michael Meyling ___________________________________________________ Summary ═══════ In this text we present the development of predicate calculus in axiomatic form. The language of our calculus bases on the formalizations of D .  H i l b e r t , W .  A c k e r m a n n [hilback], P .  S .  N o v i k o v [novikov], V .  D e t l o v s and K .  P o d n i e k s [detnieks]. New rules can be derived from the herein presented logical axioms and basic inference rules. Only these meta rules lead to a smooth flowing logical argumentation. For background informations see under https://dspace.lu.lv/dspace/handle/7/1308  [detnieks] and http://en.wikipedia.org/wiki/Propositional_calculus . ___________________________________________________ Chapter 1 Language ════════ In this chapter we define a formal language to express mathematical propositions in a very precise way. Although this document describes a very formal approach to express mathematical content it is not sufficent to serve as a definition for an computer readable document format. Therefore such an extensive specification has to be done elsewhere. Here our choosen format is the E x t e n s i b l e M a r k u p L a n g u a g e abbreviated X M L . XML is a set of rules for encoding documents electronically. ┌ │ See http://www.w3.org/XML/ for more information. └ The according formal syntax specification can be found at http://www.qedeq.org/current/xml/qedeq.xsd . It specifies a complete mathematical document format that enables the generation of LaTeX books and makes automatic proof checking possible. Further syntax restrictions and some explanations can be found at http://www.qedeq.org/current/doc/project/qedeq_logic_language_en.pdf . Even this document is (or was generated) from an XML file that can be found here: http://wwww.qedeq.org/0_04_07/doc/math/qedeq_logic_v1.xml . But now we just follow the traditional mathematical way to present the elements of mathematical logic. 1.1 Terms and Formulas ―――――――――――――――――――――― We use the l o g i c a l s y m b o l s L = { ‘¬’, ‘∧’, ‘∨’, ‘↔’, ‘→’, ‘∀’, ‘ ∃’ }, the p r e d i c a t e c o n s t a n t s C = {c^k_i | i, k ∈ ω}, the f u n c t i o n v a r i a b l e s ┌ │ Function variables are used for a shorter notation. For example │ writing an identity proposition x = y → f(x) = f(y). Also this │ introduction prepares for the syntax extension for functional │ classes. └ F = {f^k_i | i, k ∈ ω ∧ k > 0}, the f u n c t i o n c o n s t a n t s ┌ │ Function constants are also introduced for convenience and are used │ for direct defined class functions. For example to define building │ of the power class operator, the union and intersection operator and │ the successor function. All these function constants can be │ interpreted as abbreviations. └ H = {h^k_i | i, k ∈ ω}, the s u b j e c t v a r i a b l e s V = {v_i | i ∈ ω}, as well as p r e d i c a t e v a r i a b l e s P = {p^k_i | i, k ∈ ω}. ┌ │ By ω we understand the natural numbers including zero. All involved │ symbols are pairwise disjoint. Therefore we can conclude for │ example: f^k_i = f^(k')_(i') → (k = k’ ∧ i = i’) and h^k_i ≠ v_j. └ For the a r i t y or r a n k of an operator we take the upper index. The set of predicate variables with zero arity is also called set of p r o p o s i t i o n v a r i a b l e s or s e n t e n c e l e t t e r s : A := {p_i⁰ | i ∈ ω }. For subject variables we write short hand certain lower letters: v₁ = ‘u’, v₂ = ‘v’, v₃ = ‘w’, v₄ = ‘x’, v₅ = ‘y’, v₅ = ‘z’. Furthermore we use the following short notations: for the predicate variables pⁿ₁ = ‘φ’ und pⁿ₂ = ‘ψ’, where the appropriate arity n is calculated by counting the subsequent parameters, for the proposition variables a₁ = ‘A’, a₂ = ‘B’ and a₃ = C’, for the function variables: fⁿ₁ = ‘f’ und fⁿ₂ = ‘g’, where again the appropriate arity n is calculated by counting the subsequent parameters. All binary propositional operators are written in infix notation. Parentheses surrounding groups of operands and operators are necessary to indicate the intended order in which operations are to be performed. E. g. for the operator ∧ with the parameters A and B we write (A ∧ B). In the absence of parentheses the usual precedence rules determine the order of operations. Especially outermost parentheses are omitted. Also empty parentheses are stripped. The operators have the order of precedence described below (starting with the highest). ¬, ∀, ∃ ∧ ∨ →, ↔ The term t e r m is defined recursively as follows: 1. Every subject variable is a term. 2. Let i, k ∈ ω and let t₁, ..., t_k be terms. Then h^k_i(t₁, ..., t_k) is a term and if k > 0, so f^k_i(t₁, ..., t_k) is a term too. Therefore all zero arity function constants {h⁰_i | i ∈ ω} are terms. They are called i n d i v i d u a l c o n s t a n t s . ┌ │ In an analogous manner subject variables might be defined as │ function variables of zero arity. Because subject variables play an │ important role they have their own notation. └ We define a f o r m u l a and the relations f r e e and b o u n d subject variable recursivly as follows: 1. Every proposition variable is a formula. Such formulas contain no free or bound subject variables. 2. If p^k is a predicate variable with arity k and c^k is a predicate constant with arity k and t₁, t₂, ..., t_k are terms, then p^k(t₁, t₂, ... t_k) and c^k(t₁, t₂, ..., t_k) are formulas. All subject variables that occur at least in one of t₁, t₂, ..., t_k are free subject variables. Bound subject variables does not occur. ┌ │ This second item includes the first one, which is only listed for │ clarity. └ 3. Let α, β be formulas in which no subject variables occur bound in one formula and free in the other. Then ¬ α, (α ∧ β), (α ∨ β), (α → β) and (α ↔ β) are also formulas. Subject variables which occur free (respectively bound) in α or β stay free (respectively bound). 4. If in the formula α the subject variable x₁ occurs not bound ┌ │ This means that x₁ is free in the formula or does not occur at │ all. └ , then also ∀ x₁ α and ∃ x₁ α are formulas. The symbol ∀ is called u n i v e r s a l q u a n t i f i e r and ∃ as e x i s t e n t i a l q u a n t i f i e r . Except for x₁ all free subject variables of α stay free. All bound subject variables are still bound and additionally x₁ is bound too. All formulas that are only built by usage of 1. and 3. are called formulas of the p r o p o s i t i o n a l c a l c u l u s . For each formula α the following proposition holds: the set of free subject variables is disjoint with the set of bound subject variables.. ┌ │ Other formalizations allow for example ∀ x₁ α also if x₁ occurs │ already bound within α. Also propositions like α(x₁) ∧ (∀ x₁ β) are │ allowed. In this formalizations free and bound are defined for a │ single occurrence of a variable. └ If a formula has the form ∀ x₁   α respectively ∃ x₁   α then the formula α is called the s c o p e of the quantifier ∀ respectively ∃. All formulas that are used to build up a formula by 1. to 4. are called p a r t f o r m u l a s . ___________________________________________________ Chapter 2 Axioms and Rules of Inference ═════════════════════════════ We now state the system of axioms for the propositional calculus and present the rules for obtaining new formulas from them. 2.1 Axioms ―――――――――― We just list the axioms without further explanations. ☉ Axiom 1 (Implication Introduction) [axiom:THEN-1] A → (B → A) ☉ Axiom 2 (Distribute Hypothesis over Implication) [axiom:THEN-2] (A → (B → C)) → ((A → B) → (A → C)) ☉ Axiom 3 (Eliminate Conjunction Right) [axiom:AND-1] (A ∧ B) → A ☉ Axiom 4 (Eliminate Conjunction Left) [axiom:AND-2] (A ∧ B) → B ☉ Axiom 5 (Conjunction Introduction) [axiom:AND-3] B → (A → (A ∧ B)) ☉ Axiom 6 (Disjunction Introduction Right) [axiom:OR-1] A → (A ∨ B) ☉ Axiom 7 (Disjunction Introduction Left) [axiom:OR-2] A → (B ∨ A) ☉ Axiom 8 (Disjunction Elimination) [axiom:OR-3] (A → C) → ((B → C) → ((A ∨ B) → C)) ☉ Axiom 9 (Negation Introduction) [axiom:NOT-1] (A → B) → ((A → ¬ B) → ¬ A) ☉ Axiom 10 (Negation Elimination) [axiom:NOT-2] ¬ A → (A → B) ☉ Axiom 11 (Excluded Middle) [axiom:NOT-3] A ∨ ¬ A ☉ Axiom 12 (Equivalence Elimination right) [axiom:IFF-1] (A ↔ B) → (A → B) ☉ Axiom 13 (Equivalence Elimination left) [axiom:IFF-2] (A ↔ B) → (B → A) ☉ Axiom 14 (Equivalence Introduction) [axiom:IFF-3] (A → B) → ((B → A) → (A ↔ B)) If something is true for all x, it is true for any specific y. ☉ Axiom 15 (Universal Instantiation) [axiom:universalInstantiation] ∀ x φ(x) → φ(y) If a predicate holds for some particular y, then there is an x for which the predicate holds. ☉ Axiom 16 (Existential Generalization) [axiom:existencialGeneralization] φ(y) → ∃ x φ(x) 2.2 Rules of Inference ―――――――――――――――――――――― The following rules of inference enable us to obtain new true formulas from the axioms that are assumed to be true. From these new formulas we derive further formulas. So we can successively extend the set of true formulas. ☉ Rule 1 (Add true formula) [rule:addProvenFormula] Name: Add - Version: 0.01.00 Addition of an axiom, definition or already proven formula. We have to reference to the location of a true formula. ☉ Rule 2 (Modus Ponens) [rule:modusPonens] Name: MP - Version: 0.01.00 If both formulas α and α → β are true, then we can conclude that β is true as well. ☉ Rule 3 (Replace Free Subject Variable) [rule:replaceFree] Name: SubstFree - Version: 0.01.00 We start with a true formula. A free subject variable may be replaced by an arbitrary term, provided that the substituted term contains no subject variable that have a bound occurrence in the original formula. All occurrences of the free variable must be simultaneously replaced. The prohibition to use subject variables within the term that occur bound in the original formula has two reasons. First it ensures that the resulting formula is well-formed. Secondly it preserves the validity of the formula. Let us look at the following derivation. ∀ x ∃ y φ(x, y) → ∃ y φ(z,y) with axiom 15 ∀ x ∃ y φ(x, y) → ∃ y φ(y,y) forbidden replacement: z in y, despite y is already bound ∀ x ∃ y x ≠ y → ∃ y y ≠ y replace φ by ≠ This last proposition is not valid in many models. ☉ Rule 4 (Rename Bound Subject Variable) [rule:renameBound] Name: Rename - Version: 0.01.00 We may replace a bound subject variable occurring in a formula by any other subject variable, provided that the new variable occurs not free in the original formula. If the variable to be replaced occurs in more than one scope, then the replacement needs to be made in one scope only. ☉ Rule 5 (Replace Predicate Variable) [rule:replacePred] Name: SubstPred - Version: 0.01.00 Let α be a true formula that contains a predicate variable p of arity n, let x₁, ..., x_n be pairwise different subject variables and let β(x₁, ..., x_n) be a formula where x₁, ..., x_n are not bound. The formula β(x₁, ..., x_n) must not contain all x₁, ..., x_n as free subject variables. Furthermore it can also have other subject variables either free or bound. If the following conditions are fulfilled, then a replacement of all occurrences of p(t₁, ..., t_n) each with appropriate terms t₁, ..., t_n in α by β(t₁, ..., t_n) results in another true formula. 1. the free variables of β(x₁, ..., x_n) without x₁, ..., x_n do not occur as bound variables in α 2. each occurrence of p(t₁, ..., t_n) in α contains no bound variable of β(x₁, ..., x_n) 3. the result of the substitution is a well-formed formula See III § 5 in [hilback]. We can think in the same lines as by rule 3. The prohibition to use additional subject variables within the replacement formula that occur bound in the original formula assurs that the resulting formula is well-formed. Furthermore it preserves the validity of the formla. Take a look at the following derivation. φ(x) → ∃ y φ(y) with axiom 16 (∃ y y = y) ∧ φ(x) → ∃ y φ(y) ∃ y (y = y ∧ φ(x)) → ∃ y φ(y) ∃ y (y = y ∧ x ≠ y) → ∃ y y ≠ y forbidden replacment: φ(x) by x ≠ y, despite y is already bound ∃ y x ≠ y → ∃ y y ≠ y The last proposition is not valid in many models. Analogous to rule 5 we can replace function variables too. ☉ Rule 6 (Replace Function Variable) [rule:replaceFunct] Name: SubstFun - Version: 0.01.00 Let α be an already proved formula that contains a function variable σ of arity n, let x₁, ..., x_n be pairwise different subject variables and let τ(x₁, ..., x_n) be an arbitrary term where x₁, ..., x_n are not bound. The term τ(x₁, ..., x_n) must not contain all x₁, ..., x_n as free subject variables. Furthermore it can also have other subject variables either free or bound. If the following conditions are fulfilled we can obtain a new true formula by replacing each occurrence of σ(t₁, ..., t_n) with appropriate terms t₁, ..., t_n in α by τ(t₁, ..., t_n). 1. the free variables of τ(x₁, ..., x_n) without x₁, ..., x_n do not occur as bound variables in α 2. each occurrence of σ(t₁, ..., t_n) in α contains no bound variable of τ(x₁, ..., x_n) 3. the result of the substitution is a well-formed formula ☉ Rule 7 (Universal Generalization) [rule:universalGeneralization] Name: Universal - Version: 0.01.00 If α → β(x₁) is a true formula and α does not contain the subject variable x₁, then α → (∀ x₁ (β(x₁))) is a true formula too. ☉ Rule 8 (Existential Generalization) [rule:existentialGeneralization] Name: Existential - Version: 0.01.00 If α(x₁) → β is already proved to be true and β does not contain the subject variable x₁, then (∃ x₁ α(x₁)) → β is also a true formula. ___________________________________________________ Chapter 3 Propositional Calculus ══════════════════════ In this chapter we introduce an importent new inference rule and develop the traditional results of propositional calculus. 3.1 First Propositions ―――――――――――――――――――――― Here we draw the first conclusions. ☉ Proposition 1 [proposition:implicationReflexive1] A → A Proof (formal): (1) A → (B → A) Add axiom 1 (2) (A → (B → C)) → ((A → B) → (A → C)) Add axiom 2 (3) A → (B ∨ A) Add axiom 7 (4) A → ((B ∨ A) → A) SubstPred B by B ∨ A in (1) (5) (A → ((B ∨ A) → C)) → ((A → (B ∨ A)) SubstPred B by B ∨ A in (2) → (A → C)) (6) (A → ((B ∨ A) → A)) → ((A → (B ∨ A)) SubstPred C by A in (5) → (A → A)) (7) (A → (B ∨ A)) → (A → A) MP (6), (4) (8) A → A MP (7), (3) q.e.d. ☉ Proposition 2 [proposition:implication2] (A ∨ A) → A Proof (formal): (1) A → A Add proposition 1 (2) (A → C) → ((B → C) → ((A ∨ B) → C)) Add axiom 8 (3) (A → C) → ((A → C) → ((A ∨ A) → C)) SubstPred B by A in (2) (4) (A → A) → ((A → A) → ((A ∨ A) → A)) SubstPred C by A in (3) (5) (A → A) → ((A ∨ A) → A) MP (4), (1) (6) (A ∨ A) → A MP (5), (1) q.e.d. ☉ Proposition 3 [proposition:implication03] (A ∨ B) → (B ∨ A) Proof (formal): (1) A → (A ∨ B) Add axiom 6 (2) A → (B ∨ A) Add axiom 7 (3) (A → C) → ((B → C) → ((A ∨ B) → C)) Add axiom 8 (4) D → (D ∨ B) SubstPred A by D in (1) (5) (A → (C ∨ A)) → ((B → (C ∨ A)) → ((A SubstPred C by C ∨ A in (3) ∨ B) → (C ∨ A))) (6) D → (D ∨ A) SubstPred B by A in (4) (7) (A → (B ∨ A)) → ((B → (B ∨ A)) → ((A SubstPred C by B in (5) ∨ B) → (B ∨ A))) (8) (B → (B ∨ A)) → ((A ∨ B) → (B ∨ A)) MP (7), (2) (9) B → (B ∨ A) SubstPred D by B in (6) (10) (A ∨ B) → (B ∨ A) MP (8), (9) q.e.d. ☉ Proposition 4 [proposition:implication04] ¬ (A ∧ ¬ A) Proof (formal): (1) (A ∧ B) → A Add axiom 3 (2) (A ∧ B) → B Add axiom 4 (3) (A → B) → ((A → ¬ B) → ¬ A) Add axiom 9 (4) (A ∧ ¬ A) → A SubstPred B by ¬ A in (1) (5) (A ∧ ¬ A) → ¬ A SubstPred B by ¬ A in (2) (6) ((A ∧ ¬ A) → B) → (((A ∧ ¬ A) → ¬ B) SubstPred A by A ∧ ¬ A in (3) → ¬ (A ∧ ¬ A)) (7) ((A ∧ ¬ A) → A) → (((A ∧ ¬ A) → ¬ A) SubstPred B by A in (6) → ¬ (A ∧ ¬ A)) (8) ((A ∧ ¬ A) → ¬ A) → ¬ (A ∧ ¬ A) MP (7), (4) (9) ¬ (A ∧ ¬ A) MP (8), (5) q.e.d. 3.2 Deduction Theorem ――――――――――――――――――――― We prove the deduction theorem. This leads to the new rule C o n d i t i o n a l P r o o f . If we can prove B by assuming A as a hypothesis then we have proved A → B. This reasoning is justified by the so-called d e d u c t i o n t h e o r e m . The deduction theorem holds for all first-order theories with the usual deductive systems for first-order logic. However our use of proposition variables and substitution rules make difficulties. We have to restrict the allowed inference rules to get a simular result. ☉ Rule 9 [rule:CP] Name: CP - Version: 0.02.00 We have the well-formed formula α and add it as a new proof line. Now we modify the existing inference rules. We can add a further proof line β if α → β is a well-formed formula and the usage of a previous inference rule with the following restrictions justifies the addition: for rule 3 occurs the replaced free variable not in α, for rule 5 occurs the replaced predicate variable not in α, for rule 6 occurs the replaced function variable not in α. Based on: (axiom:THEN-1) (axiom:THEN-2) The following rules have to be extended. Name: MP - Version: 0.02.00 See rule 9. Name: Add - Version: 0.02.00 See rule 9. Name: Rename - Version: 0.02.00 See rule 9. Name: SubstFree - Version: 0.02.00 See rule 9. Name: SubstPred - Version: 0.02.00 See rule 9. Name: SubstFun - Version: 0.02.00 See rule 9. Name: Universal - Version: 0.02.00 See rule 9. Name: Existential - Version: 0.02.00 See rule 9. Proof: TODO 20110613 m31 q.e.d. The deduction theorem enables us to prove propositions more easier in the next sections. 3.3 Propositions about implication ―――――――――――――――――――――――――――――――――― We use rule 9 to derive more propositions containing only the implication operator. ☉ Proposition 5 [proposition:implication10] (A → (A → B)) → (A → B) Proof (formal): Conditional Proof (1) A → (A → B) Hypothesis Conditional Proof (2) A Hypothesis (3) A → B MP (1), (2) (4) B MP (3), (2) (5) A → B Conclusion (6) (A → (A → B)) → (A → B) Conclusion q.e.d. ☉ Proposition 6 [proposition:implication11] ((A → B) → (A → C)) → (A → (B → C)) Proof (formal): (1) A → (B → A) Add axiom 1 (2) D → (B → D) SubstPred A by D in (1) (3) D → (A → D) SubstPred B by A in (2) (4) B → (A → B) SubstPred D by B in (3) Conditional Proof (5) (A → B) → (A → C) Hypothesis Conditional Proof (6) A Hypothesis Conditional Proof (7) B Hypothesis (8) A → B MP (4), (7) (9) A → C MP (5), (8) (10) C MP (9), (6) (11) B → C Conclusion (12) A → (B → C) Conclusion (13) ((A → B) → (A → C)) → (A → (B → C)) Conclusion q.e.d. ☉ Proposition 7 [proposition:implication12] (A → B) → ((B → C) → (A → C)) Proof (formal): Conditional Proof (1) A → B Hypothesis Conditional Proof (2) B → C Hypothesis Conditional Proof (3) A Hypothesis (4) B MP (1), (3) (5) C MP (2), (4) (6) A → C Conclusion (7) (B → C) → (A → C) Conclusion (8) (A → B) → ((B → C) → (A → C)) Conclusion q.e.d. ☉ Proposition 8 [proposition:implication13] (A → (B → C)) → (B → (A → C)) Proof (formal): Conditional Proof (1) A → (B → C) Hypothesis Conditional Proof (2) B Hypothesis Conditional Proof (3) A Hypothesis (4) B → C MP (1), (3) (5) C MP (4), (2) (6) A → C Conclusion (7) B → (A → C) Conclusion (8) (A → (B → C)) → (B → (A → C)) Conclusion q.e.d. 3.4 Propositions about conjunction ―――――――――――――――――――――――――――――――――― We use rule 9 to derive more propositions containing the conjunction operator. ☉ Proposition 9 [proposition:implication14] A → (A ∧ A) Proof (formal): (1) B → (A → (A ∧ B)) Add axiom 5 (2) A → (A → (A ∧ A)) SubstPred B by A in (1) Conditional Proof (3) A Hypothesis (4) A → (A ∧ A) MP (2), (3) (5) A ∧ A MP (4), (3) (6) A → (A ∧ A) Conclusion q.e.d. ☉ Proposition 10 [proposition:AND-3b] A → (B → (A ∧ B)) Proof (formal): (1) (A → (B → C)) → (B → (A → C)) Add proposition 8 (2) (A → (D → C)) → (D → (A → C)) SubstPred B by D in (1) (3) (B → (D → C)) → (D → (B → C)) SubstPred A by B in (2) (4) (B → (A → C)) → (A → (B → C)) SubstPred D by A in (3) (5) (B → (A → (A ∧ B))) → (A → (B → (A ∧ SubstPred C by A ∧ B in (4) B))) (6) B → (A → (A ∧ B)) Add axiom 5 (7) A → (B → (A ∧ B)) MP (5), (6) q.e.d. ☉ Proposition 11 [proposition:implication15] ((A → B) ∧ (B → C)) → (A → C) Proof (formal): (1) (A ∧ B) → A Add axiom 3 (2) (A ∧ (B → C)) → A SubstPred B by B → C in (1) (3) ((A → B) ∧ (B → C)) → (A → B) SubstPred A by A → B in (2) (4) (A ∧ B) → B Add axiom 4 (5) (A ∧ (B → C)) → (B → C) SubstPred B by B → C in (4) (6) ((A → B) ∧ (B → C)) → (B → C) SubstPred A by A → B in (5) Conditional Proof (7) (A → B) ∧ (B → C) Hypothesis (8) A → B MP (3), (7) (9) B → C MP (6), (7) (10) (A → B) → ((B → C) → (A → C)) Add proposition 7 (11) (B → C) → (A → C) MP (10), (8) (12) A → C MP (11), (9) (13) ((A → B) ∧ (B → C)) → (A → C) Conclusion q.e.d. ☉ Proposition 12 [proposition:implication17] (A → B) → ((A → C) → (A → (B ∧ C))) Proof (formal): (1) B → (A → (A ∧ B)) Add axiom 5 (2) C → (A → (A ∧ C)) SubstPred B by C in (1) (3) C → (B → (B ∧ C)) SubstPred A by B in (2) Conditional Proof (4) A → B Hypothesis Conditional Proof (5) A → C Hypothesis Conditional Proof (6) A Hypothesis (7) C MP (5), (6) (8) B → (B ∧ C) MP (3), (7) (9) B MP (4), (6) (10) B ∧ C MP (8), (9) (11) A → (B ∧ C) Conclusion (12) (A → C) → (A → (B ∧ C)) Conclusion (13) (A → B) → ((A → C) → (A → (B ∧ C))) Conclusion q.e.d. ☉ Proposition 13 [proposition:implication18] (A → B) → ((A ∧ C) → (B ∧ C)) Proof (formal): (1) (A ∧ B) → A Add axiom 3 (2) (A ∧ C) → A SubstPred B by C in (1) (3) (A ∧ B) → B Add axiom 4 (4) (A ∧ C) → C SubstPred B by C in (3) (5) B → (A → (A ∧ B)) Add axiom 5 (6) C → (A → (A ∧ C)) SubstPred B by C in (5) (7) C → (B → (B ∧ C)) SubstPred A by B in (6) Conditional Proof (8) A → B Hypothesis Conditional Proof (9) A ∧ C Hypothesis (10) A MP (2), (9) (11) B MP (8), (10) (12) C MP (4), (9) (13) B → (B ∧ C) MP (7), (12) (14) B ∧ C MP (13), (11) (15) (A ∧ C) → (B ∧ C) Conclusion (16) (A → B) → ((A ∧ C) → (B ∧ C)) Conclusion q.e.d. ☉ Proposition 14 [proposition:implication19] (A ∧ B) → (B ∧ A) Proof (formal): (1) B → (A → (A ∧ B)) Add axiom 5 (2) C → (A → (A ∧ C)) SubstPred B by C in (1) (3) C → (B → (B ∧ C)) SubstPred A by B in (2) (4) A → (B → (B ∧ A)) SubstPred C by A in (3) (5) (A ∧ B) → A Add axiom 3 (6) (A ∧ B) → B Add axiom 4 Conditional Proof (7) A ∧ B Hypothesis (8) A MP (5), (7) (9) B → (B ∧ A) MP (4), (8) (10) B MP (6), (7) (11) B ∧ A MP (9), (10) (12) (A ∧ B) → (B ∧ A) Conclusion q.e.d. ☉ Proposition 15 [proposition:implication20] (A → (B → C)) → ((A ∧ B) → C) Proof (formal): Conditional Proof (1) A → (B → C) Hypothesis Conditional Proof (2) A ∧ B Hypothesis (3) (A ∧ B) → A Add axiom 3 (4) A MP (3), (2) (5) (A ∧ B) → B Add axiom 4 (6) B MP (5), (2) (7) B → C MP (1), (4) (8) C MP (7), (6) (9) (A ∧ B) → C Conclusion (10) (A → (B → C)) → ((A ∧ B) → C) Conclusion q.e.d. ☉ Proposition 16 [proposition:implication21] ((A ∧ B) → C) → (A → (B → C)) Proof (formal): Conditional Proof (1) (A ∧ B) → C Hypothesis Conditional Proof (2) A Hypothesis (3) B → (A → (A ∧ B)) Add axiom 5 Conditional Proof (4) B Hypothesis (5) A → (A ∧ B) MP (3), (4) (6) A ∧ B MP (5), (2) (7) C MP (1), (6) (8) B → C Conclusion (9) A → (B → C) Conclusion (10) ((A ∧ B) → C) → (A → (B → C)) Conclusion q.e.d. ☉ Proposition 17 [proposition:implication25] ((A → B) ∧ (A → C)) → (A → (B ∧ C)) Proof (formal): (1) (A ∧ B) → A Add axiom 3 (2) (A ∧ C) → A SubstPred B by C in (1) (3) ((A → B) ∧ C) → (A → B) SubstPred A by A → B in (2) (4) ((A → B) ∧ (A → C)) → (A → B) SubstPred C by A → C in (3) (5) (A ∧ B) → B Add axiom 4 (6) (A ∧ C) → C SubstPred B by C in (5) (7) ((A → B) ∧ C) → C SubstPred A by A → B in (6) (8) ((A → B) ∧ (A → C)) → (A → C) SubstPred C by A → C in (7) (9) B → (A → (A ∧ B)) Add axiom 5 (10) C → (A → (A ∧ C)) SubstPred B by C in (9) (11) C → (B → (B ∧ C)) SubstPred A by B in (10) Conditional Proof (12) (A → B) ∧ (A → C) Hypothesis (13) A → B MP (4), (12) (14) A → C MP (8), (12) Conditional Proof (15) A Hypothesis (16) B MP (13), (15) (17) C MP (14), (15) (18) B → (B ∧ C) MP (11), (17) (19) B ∧ C MP (18), (16) (20) A → (B ∧ C) Conclusion (21) ((A → B) ∧ (A → C)) → (A → (B ∧ C)) Conclusion q.e.d. ☉ Proposition 18 [proposition:implication26] (A → (B ∧ C)) → ((A → B) ∧ (A → C)) Proof (formal): (1) (A ∧ B) → A Add axiom 3 (2) (A ∧ C) → A SubstPred B by C in (1) (3) (B ∧ C) → B SubstPred A by B in (2) (4) (A ∧ B) → B Add axiom 4 (5) (A ∧ C) → C SubstPred B by C in (4) (6) (B ∧ C) → C SubstPred A by B in (5) (7) B → (A → (A ∧ B)) Add axiom 5 (8) C → (A → (A ∧ C)) SubstPred B by C in (7) (9) C → ((A → B) → ((A → B) ∧ C)) SubstPred A by A → B in (8) (10) (A → C) → ((A → B) → ((A → B) ∧ (A → SubstPred C by A → C in (9) C))) Conditional Proof (11) A → (B ∧ C) Hypothesis Conditional Proof (12) A Hypothesis (13) B ∧ C MP (11), (12) (14) B MP (3), (13) (15) A → B Conclusion Conditional Proof (16) A Hypothesis (17) B ∧ C MP (11), (16) (18) C MP (6), (17) (19) A → C Conclusion (20) (A → B) → ((A → B) ∧ (A → C)) MP (10), (19) (21) (A → B) ∧ (A → C) MP (20), (15) (22) (A → (B ∧ C)) → ((A → B) ∧ (A → C)) Conclusion q.e.d. ☉ Proposition 19 [proposition:implication27] ((A ∧ B) ∧ C) → (A ∧ (B ∧ C)) Proof (formal): (1) (A ∧ B) → A Add axiom 3 (2) (A ∧ C) → A SubstPred B by C in (1) (3) ((A ∧ B) ∧ C) → (A ∧ B) SubstPred A by A ∧ B in (2) (4) (A ∧ B) → B Add axiom 4 (5) (A ∧ C) → C SubstPred B by C in (4) (6) ((A ∧ B) ∧ C) → C SubstPred A by A ∧ B in (5) (7) B → (A → (A ∧ B)) Add axiom 5 (8) C → (A → (A ∧ C)) SubstPred B by C in (7) (9) C → (B → (B ∧ C)) SubstPred A by B in (8) (10) (B ∧ C) → (A → (A ∧ (B ∧ C))) SubstPred B by B ∧ C in (7) Conditional Proof (11) (A ∧ B) ∧ C Hypothesis (12) A ∧ B MP (3), (11) (13) A MP (1), (12) (14) B MP (4), (12) (15) C MP (6), (11) (16) B → (B ∧ C) MP (9), (15) (17) B ∧ C MP (16), (14) (18) A → (A ∧ (B ∧ C)) MP (10), (17) (19) A ∧ (B ∧ C) MP (18), (13) (20) ((A ∧ B) ∧ C) → (A ∧ (B ∧ C)) Conclusion q.e.d. ☉ Proposition 20 [proposition:implication28] (A ∧ (B ∧ C)) → ((A ∧ B) ∧ C) Proof (formal): (1) (A ∧ B) → A Add axiom 3 (2) (A ∧ (B ∧ C)) → A SubstPred B by B ∧ C in (1) (3) (A ∧ C) → A SubstPred B by C in (1) (4) (B ∧ C) → B SubstPred A by B in (3) (5) (A ∧ B) → B Add axiom 4 (6) (A ∧ (B ∧ C)) → (B ∧ C) SubstPred B by B ∧ C in (5) (7) (A ∧ C) → C SubstPred B by C in (5) (8) (B ∧ C) → C SubstPred A by B in (7) (9) B → (A → (A ∧ B)) Add axiom 5 (10) C → (A → (A ∧ C)) SubstPred B by C in (9) (11) C → ((A ∧ B) → ((A ∧ B) ∧ C)) SubstPred A by A ∧ B in (10) Conditional Proof (12) A ∧ (B ∧ C) Hypothesis (13) A MP (2), (12) (14) B ∧ C MP (6), (12) (15) B MP (4), (14) (16) C MP (8), (14) (17) A → (A ∧ B) MP (9), (15) (18) A ∧ B MP (17), (13) (19) (A ∧ B) → ((A ∧ B) ∧ C) MP (11), (16) (20) (A ∧ B) ∧ C MP (19), (18) (21) (A ∧ (B ∧ C)) → ((A ∧ B) ∧ C) Conclusion q.e.d. 3.5 Propositions about disjunction ―――――――――――――――――――――――――――――――――― The disjunction is our theme here. ☉ Proposition 21 [proposition:implication40] (A ∨ (B ∨ C)) → ((A ∨ B) ∨ C) Proof (formal): (1) A → (A ∨ B) Add axiom 6 (2) A → (A ∨ C) SubstPred B by C in (1) (3) (A ∨ B) → ((A ∨ B) ∨ C) SubstPred A by A ∨ B in (2) Conditional Proof (4) A Hypothesis (5) A ∨ B MP (1), (4) (6) (A ∨ B) ∨ C MP (3), (5) (7) A → ((A ∨ B) ∨ C) Conclusion (8) A → (B ∨ A) Add axiom 7 (9) C → (B ∨ C) SubstPred A by C in (8) (10) C → (A ∨ C) SubstPred B by A in (9) (11) B → (A ∨ B) SubstPred C by B in (10) Conditional Proof (12) B Hypothesis (13) A ∨ B MP (11), (12) (14) (A ∨ B) ∨ C MP (3), (13) (15) B → ((A ∨ B) ∨ C) Conclusion (16) C → ((A ∨ B) ∨ C) SubstPred B by A ∨ B in (9) (17) (A → C) → ((B → C) → ((A ∨ B) → C)) Add axiom 8 (18) (A → D) → ((B → D) → ((A ∨ B) → D)) SubstPred C by D in (17) (19) (A → D) → ((C → D) → ((A ∨ C) → D)) SubstPred B by C in (18) (20) (B → D) → ((C → D) → ((B ∨ C) → D)) SubstPred A by B in (19) (21) (B → ((A ∨ B) ∨ C)) → ((C → ((A ∨ B) SubstPred D by (A ∨ B) ∨ C in (20) ∨ C)) → ((B ∨ C) → ((A ∨ B) ∨ C))) (22) (C → ((A ∨ B) ∨ C)) → ((B ∨ C) → ((A MP (21), (15) ∨ B) ∨ C)) (23) (B ∨ C) → ((A ∨ B) ∨ C) MP (22), (16) (24) (A → D) → (((B ∨ C) → D) → ((A ∨ (B SubstPred B by B ∨ C in (18) ∨ C)) → D)) (25) (A → ((A ∨ B) ∨ C)) → (((B ∨ C) → (( SubstPred D by (A ∨ B) ∨ C in (24) A ∨ B) ∨ C)) → ((A ∨ (B ∨ C)) → ((A ∨ B) ∨ C))) (26) ((B ∨ C) → ((A ∨ B) ∨ C)) → ((A ∨ (B MP (25), (7) ∨ C)) → ((A ∨ B) ∨ C)) (27) (A ∨ (B ∨ C)) → ((A ∨ B) ∨ C) MP (26), (23) q.e.d. ☉ Proposition 22 [proposition:implication41] ((A ∨ B) ∨ C) → (A ∨ (B ∨ C)) Proof (formal): (1) A → (A ∨ B) Add axiom 6 (2) A → (A ∨ (B ∨ C)) SubstPred B by B ∨ C in (1) (3) A → (A ∨ C) SubstPred B by C in (1) (4) B → (B ∨ C) SubstPred A by B in (3) (5) A → (B ∨ A) Add axiom 7 (6) A → (D ∨ A) SubstPred B by D in (5) (7) (B ∨ C) → (D ∨ (B ∨ C)) SubstPred A by B ∨ C in (6) (8) (B ∨ C) → (A ∨ (B ∨ C)) SubstPred D by A in (7) Conditional Proof (9) B Hypothesis (10) B ∨ C MP (4), (9) (11) A ∨ (B ∨ C) MP (8), (10) (12) B → (A ∨ (B ∨ C)) Conclusion (13) C → (B ∨ C) SubstPred A by C in (5) Conditional Proof (14) C Hypothesis (15) B ∨ C MP (13), (14) (16) A ∨ (B ∨ C) MP (8), (15) (17) C → (A ∨ (B ∨ C)) Conclusion (18) (A → C) → ((B → C) → ((A ∨ B) → C)) Add axiom 8 (19) (A → (A ∨ (B ∨ C))) → ((B → (A ∨ (B SubstPred C by A ∨ (B ∨ C) in (18) ∨ C))) → ((A ∨ B) → (A ∨ (B ∨ C)))) (20) (B → (A ∨ (B ∨ C))) → ((A ∨ B) → (A MP (19), (2) ∨ (B ∨ C))) (21) (A ∨ B) → (A ∨ (B ∨ C)) MP (20), (12) (22) (A → D) → ((B → D) → ((A ∨ B) → D)) SubstPred C by D in (18) (23) (A → D) → ((C → D) → ((A ∨ C) → D)) SubstPred B by C in (22) (24) ((A ∨ B) → D) → ((C → D) → (((A ∨ B) SubstPred A by A ∨ B in (23) ∨ C) → D)) (25) ((A ∨ B) → (A ∨ (B ∨ C))) → ((C → (A SubstPred D by A ∨ (B ∨ C) in (24) ∨ (B ∨ C))) → (((A ∨ B) ∨ C) → (A ∨ (B ∨ C)))) (26) (C → (A ∨ (B ∨ C))) → (((A ∨ B) ∨ C) MP (25), (21) → (A ∨ (B ∨ C))) (27) ((A ∨ B) ∨ C) → (A ∨ (B ∨ C)) MP (26), (17) q.e.d. ☉ Proposition 23 [proposition:implication42] (A → B) → ((A ∨ C) → (B ∨ C)) Proof (formal): (1) (A → C) → ((B → C) → ((A ∨ B) → C)) Add axiom 8 (2) (A → D) → ((B → D) → ((A ∨ B) → D)) SubstPred C by D in (1) (3) (A → D) → ((C → D) → ((A ∨ C) → D)) SubstPred B by C in (2) (4) (A → (B ∨ C)) → ((C → (B ∨ C)) → ((A SubstPred D by B ∨ C in (3) ∨ C) → (B ∨ C))) (5) A → (A ∨ B) Add axiom 6 (6) A → (A ∨ C) SubstPred B by C in (5) (7) B → (B ∨ C) SubstPred A by B in (6) (8) A → (B ∨ A) Add axiom 7 (9) C → (B ∨ C) SubstPred A by C in (8) Conditional Proof (10) A → B Hypothesis Conditional Proof (11) A Hypothesis (12) B MP (10), (11) (13) B ∨ C MP (7), (12) (14) A → (B ∨ C) Conclusion (15) (C → (B ∨ C)) → ((A ∨ C) → (B ∨ C) MP (4), (14) ) (16) (A ∨ C) → (B ∨ C) MP (15), (9) (17) (A → B) → ((A ∨ C) → (B ∨ C)) Conclusion q.e.d. 3.6 Propositions about negation ――――――――――――――――――――――――――――――― Now we look at negation. Here we must use the principle of the excluded middle for the first time. ☉ Proposition 24 [proposition:implication50] A → ¬ ¬ A Proof (formal): (1) A → (B → A) Add axiom 1 (2) A → (¬ A → A) SubstPred B by ¬ A in (1) (3) (A → B) → ((A → ¬ B) → ¬ A) Add axiom 9 (4) (¬ A → B) → ((¬ A → ¬ B) → ¬ ¬ A) SubstPred A by ¬ A in (3) (5) (¬ A → A) → ((¬ A → ¬ A) → ¬ ¬ A) SubstPred B by A in (4) (6) A → A Add proposition 1 (7) ¬ A → ¬ A SubstPred A by ¬ A in (6) Conditional Proof (8) A Hypothesis (9) ¬ A → A MP (2), (8) (10) (¬ A → ¬ A) → ¬ ¬ A MP (5), (9) (11) ¬ ¬ A MP (10), (7) (12) A → ¬ ¬ A Conclusion q.e.d. ☉ Proposition 25 [proposition:implication51] (A → ¬ B) → (B → ¬ A) Proof (formal): (1) A → (B → A) Add axiom 1 (2) C → (B → C) SubstPred A by C in (1) (3) C → (A → C) SubstPred B by A in (2) (4) B → (A → B) SubstPred C by B in (3) (5) (A → B) → ((A → ¬ B) → ¬ A) Add axiom 9 Conditional Proof (6) A → ¬ B Hypothesis Conditional Proof (7) B Hypothesis (8) A → B MP (4), (7) (9) (A → ¬ B) → ¬ A MP (5), (8) (10) ¬ A MP (9), (6) (11) B → ¬ A Conclusion (12) (A → ¬ B) → (B → ¬ A) Conclusion q.e.d. ☉ Proposition 26 [proposition:implication52] (A → B) → (¬ B → ¬ A) Proof (formal): (1) A → (B → A) Add axiom 1 (2) C → (B → C) SubstPred A by C in (1) (3) C → (A → C) SubstPred B by A in (2) (4) ¬ B → (A → ¬ B) SubstPred C by ¬ B in (3) (5) (A → B) → ((A → ¬ B) → ¬ A) Add axiom 9 Conditional Proof (6) A → B Hypothesis (7) (A → ¬ B) → ¬ A MP (5), (6) Conditional Proof (8) ¬ B Hypothesis (9) A → ¬ B MP (4), (8) (10) ¬ A MP (7), (9) (11) ¬ B → ¬ A Conclusion (12) (A → B) → (¬ B → ¬ A) Conclusion q.e.d. ☉ Proposition 27 [proposition:implication54] ¬ ¬ ¬ A → ¬ A Proof (formal): (1) A → ¬ ¬ A Add proposition 24 (2) (A → B) → (¬ B → ¬ A) Add proposition 26 (3) (A → ¬ ¬ A) → (¬ ¬ ¬ A → ¬ A) SubstPred B by ¬ ¬ A in (2) (4) ¬ ¬ ¬ A → ¬ A MP (3), (1) q.e.d. ☉ Proposition 28 [proposition:implication55] (¬ A → A) → ¬ ¬ A Proof (formal): (1) A → A Add proposition 1 (2) ¬ A → ¬ A SubstPred A by ¬ A in (1) (3) (A → B) → ((A → ¬ B) → ¬ A) Add axiom 9 (4) (¬ A → B) → ((¬ A → ¬ B) → ¬ ¬ A) SubstPred A by ¬ A in (3) (5) (¬ A → A) → ((¬ A → ¬ A) → ¬ ¬ A) SubstPred B by A in (4) Conditional Proof (6) ¬ A → A Hypothesis (7) (¬ A → ¬ A) → ¬ ¬ A MP (5), (6) (8) ¬ ¬ A MP (7), (2) (9) (¬ A → A) → ¬ ¬ A Conclusion q.e.d. ☉ Proposition 29 [proposition:implication56] ¬ ¬ A → A Proof (formal): (1) A ∨ ¬ A Add axiom 11 (2) (A → C) → ((B → C) → ((A ∨ B) → C)) Add axiom 8 (3) (A → A) → ((B → A) → ((A ∨ B) → A)) SubstPred C by A in (2) (4) A → A Add proposition 1 (5) (B → A) → ((A ∨ B) → A) MP (3), (4) (6) (¬ A → A) → ((A ∨ ¬ A) → A) SubstPred B by ¬ A in (5) (7) ¬ A → (A → B) Add axiom 10 (8) ¬ ¬ A → (¬ A → B) SubstPred A by ¬ A in (7) (9) ¬ ¬ A → (¬ A → A) SubstPred B by A in (8) Conditional Proof (10) ¬ ¬ A Hypothesis (11) ¬ A → A MP (9), (10) (12) (A ∨ ¬ A) → A MP (6), (11) (13) A MP (12), (1) (14) ¬ ¬ A → A Conclusion q.e.d. ☉ Proposition 30 [proposition:implication57] (¬ B → ¬ A) → (A → B) Proof (formal): (1) ¬ ¬ A → A Add proposition 29 (2) ¬ ¬ B → B SubstPred A by B in (1) (3) (A → ¬ B) → (B → ¬ A) Add proposition 25 (4) (C → ¬ B) → (B → ¬ C) SubstPred A by C in (3) (5) (C → ¬ A) → (A → ¬ C) SubstPred B by A in (4) (6) (¬ B → ¬ A) → (A → ¬ ¬ B) SubstPred C by ¬ B in (5) Conditional Proof (7) ¬ B → ¬ A Hypothesis (8) A → ¬ ¬ B MP (6), (7) Conditional Proof (9) A Hypothesis (10) ¬ ¬ B MP (8), (9) (11) B MP (2), (10) (12) A → B Conclusion (13) (¬ B → ¬ A) → (A → B) Conclusion q.e.d. 3.7 Mixing conjunction and disjunction. ――――――――――――――――――――――――――――――――――――――― Now we show how disjunction and conjunction are connected. ☉ Proposition 31 [proposition:implication70] ((A → C) ∧ (B → C)) → ((A ∨ B) → C) Proof (formal): (1) (A → (B → C)) → ((A ∧ B) → C) Add proposition 15 (2) (A → (B → D)) → ((A ∧ B) → D) SubstPred C by D in (1) (3) ((A → C) → (B → D)) → (((A → C) ∧ B) SubstPred A by A → C in (2) → D) (4) ((A → C) → ((B → C) → D)) → (((A → C SubstPred B by B → C in (3) ) ∧ (B → C)) → D) (5) ((A → C) → ((B → C) → ((A ∨ B) → C)) SubstPred D by (A ∨ B) → C in (4) ) → (((A → C) ∧ (B → C)) → ((A ∨ B) → C)) (6) (A → C) → ((B → C) → ((A ∨ B) → C)) Add axiom 8 (7) ((A → C) ∧ (B → C)) → ((A ∨ B) → C) MP (5), (6) q.e.d. ☉ Proposition 32 [proposition:implication71] ((A ∧ B) ∨ C) → ((A ∨ C) ∧ (B ∨ C)) Proof (formal): (1) B → (A → (A ∧ B)) Add axiom 5 (2) (B ∨ C) → (A → (A ∧ (B ∨ C))) SubstPred B by B ∨ C in (1) (3) (B ∨ C) → ((A ∨ C) → ((A ∨ C) ∧ (B ∨ SubstPred A by A ∨ C in (2) C))) (4) (A ∧ B) → A Add axiom 3 (5) (A → B) → ((A ∨ C) → (B ∨ C)) Add proposition 23 (6) (A → D) → ((A ∨ C) → (D ∨ C)) SubstPred B by D in (5) (7) ((A ∧ B) → D) → (((A ∧ B) ∨ C) → (D SubstPred A by A ∧ B in (6) ∨ C)) (8) ((A ∧ B) → A) → (((A ∧ B) ∨ C) → (A SubstPred D by A in (7) ∨ C)) (9) ((A ∧ B) ∨ C) → (A ∨ C) MP (8), (4) (10) (A ∧ B) → B Add axiom 4 (11) ((A ∧ B) → B) → (((A ∧ B) ∨ C) → (B SubstPred D by B in (7) ∨ C)) (12) ((A ∧ B) ∨ C) → (B ∨ C) MP (11), (10) Conditional Proof (13) (A ∧ B) ∨ C Hypothesis (14) A ∨ C MP (9), (13) (15) B ∨ C MP (12), (13) (16) (A ∨ C) → ((A ∨ C) ∧ (B ∨ C)) MP (3), (15) (17) (A ∨ C) ∧ (B ∨ C) MP (16), (14) (18) ((A ∧ B) ∨ C) → ((A ∨ C) ∧ (B ∨ C)) Conclusion q.e.d. ☉ Proposition 33 [proposition:implication72] ((A ∨ C) ∧ (B ∨ C)) → ((A ∧ B) ∨ C) Proof (formal): (1) A → (B ∨ A) Add axiom 7 (2) C → (B ∨ C) SubstPred A by C in (1) (3) C → ((A ∧ B) ∨ C) SubstPred B by A ∧ B in (2) (4) (A → C) → ((B → C) → ((A ∨ B) → C)) Add axiom 8 (5) (A → D) → ((B → D) → ((A ∨ B) → D)) SubstPred C by D in (4) (6) (A → D) → ((C → D) → ((A ∨ C) → D)) SubstPred B by C in (5) (7) (B → D) → ((C → D) → ((B ∨ C) → D)) SubstPred A by B in (6) (8) (B → ((A ∧ B) ∨ C)) → ((C → ((A ∧ B) SubstPred D by (A ∧ B) ∨ C in (7) ∨ C)) → ((B ∨ C) → ((A ∧ B) ∨ C))) Conditional Proof (9) C Hypothesis Conditional Proof (10) B Hypothesis (11) (A ∧ B) ∨ C MP (3), (9) (12) B → ((A ∧ B) ∨ C) Conclusion (13) (C → ((A ∧ B) ∨ C)) → ((B ∨ C) → ( MP (8), (12) (A ∧ B) ∨ C)) (14) (B ∨ C) → ((A ∧ B) ∨ C) MP (13), (3) (15) C → ((B ∨ C) → ((A ∧ B) ∨ C)) Conclusion (16) (A → B) → ((A ∨ C) → (B ∨ C)) Add proposition 23 (17) (D → B) → ((D ∨ C) → (B ∨ C)) SubstPred A by D in (16) (18) (D → (A ∧ B)) → ((D ∨ C) → ((A ∧ B) SubstPred B by A ∧ B in (17) ∨ C)) (19) (B → (A ∧ B)) → ((B ∨ C) → ((A ∧ B) SubstPred D by B in (18) ∨ C)) (20) A → (B → (A ∧ B)) Add proposition 10 Conditional Proof (21) A Hypothesis (22) B → (A ∧ B) MP (20), (21) (23) (B ∨ C) → ((A ∧ B) ∨ C) MP (19), (22) (24) A → ((B ∨ C) → ((A ∧ B) ∨ C)) Conclusion (25) (A → C) → ((B → C) → ((A ∨ B) → C)) Add axiom 8 (26) (A → D) → ((B → D) → ((A ∨ B) → D)) SubstPred C by D in (25) (27) (A → D) → ((C → D) → ((A ∨ C) → D)) SubstPred B by C in (26) (28) (A → ((B ∨ C) → ((A ∧ B) ∨ C))) → (( SubstPred D by (B ∨ C) → ((A ∧ B) ∨ C → ((B ∨ C) → ((A ∧ B) ∨ C))) → ((A C) in (27) ∨ C) → ((B ∨ C) → ((A ∧ B) ∨ C)))) (29) (C → ((B ∨ C) → ((A ∧ B) ∨ C))) → (( MP (28), (24) A ∨ C) → ((B ∨ C) → ((A ∧ B) ∨ C))) (30) (A ∨ C) → ((B ∨ C) → ((A ∧ B) ∨ C)) MP (29), (15) (31) (A → (B → C)) → ((A ∧ B) → C) Add proposition 15 (32) (A → (B → D)) → ((A ∧ B) → D) SubstPred C by D in (31) (33) ((A ∨ C) → (B → D)) → (((A ∨ C) ∧ B) SubstPred A by A ∨ C in (32) → D) (34) ((A ∨ C) → ((B ∨ C) → D)) → (((A ∨ C SubstPred B by B ∨ C in (33) ) ∧ (B ∨ C)) → D) (35) ((A ∨ C) → ((B ∨ C) → ((A ∧ B) ∨ C)) SubstPred D by (A ∧ B) ∨ C in (34) ) → (((A ∨ C) ∧ (B ∨ C)) → ((A ∧ B) ∨ C)) (36) ((A ∨ C) ∧ (B ∨ C)) → ((A ∧ B) ∨ C) MP (35), (30) q.e.d. ___________________________________________________ Bibliography ════════════ [novikov] P . S . N o v i k o v , Elements of Mathematical Logic, Edinburgh: Oliver and Boyd, 1964. [detnieks] V .  D e t l o v s , K .  P o d n i e k s , Introduction to Mathematical Logic, https://dspace.lu.lv/dspace/handle/7/1308 . [hilback] D .  H i l b e r t , W .  A c k e r m a n n , Grundzüge der theoretischen Logik, 2nd ed., Berlin: Springer, 1938. English version: Principles of Mathematical Logic, Chelsea, New York 1950, ed. by R. E. Luce. See also http://www.math.uwaterloo.ca/~snburris/htdocs/scav/hilbert/hilbert.html [mendelson] E .  M e n d e l s o n , Introduction to Mathematical Logic, 3rd. ed., Belmont, CA: Wadsworth, 1987. QEDEQ modules that use this one: qedeq_logic_v1 http://www.qedeq.org/0_04_07/doc/math/qedeq_logic_v1.xml