A Logical Approach to Discrete Math Ch.3¶
In [ ]:
// Load the Sylph package which contains the PropCalculus theory
// Run this cell first if there are any namespace errors when using this notebook.
#r "nuget: Sylph"
// Load helpers for the Jupyter .NET Core kernel.
#load "netcore.fsx"
In [3]:
open Sylvester
open PropCalculus
// Declare symbols we can reuse in formulae
let p,q,r = var3<bool>
In [38]:
// Theorem 3.2
let ``3.2`` = proof prop_calculus <@ p = p = q = q @> [
RightAssoc |> LR
def_true <@ q @> |> Trn |> R
Commute |> LR
]
[Lemma] true = (q = q):
⊢ true = (q = q). [Definition of true]
Proof complete.
[Lemma] q = q = true:
1. Logical operators in expression are commutative: q = q = true → true = (q = q).
⊢ true = (q = q). [Definition of true]
Proof complete.
Proof of p = p = q = q:
1. Logical operators in expression are right-associative: p = p = q = q → p = p = (q = q).
Proof incomplete. Current state: p = p = (q = q).
2. Substitute q = q ≡ true into right of expression.
Proof incomplete. Current state: p = p = true.
3. Logical operators in expression are commutative: p = p = true → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
In [5]:
// Theorem 3.4
let ``3.4`` = proof prop_calculus <@ true @> [
def_true <@ p @> |> LR
]
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
Proof of true:
1. Substitute true ≡ p = p into expression.
⊢ p = p. [Axiom of Symbolic Equality]
Proof complete.
In [6]:
// Theorem 3.5
let ``3.5`` = axiom prop_calculus <@ p = p @>
[Lemma] p = p:
⊢ p = p. [Axiom of Symbolic Equality]
Proof complete.
In [7]:
// Theorem 3.11
let ``3.11`` = proof prop_calculus <@ not p = q = p = not q @> [
Collect |> L
RightAssoc |> LR
Commute |> R
Collect |> R
Commute |> R
]
Proof of ¬ p = q = p = ¬ q: 1. Collect distributed logical terms in left of expression: ¬ p = q = p = ¬ q → ¬ (p = q) = p = ¬ q. Proof incomplete. Current state: ¬ (p = q) = p = ¬ q. 2. Logical operators in expression are right-associative: ¬ (p = q) = p = ¬ q → ¬ (p = q) = (p = ¬ q). Proof incomplete. Current state: ¬ (p = q) = (p = ¬ q). 3. Logical operators in right of expression are commutative: ¬ (p = q) = (p = ¬ q) → ¬ (p = q) = (¬ q = p). Proof incomplete. Current state: ¬ (p = q) = (¬ q = p). 4. Collect distributed logical terms in right of expression: ¬ (p = q) = (¬ q = p) → ¬ (p = q) = ¬ (q = p). Proof incomplete. Current state: ¬ (p = q) = ¬ (q = p). 5. Logical operators in right of expression are commutative: ¬ (p = q) = ¬ (q = p) → ¬ (p = q) = ¬ (p = q). ⊢ ¬ (p = q) = ¬ (p = q). [Axiom of Symbolic Equality] Proof complete.
In [8]:
// Theorem 3.12
let ``3.12`` = proof prop_calculus <@ not (not p) = p @> [
Collect |> LR
def_false <@ p @> |> Trn |> LR
not_false |> Truth |> LR
]
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] p = p = true:
1. Logical operators in expression are commutative: p = p = true → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] false = (¬ p = p):
1. Collect distributed logical terms in expression: false = (¬ p = p) → false = ¬ (p = p).
Proof incomplete. Current state: false = ¬ (p = p).
2. Substitute p = p ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] ¬ p = p = false:
1. Logical operators in expression are commutative: ¬ p = p = false → false = (¬ p = p).
Proof incomplete. Current state: false = (¬ p = p).
2. Collect distributed logical terms in expression: false = (¬ p = p) → false = ¬ (p = p).
Proof incomplete. Current state: false = ¬ (p = p).
3. Substitute p = p ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] true = true = true:
1. Logical operators in expression are commutative: true = true = true → true = (true = true).
⊢ true = (true = true). [Definition of true]
Proof complete.
[Lemma] ¬ false = (true = true):
1. Substitute true = true ≡ true into right of expression.
Proof incomplete. Current state: ¬ false = true.
2. Logical operators in expression are commutative: ¬ false = true → true = ¬ false.
Proof incomplete. Current state: true = ¬ false.
3. Substitute true ≡ false = false into left of expression.
Proof incomplete. Current state: false = false = ¬ false.
4. Logical operators in expression are right-associative: false = false = ¬ false → false = (false = ¬ false).
Proof incomplete. Current state: false = (false = ¬ false).
5. Logical operators in right of expression are commutative: false = (false = ¬ false) → false = (¬ false = false).
Proof incomplete. Current state: false = (¬ false = false).
6. Collect distributed logical terms in right of expression: false = (¬ false = false) → false = ¬ (false = false).
Proof incomplete. Current state: false = ¬ (false = false).
7. Substitute false = false ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
Proof of ¬ (¬ p) = p:
1. Collect distributed logical terms in expression: ¬ (¬ p) = p → ¬ (¬ p = p).
Proof incomplete. Current state: ¬ (¬ p = p).
2. Substitute ¬ p = p ≡ false into expression.
Proof incomplete. Current state: ¬ false.
3. Substitute ¬ false ≡ true = true into expression.
⊢ true = true. [Axiom of Symbolic Equality]
Proof complete.
In [9]:
// Theorem 3.13
let ``3.13``= proof prop_calculus <@not false = true@> [
Commute |> LR
def_true <@ false @> |> L
RightAssoc |> LR
Commute |> R
Collect |> R
def_true <@ false @> |> Trn |> R
]
[Lemma] true = (false = false):
⊢ true = (false = false). [Definition of true]
Proof complete.
[Lemma] true = (false = false):
⊢ true = (false = false). [Definition of true]
Proof complete.
[Lemma] false = false = true:
1. Logical operators in expression are commutative: false = false = true → true = (false = false).
⊢ true = (false = false). [Definition of true]
Proof complete.
Proof of ¬ false = true:
1. Logical operators in expression are commutative: ¬ false = true → true = ¬ false.
Proof incomplete. Current state: true = ¬ false.
2. Substitute true ≡ false = false into left of expression.
Proof incomplete. Current state: false = false = ¬ false.
3. Logical operators in expression are right-associative: false = false = ¬ false → false = (false = ¬ false).
Proof incomplete. Current state: false = (false = ¬ false).
4. Logical operators in right of expression are commutative: false = (false = ¬ false) → false = (¬ false = false).
Proof incomplete. Current state: false = (¬ false = false).
5. Collect distributed logical terms in right of expression: false = (¬ false = false) → false = ¬ (false = false).
Proof incomplete. Current state: false = ¬ (false = false).
6. Substitute false = false ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
In [10]:
// Theorem 3.14
let ``3.14`` = axiom prop_calculus <@ (p <> q) = not (p = q) @>
[Lemma] p <> q = ¬ (p = q):
⊢ p <> q = ¬ (p = q). [Definition of (<>)]
Proof complete.
In [11]:
// Theorem 3.15
let ``3.15`` = proof prop_calculus <@ not p = p = false@> [
Collect |> L
def_true <@ p @> |> Trn |> L
Commute |> LR
]
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] p = p = true:
1. Logical operators in expression are commutative: p = p = true → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
Proof of ¬ p = p = false:
1. Collect distributed logical terms in left of expression: ¬ p = p = false → ¬ (p = p) = false.
Proof incomplete. Current state: ¬ (p = p) = false.
2. Substitute p = p ≡ true into left of expression.
Proof incomplete. Current state: ¬ true = false.
3. Logical operators in expression are commutative: ¬ true = false → false = ¬ true.
⊢ false = ¬ true. [Definition of false]
Proof complete.
In [12]:
// Theorem 3.16
let ``3.16`` = proof prop_calculus <@ (p <> q) = (q <> p) @> [
def_not_eq <@ p @> <@ q @> |> L
def_not_eq <@ q @> <@ p @> |> R
Commute |> R
]
[Lemma] p <> q = ¬ (p = q):
⊢ p <> q = ¬ (p = q). [Definition of (<>)]
Proof complete.
[Lemma] q <> p = ¬ (q = p):
⊢ q <> p = ¬ (q = p). [Definition of (<>)]
Proof complete.
Proof of p <> q = (q <> p):
1. Substitute p <> q ≡ ¬ (p = q) into left of expression.
Proof incomplete. Current state: ¬ (p = q) = (q <> p).
2. Substitute q <> p ≡ ¬ (q = p) into right of expression.
Proof incomplete. Current state: ¬ (p = q) = ¬ (q = p).
3. Logical operators in right of expression are commutative: ¬ (p = q) = ¬ (q = p) → ¬ (p = q) = ¬ (p = q).
⊢ ¬ (p = q) = ¬ (p = q). [Axiom of Symbolic Equality]
Proof complete.
In [13]:
// Theorem 3.17
let ``3.17`` =
proof prop_calculus <@ ((p <> q) <> r) = (p <> (q <> r)) @> [
def_not_eq <@ p @> <@ q @> |> L
def_not_eq <@ not (p = q) @> <@ r @> |> L
def_not_eq <@ q @> <@ r @> |> R
def_not_eq <@ p @> <@ not (q = r) @> |> R
distrib_not <@ q @> <@ r @> |> R
LeftAssoc |> R
commute_eq <@ p @> <@ not q @> |> R
collect_not <@ q @> <@ p @> |> R
commute_eq <@ q @> <@ p @> |> R
]
[Lemma] p <> q = ¬ (p = q):
⊢ p <> q = ¬ (p = q). [Definition of (<>)]
Proof complete.
[Lemma] ¬ (p = q) <> r = ¬ (¬ (p = q) = r):
⊢ ¬ (p = q) <> r = ¬ (¬ (p = q) = r). [Definition of (<>)]
Proof complete.
[Lemma] q <> r = ¬ (q = r):
⊢ q <> r = ¬ (q = r). [Definition of (<>)]
Proof complete.
[Lemma] p <> ¬ (q = r) = ¬ (p = ¬ (q = r)):
⊢ p <> ¬ (q = r) = ¬ (p = ¬ (q = r)). [Definition of (<>)]
Proof complete.
[Lemma] ¬ (q = r) = (¬ q = r):
⊢ ¬ (q = r) = (¬ q = r). [Axiom of Distributivity]
Proof complete.
[Lemma] p = ¬ q = (¬ q = p):
1. Logical operators in expression are left-associative: p = ¬ q = (¬ q = p) → p = ¬ q = ¬ q = p.
⊢ p = ¬ q = ¬ q = p. [Axiom of Symmetry]
Proof complete.
[Lemma] ¬ (q = p) = (¬ q = p):
⊢ ¬ (q = p) = (¬ q = p). [Axiom of Distributivity]
Proof complete.
[Lemma] ¬ q = p = ¬ (q = p):
1. Logical operators in expression are commutative: ¬ q = p = ¬ (q = p) → ¬ (q = p) = (¬ q = p).
⊢ ¬ (q = p) = (¬ q = p). [Axiom of Distributivity]
Proof complete.
[Lemma] q = p = (p = q):
1. Logical operators in expression are left-associative: q = p = (p = q) → q = p = p = q.
⊢ q = p = p = q. [Axiom of Symmetry]
Proof complete.
Proof of p <> q <> r = (p <> (q <> r)):
1. Substitute p <> q ≡ ¬ (p = q) into left of expression.
Proof incomplete. Current state: ¬ (p = q) <> r = (p <> (q <> r)).
2. Substitute ¬ (p = q) <> r ≡ ¬ (¬ (p = q) = r) into left of expression.
Proof incomplete. Current state: ¬ (¬ (p = q) = r) = (p <> (q <> r)).
3. Substitute q <> r ≡ ¬ (q = r) into right of expression.
Proof incomplete. Current state: ¬ (¬ (p = q) = r) = (p <> ¬ (q = r)).
4. Substitute p <> ¬ (q = r) ≡ ¬ (p = ¬ (q = r)) into right of expression.
Proof incomplete. Current state: ¬ (¬ (p = q) = r) = ¬ (p = ¬ (q = r)).
5. Substitute ¬ (q = r) ≡ ¬ q = r into right of expression.
Proof incomplete. Current state: ¬ (¬ (p = q) = r) = ¬ (p = (¬ q = r)).
6. Logical operators in right of expression are left-associative: ¬ (¬ (p = q) = r) = ¬ (p = (¬ q = r)) → ¬ (¬ (p = q) = r) = ¬ (p = ¬ q = r).
Proof incomplete. Current state: ¬ (¬ (p = q) = r) = ¬ (p = ¬ q = r).
7. Substitute p = ¬ q ≡ ¬ q = p into right of expression.
Proof incomplete. Current state: ¬ (¬ (p = q) = r) = ¬ (¬ q = p = r).
8. Substitute ¬ q = p ≡ ¬ (q = p) into right of expression.
Proof incomplete. Current state: ¬ (¬ (p = q) = r) = ¬ (¬ (q = p) = r).
9. Substitute q = p ≡ p = q into right of expression.
⊢ ¬ (¬ (p = q) = r) = ¬ (¬ (p = q) = r). [Axiom of Symbolic Equality]
Proof complete.
In [14]:
// Theorem 3.29
let ``3.29`` = proof prop_calculus <@ p ||| true = true @> [
def_true <@ p @> |> LR
Distrib |> LR
Idemp |> LR
]
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
Proof of p ∨ true = true:
1. Substitute true ≡ p = p into expression.
Proof incomplete. Current state: p ∨ (p = p) = (p = p).
2. Distribute logical terms in expression: p ∨ (p = p) = (p = p) → p ∨ p = p ∨ p = (p = p).
Proof incomplete. Current state: p ∨ p = p ∨ p = (p = p).
3. Substitute idempotent logical terms in expression: p ∨ p = p ∨ p = (p = p) → p = p = (p = p).
⊢ p = p = (p = p). [Axiom of Symbolic Equality]
Proof complete.
In [15]:
// Theorem 3.30
let ``3.30`` = proof prop_calculus <@p ||| false = p @> [
def_false <@ p @> |> L
L Distrib
LR RightAssoc
R Idemp
L ExcludedMiddle
]
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] p = p = true:
1. Logical operators in expression are commutative: p = p = true → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] false = (¬ p = p):
1. Collect distributed logical terms in expression: false = (¬ p = p) → false = ¬ (p = p).
Proof incomplete. Current state: false = ¬ (p = p).
2. Substitute p = p ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
Proof of p ∨ false = p:
1. Substitute false ≡ ¬ p = p into left of expression.
Proof incomplete. Current state: p ∨ (¬ p = p) = p.
2. Distribute logical terms in left of expression: p ∨ (¬ p = p) = p → p ∨ ¬ p = p ∨ p = p.
Proof incomplete. Current state: p ∨ ¬ p = p ∨ p = p.
3. Logical operators in expression are right-associative: p ∨ ¬ p = p ∨ p = p → p ∨ ¬ p = (p ∨ p = p).
Proof incomplete. Current state: p ∨ ¬ p = (p ∨ p = p).
4. Substitute idempotent logical terms in right of expression: p ∨ ¬ p = (p ∨ p = p) → p ∨ ¬ p = (p = p).
Proof incomplete. Current state: p ∨ ¬ p = (p = p).
5. Logical terms in left of expression satisfy the law of excluded middle: p ∨ ¬ p = (p = p) → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
In [16]:
// Theorem 3.31
let ``3.31`` = proof prop_calculus <@ (p ||| (q ||| r)) = ((p ||| q) ||| (p ||| r)) @> [
commute_or_or <@ p @> <@ q @> <@ p @> <@ r @> |> R
idemp_or <@ p @> |> R
]
[Lemma] p ∨ q ∨ (p ∨ r) = p ∨ q ∨ p ∨ r:
1. Logical operators in expression are left-associative: p ∨ q ∨ (p ∨ r) = p ∨ q ∨ p ∨ r → p ∨ q ∨ p ∨ r = p ∨ q ∨ p ∨ r.
⊢ p ∨ q ∨ p ∨ r = p ∨ q ∨ p ∨ r. [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p ∨ (q ∨ p) = p ∨ q ∨ p:
1. Logical operators in expression are left-associative: p ∨ (q ∨ p) = p ∨ q ∨ p → p ∨ q ∨ p = p ∨ q ∨ p.
⊢ p ∨ q ∨ p = p ∨ q ∨ p. [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p ∨ q ∨ p = p ∨ (q ∨ p):
⊢ p ∨ q ∨ p = p ∨ (q ∨ p). [Axiom of Associativity]
Proof complete.
[Lemma] q ∨ p = p ∨ q:
⊢ q ∨ p = p ∨ q. [Axiom of Commutativity]
Proof complete.
[Lemma] p ∨ q ∨ (p ∨ r) = p ∨ p ∨ (q ∨ r):
1. Substitute p ∨ q ∨ (p ∨ r) ≡ p ∨ q ∨ p ∨ r into left of expression.
Proof incomplete. Current state: p ∨ q ∨ p ∨ r = p ∨ p ∨ (q ∨ r).
2. Substitute p ∨ q ∨ p ≡ p ∨ (q ∨ p) into left of expression.
Proof incomplete. Current state: p ∨ (q ∨ p) ∨ r = p ∨ p ∨ (q ∨ r).
3. Substitute q ∨ p ≡ p ∨ q into left of expression.
Proof incomplete. Current state: p ∨ (p ∨ q) ∨ r = p ∨ p ∨ (q ∨ r).
4. Logical operators in left of expression are left-associative: p ∨ (p ∨ q) ∨ r = p ∨ p ∨ (q ∨ r) → p ∨ p ∨ q ∨ r = p ∨ p ∨ (q ∨ r).
⊢ p ∨ p ∨ q ∨ r = p ∨ p ∨ (q ∨ r). [Axiom of Associativity]
Proof complete.
[Lemma] p ∨ p = p:
⊢ p ∨ p = p. [Axiom of Idempotency]
Proof complete.
Proof of p ∨ (q ∨ r) = p ∨ q ∨ (p ∨ r):
1. Substitute p ∨ q ∨ (p ∨ r) ≡ p ∨ p ∨ (q ∨ r) into right of expression.
Proof incomplete. Current state: p ∨ (q ∨ r) = p ∨ p ∨ (q ∨ r).
2. Substitute p ∨ p ≡ p into right of expression.
⊢ p ∨ (q ∨ r) = p ∨ (q ∨ r). [Axiom of Symbolic Equality]
Proof complete.
In [17]:
let ``3.32`` = proof prop_calculus <@ (p ||| q) = (p ||| not q = p) @> [
LeftAssoc |> LR
collect_or_eq <@ p @> <@ q @> <@ not q @> |> LR
commute_eq <@ q @> <@ not q @> |> L
def_false <@ q @> |> Trn |> L
ident_or <@ p @> |> L
]
[Lemma] p ∨ (q = ¬ q) = (p ∨ q = p ∨ ¬ q):
⊢ p ∨ (q = ¬ q) = (p ∨ q = p ∨ ¬ q). [Axiom of Distributivity]
Proof complete.
[Lemma] p ∨ q = p ∨ ¬ q = p ∨ (q = ¬ q):
1. Logical operators in expression are commutative: p ∨ q = p ∨ ¬ q = p ∨ (q = ¬ q) → p ∨ (q = ¬ q) = (p ∨ q = p ∨ ¬ q).
⊢ p ∨ (q = ¬ q) = (p ∨ q = p ∨ ¬ q). [Axiom of Distributivity]
Proof complete.
[Lemma] q = ¬ q = (¬ q = q):
1. Logical operators in expression are left-associative: q = ¬ q = (¬ q = q) → q = ¬ q = ¬ q = q.
⊢ q = ¬ q = ¬ q = q. [Axiom of Symmetry]
Proof complete.
[Lemma] true = (q = q):
⊢ true = (q = q). [Definition of true]
Proof complete.
[Lemma] q = q = true:
1. Logical operators in expression are commutative: q = q = true → true = (q = q).
⊢ true = (q = q). [Definition of true]
Proof complete.
[Lemma] false = (¬ q = q):
1. Collect distributed logical terms in expression: false = (¬ q = q) → false = ¬ (q = q).
Proof incomplete. Current state: false = ¬ (q = q).
2. Substitute q = q ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] ¬ q = q = false:
1. Logical operators in expression are commutative: ¬ q = q = false → false = (¬ q = q).
Proof incomplete. Current state: false = (¬ q = q).
2. Collect distributed logical terms in expression: false = (¬ q = q) → false = ¬ (q = q).
Proof incomplete. Current state: false = ¬ (q = q).
3. Substitute q = q ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] p = p = true:
1. Logical operators in expression are commutative: p = p = true → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] false = (¬ p = p):
1. Collect distributed logical terms in expression: false = (¬ p = p) → false = ¬ (p = p).
Proof incomplete. Current state: false = ¬ (p = p).
2. Substitute p = p ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] p ∨ false = p:
1. Substitute false ≡ ¬ p = p into expression.
Proof incomplete. Current state: p ∨ (¬ p = p) = p.
2. Distribute logical terms in left of expression: p ∨ (¬ p = p) = p → p ∨ ¬ p = p ∨ p = p.
Proof incomplete. Current state: p ∨ ¬ p = p ∨ p = p.
3. Logical operators in expression are right-associative: p ∨ ¬ p = p ∨ p = p → p ∨ ¬ p = (p ∨ p = p).
Proof incomplete. Current state: p ∨ ¬ p = (p ∨ p = p).
4. Substitute idempotent logical terms in right of expression: p ∨ ¬ p = (p ∨ p = p) → p ∨ ¬ p = (p = p).
Proof incomplete. Current state: p ∨ ¬ p = (p = p).
5. Substitute true ≡ p = p into expression: No change.
Proof incomplete. Current state: p ∨ ¬ p = (p = p).
6. Logical terms in left of expression satisfy the law of excluded middle: p ∨ ¬ p = (p = p) → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
Proof of p ∨ q = (p ∨ ¬ q = p):
1. Logical operators in expression are left-associative: p ∨ q = (p ∨ ¬ q = p) → p ∨ q = p ∨ ¬ q = p.
Proof incomplete. Current state: p ∨ q = p ∨ ¬ q = p.
2. Substitute p ∨ q = p ∨ ¬ q ≡ p ∨ (q = ¬ q) into expression.
Proof incomplete. Current state: p ∨ (q = ¬ q) = p.
3. Substitute q = ¬ q ≡ ¬ q = q into left of expression.
Proof incomplete. Current state: p ∨ (¬ q = q) = p.
4. Substitute ¬ q = q ≡ false into left of expression.
Proof incomplete. Current state: p ∨ false = p.
5. Substitute p ∨ false ≡ p into left of expression.
⊢ p = p. [Axiom of Symbolic Equality]
Proof complete.
In [18]:
let ``3.37`` = proof prop_calculus <@ (p |&| q |&| r) = (p |&| (q |&| r)) @> [
golden_rule <@ p @> <@ q @> |> L
golden_rule <@ (p = q) = (p ||| q) @> <@ r @> |> L
commute_or <@ ((p = q) = (p ||| q)) @> <@ r @> |> L
distrib_or_eq <@ r @> <@ p = q @> <@ p ||| q @> |> L
distrib_or_eq <@ r @> <@ p @> <@ q @> |> L
right_assoc_eq <@ p = q@> <@ p ||| q@> <@ r @> |> L
commute_eq <@ p ||| q @> <@ r @> |> L
commute_or <@ r @> <@ q @> |> L
commute_eq <@ r ||| p@> <@ q ||| r@> |> L
commute_or <@ r @> <@ p ||| q @> |> L
L LeftAssoc
L LeftAssoc
L LeftAssoc
commute_and <@ p @> <@ q |&| r @> |> R
ident_and_eq_all <@ q @> <@ r @> <@ p @> |> R
commute_eq <@q = r@> <@ p @> |> R
]
[Lemma] p ∧ q = (p = q = p ∨ q):
⊢ p ∧ q = (p = q = p ∨ q). [Axiom of the Golden Rule]
Proof complete.
[Lemma] p = q = p ∨ q ∧ r = (p = q = p ∨ q = r = (p = q = p ∨ q) ∨ r):
⊢ p = q = p ∨ q ∧ r = (p = q = p ∨ q = r = (p = q = p ∨ q) ∨ r). [Axiom of the Golden Rule]
Proof complete.
[Lemma] (p = q = p ∨ q) ∨ r = r ∨ (p = q = p ∨ q):
⊢ (p = q = p ∨ q) ∨ r = r ∨ (p = q = p ∨ q). [Axiom of Commutativity]
Proof complete.
[Lemma] r ∨ (p = q = p ∨ q) = (r ∨ (p = q) = r ∨ (p ∨ q)):
⊢ r ∨ (p = q = p ∨ q) = (r ∨ (p = q) = r ∨ (p ∨ q)). [Axiom of Distributivity]
Proof complete.
[Lemma] r ∨ (p = q) = (r ∨ p = r ∨ q):
⊢ r ∨ (p = q) = (r ∨ p = r ∨ q). [Axiom of Distributivity]
Proof complete.
[Lemma] p = q = (p ∨ q = r) = (p = q = p ∨ q = r):
1. Logical operators in right of expression are right-associative: p = q = (p ∨ q = r) = (p = q = p ∨ q = r) → p = q = (p ∨ q = r) = (p = q = (p ∨ q = r)).
⊢ p = q = (p ∨ q = r) = (p = q = (p ∨ q = r)). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p = q = p ∨ q = r = (p = q = (p ∨ q = r)):
⊢ p = q = p ∨ q = r = (p = q = (p ∨ q = r)). [Axiom of Associativity]
Proof complete.
[Lemma] p ∨ q = r = (r = p ∨ q):
1. Logical operators in expression are left-associative: p ∨ q = r = (r = p ∨ q) → p ∨ q = r = r = p ∨ q.
⊢ p ∨ q = r = r = p ∨ q. [Axiom of Symmetry]
Proof complete.
[Lemma] r ∨ q = q ∨ r:
⊢ r ∨ q = q ∨ r. [Axiom of Commutativity]
Proof complete.
[Lemma] r ∨ p = q ∨ r = (q ∨ r = r ∨ p):
1. Logical operators in expression are left-associative: r ∨ p = q ∨ r = (q ∨ r = r ∨ p) → r ∨ p = q ∨ r = q ∨ r = r ∨ p.
⊢ r ∨ p = q ∨ r = q ∨ r = r ∨ p. [Axiom of Symmetry]
Proof complete.
[Lemma] r ∨ (p ∨ q) = p ∨ q ∨ r:
⊢ r ∨ (p ∨ q) = p ∨ q ∨ r. [Axiom of Commutativity]
Proof complete.
[Lemma] (q ∧ r) ∨ p = p ∨ (q ∧ r):
⊢ (q ∧ r) ∨ p = p ∨ (q ∧ r). [Axiom of Commutativity]
Proof complete.
[Lemma] q ∧ r = p = (p = (q ∧ r)):
1. Logical operators in expression are left-associative: q ∧ r = p = (p = (q ∧ r)) → q ∧ r = p = p = (q ∧ r).
⊢ q ∧ r = p = p = (q ∧ r). [Axiom of Symmetry]
Proof complete.
[Lemma] p ∧ (q ∧ r) = (q ∧ r ∧ p):
1. Logical terms in expression satisfy the golden rule: p ∧ (q ∧ r) = (q ∧ r ∧ p) → p = (q ∧ r) = p ∨ (q ∧ r) = (q ∧ r = p = (q ∧ r) ∨ p).
Proof incomplete. Current state: p = (q ∧ r) = p ∨ (q ∧ r) = (q ∧ r = p = (q ∧ r) ∨ p).
2. Substitute (q ∧ r) ∨ p ≡ p ∨ (q ∧ r) into right of expression.
Proof incomplete. Current state: p = (q ∧ r) = p ∨ (q ∧ r) = (q ∧ r = p = p ∨ (q ∧ r)).
3. Substitute q ∧ r = p ≡ p = (q ∧ r) into right of expression.
⊢ p = (q ∧ r) = p ∨ (q ∧ r) = (p = (q ∧ r) = p ∨ (q ∧ r)). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] q ∧ r = (q = r = q ∨ r):
⊢ q ∧ r = (q = r = q ∨ r). [Axiom of the Golden Rule]
Proof complete.
[Lemma] q = r = q ∨ r ∧ p = (q = r = q ∨ r = p = (q = r = q ∨ r) ∨ p):
⊢ q = r = q ∨ r ∧ p = (q = r = q ∨ r = p = (q = r = q ∨ r) ∨ p). [Axiom of the Golden Rule]
Proof complete.
[Lemma] (q = r = q ∨ r) ∨ p = p ∨ (q = r = q ∨ r):
⊢ (q = r = q ∨ r) ∨ p = p ∨ (q = r = q ∨ r). [Axiom of Commutativity]
Proof complete.
[Lemma] p ∨ (q = r = q ∨ r) = (p ∨ (q = r) = p ∨ (q ∨ r)):
⊢ p ∨ (q = r = q ∨ r) = (p ∨ (q = r) = p ∨ (q ∨ r)). [Axiom of Distributivity]
Proof complete.
[Lemma] p ∨ (q = r) = (p ∨ q = p ∨ r):
⊢ p ∨ (q = r) = (p ∨ q = p ∨ r). [Axiom of Distributivity]
Proof complete.
[Lemma] q = r = (q ∨ r = p) = (q = r = q ∨ r = p):
1. Logical operators in right of expression are right-associative: q = r = (q ∨ r = p) = (q = r = q ∨ r = p) → q = r = (q ∨ r = p) = (q = r = (q ∨ r = p)).
⊢ q = r = (q ∨ r = p) = (q = r = (q ∨ r = p)). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] q = r = q ∨ r = p = (q = r = (q ∨ r = p)):
⊢ q = r = q ∨ r = p = (q = r = (q ∨ r = p)). [Axiom of Associativity]
Proof complete.
[Lemma] q ∨ r = p = (p = q ∨ r):
1. Logical operators in expression are left-associative: q ∨ r = p = (p = q ∨ r) → q ∨ r = p = p = q ∨ r.
⊢ q ∨ r = p = p = q ∨ r. [Axiom of Symmetry]
Proof complete.
[Lemma] p ∨ r = r ∨ p:
⊢ p ∨ r = r ∨ p. [Axiom of Commutativity]
Proof complete.
[Lemma] p ∨ q = r ∨ p = (r ∨ p = p ∨ q):
1. Logical operators in expression are left-associative: p ∨ q = r ∨ p = (r ∨ p = p ∨ q) → p ∨ q = r ∨ p = r ∨ p = p ∨ q.
⊢ p ∨ q = r ∨ p = r ∨ p = p ∨ q. [Axiom of Symmetry]
Proof complete.
[Lemma] p ∨ (q ∨ r) = q ∨ r ∨ p:
⊢ p ∨ (q ∨ r) = q ∨ r ∨ p. [Axiom of Commutativity]
Proof complete.
[Lemma] q ∧ r ∧ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p):
1. Substitute q ∧ r ≡ q = r = q ∨ r into left of expression.
Proof incomplete. Current state: q = r = q ∨ r ∧ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
2. Substitute q = r = q ∨ r ∧ p ≡ q = r = q ∨ r = p = (q = r = q ∨ r) ∨ p into left of expression.
Proof incomplete. Current state: q = r = q ∨ r = p = (q = r = q ∨ r) ∨ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
3. Substitute (q = r = q ∨ r) ∨ p ≡ p ∨ (q = r = q ∨ r) into left of expression.
Proof incomplete. Current state: q = r = q ∨ r = p = p ∨ (q = r = q ∨ r) = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
4. Substitute p ∨ (q = r = q ∨ r) ≡ p ∨ (q = r) = p ∨ (q ∨ r) into left of expression.
Proof incomplete. Current state: q = r = q ∨ r = p = (p ∨ (q = r) = p ∨ (q ∨ r)) = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
5. Substitute p ∨ (q = r) ≡ p ∨ q = p ∨ r into left of expression.
Proof incomplete. Current state: q = r = q ∨ r = p = (p ∨ q = p ∨ r = p ∨ (q ∨ r)) = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
6. Substitute q = r = q ∨ r = p ≡ q = r = (q ∨ r = p) into left of expression.
Proof incomplete. Current state: q = r = (q ∨ r = p) = (p ∨ q = p ∨ r = p ∨ (q ∨ r)) = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
7. Substitute q ∨ r = p ≡ p = q ∨ r into left of expression.
Proof incomplete. Current state: q = r = (p = q ∨ r) = (p ∨ q = p ∨ r = p ∨ (q ∨ r)) = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
8. Substitute p ∨ r ≡ r ∨ p into left of expression.
Proof incomplete. Current state: q = r = (p = q ∨ r) = (p ∨ q = r ∨ p = p ∨ (q ∨ r)) = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
9. Substitute p ∨ q = r ∨ p ≡ r ∨ p = p ∨ q into left of expression.
Proof incomplete. Current state: q = r = (p = q ∨ r) = (r ∨ p = p ∨ q = p ∨ (q ∨ r)) = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
10. Substitute p ∨ (q ∨ r) ≡ q ∨ r ∨ p into left of expression.
Proof incomplete. Current state: q = r = (p = q ∨ r) = (r ∨ p = p ∨ q = q ∨ r ∨ p) = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
11. Logical operators in left of expression are left-associative: q = r = (p = q ∨ r) = (r ∨ p = p ∨ q = q ∨ r ∨ p) = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p) → q = r = (p = q ∨ r) = (r ∨ p = p ∨ q) = q ∨ r ∨ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
Proof incomplete. Current state: q = r = (p = q ∨ r) = (r ∨ p = p ∨ q) = q ∨ r ∨ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
12. Logical operators in left of expression are left-associative: q = r = (p = q ∨ r) = (r ∨ p = p ∨ q) = q ∨ r ∨ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p) → q = r = (p = q ∨ r) = r ∨ p = p ∨ q = q ∨ r ∨ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
Proof incomplete. Current state: q = r = (p = q ∨ r) = r ∨ p = p ∨ q = q ∨ r ∨ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
13. Logical operators in left of expression are left-associative: q = r = (p = q ∨ r) = r ∨ p = p ∨ q = q ∨ r ∨ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p) → q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
⊢ q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] q = r = p = (p = (q = r)):
1. Logical operators in expression are left-associative: q = r = p = (p = (q = r)) → q = r = p = p = (q = r).
⊢ q = r = p = p = (q = r). [Axiom of Symmetry]
Proof complete.
Proof of p ∧ q ∧ r = (p ∧ (q ∧ r)):
1. Substitute p ∧ q ≡ p = q = p ∨ q into left of expression.
Proof incomplete. Current state: p = q = p ∨ q ∧ r = (p ∧ (q ∧ r)).
2. Substitute p = q = p ∨ q ∧ r ≡ p = q = p ∨ q = r = (p = q = p ∨ q) ∨ r into left of expression.
Proof incomplete. Current state: p = q = p ∨ q = r = (p = q = p ∨ q) ∨ r = (p ∧ (q ∧ r)).
3. Substitute (p = q = p ∨ q) ∨ r ≡ r ∨ (p = q = p ∨ q) into left of expression.
Proof incomplete. Current state: p = q = p ∨ q = r = r ∨ (p = q = p ∨ q) = (p ∧ (q ∧ r)).
4. Substitute r ∨ (p = q = p ∨ q) ≡ r ∨ (p = q) = r ∨ (p ∨ q) into left of expression.
Proof incomplete. Current state: p = q = p ∨ q = r = (r ∨ (p = q) = r ∨ (p ∨ q)) = (p ∧ (q ∧ r)).
5. Substitute r ∨ (p = q) ≡ r ∨ p = r ∨ q into left of expression.
Proof incomplete. Current state: p = q = p ∨ q = r = (r ∨ p = r ∨ q = r ∨ (p ∨ q)) = (p ∧ (q ∧ r)).
6. Substitute p = q = p ∨ q = r ≡ p = q = (p ∨ q = r) into left of expression.
Proof incomplete. Current state: p = q = (p ∨ q = r) = (r ∨ p = r ∨ q = r ∨ (p ∨ q)) = (p ∧ (q ∧ r)).
7. Substitute p ∨ q = r ≡ r = p ∨ q into left of expression.
Proof incomplete. Current state: p = q = (r = p ∨ q) = (r ∨ p = r ∨ q = r ∨ (p ∨ q)) = (p ∧ (q ∧ r)).
8. Substitute r ∨ q ≡ q ∨ r into left of expression.
Proof incomplete. Current state: p = q = (r = p ∨ q) = (r ∨ p = q ∨ r = r ∨ (p ∨ q)) = (p ∧ (q ∧ r)).
9. Substitute r ∨ p = q ∨ r ≡ q ∨ r = r ∨ p into left of expression.
Proof incomplete. Current state: p = q = (r = p ∨ q) = (q ∨ r = r ∨ p = r ∨ (p ∨ q)) = (p ∧ (q ∧ r)).
10. Substitute r ∨ (p ∨ q) ≡ p ∨ q ∨ r into left of expression.
Proof incomplete. Current state: p = q = (r = p ∨ q) = (q ∨ r = r ∨ p = p ∨ q ∨ r) = (p ∧ (q ∧ r)).
11. Logical operators in left of expression are left-associative: p = q = (r = p ∨ q) = (q ∨ r = r ∨ p = p ∨ q ∨ r) = (p ∧ (q ∧ r)) → p = q = (r = p ∨ q) = (q ∨ r = r ∨ p) = p ∨ q ∨ r = (p ∧ (q ∧ r)).
Proof incomplete. Current state: p = q = (r = p ∨ q) = (q ∨ r = r ∨ p) = p ∨ q ∨ r = (p ∧ (q ∧ r)).
12. Logical operators in left of expression are left-associative: p = q = (r = p ∨ q) = (q ∨ r = r ∨ p) = p ∨ q ∨ r = (p ∧ (q ∧ r)) → p = q = (r = p ∨ q) = q ∨ r = r ∨ p = p ∨ q ∨ r = (p ∧ (q ∧ r)).
Proof incomplete. Current state: p = q = (r = p ∨ q) = q ∨ r = r ∨ p = p ∨ q ∨ r = (p ∧ (q ∧ r)).
13. Logical operators in left of expression are left-associative: p = q = (r = p ∨ q) = q ∨ r = r ∨ p = p ∨ q ∨ r = (p ∧ (q ∧ r)) → p = q = r = p ∨ q = q ∨ r = r ∨ p = p ∨ q ∨ r = (p ∧ (q ∧ r)).
Proof incomplete. Current state: p = q = r = p ∨ q = q ∨ r = r ∨ p = p ∨ q ∨ r = (p ∧ (q ∧ r)).
14. Substitute p ∧ (q ∧ r) ≡ q ∧ r ∧ p into right of expression.
Proof incomplete. Current state: p = q = r = p ∨ q = q ∨ r = r ∨ p = p ∨ q ∨ r = (q ∧ r ∧ p).
15. Substitute q ∧ r ∧ p ≡ q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p into right of expression.
Proof incomplete. Current state: p = q = r = p ∨ q = q ∨ r = r ∨ p = p ∨ q ∨ r = (q = r = p = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
16. Substitute q = r = p ≡ p = (q = r) into right of expression.
Proof incomplete. Current state: p = q = r = p ∨ q = q ∨ r = r ∨ p = p ∨ q ∨ r = (p = (q = r) = q ∨ r = r ∨ p = p ∨ q = q ∨ r ∨ p).
In [19]:
let ``3.38`` = proof prop_calculus <@ (p |&| p) = p @> [
LR GoldenRule
RightAssoc |> LR
idemp_or <@ p @> |> Taut |> R
LR Commute
]
[Lemma] p ∨ p = p:
⊢ p ∨ p = p. [Axiom of Idempotency]
Proof complete.
[Lemma] p ∨ p = p = true = (p ∨ p = p):
1. Logical operators in left of expression are commutative: p ∨ p = p = true = (p ∨ p = p) → true = (p ∨ p = p) = (p ∨ p = p).
Proof incomplete. Current state: true = (p ∨ p = p) = (p ∨ p = p).
2. Logical operators in expression are right-associative: true = (p ∨ p = p) = (p ∨ p = p) → true = (p ∨ p = p = (p ∨ p = p)).
⊢ true = (p ∨ p = p = (p ∨ p = p)). [Definition of true]
Proof complete.
[Lemma] p ∨ p = p = true:
1. Substitute p ∨ p = p = true ≡ p ∨ p = p into expression.
⊢ p ∨ p = p. [Axiom of Idempotency]
Proof complete.
Proof of p ∧ p = p:
1. Logical terms in expression satisfy the golden rule: p ∧ p = p → p = p = p ∨ p = p.
Proof incomplete. Current state: p = p = p ∨ p = p.
2. Logical operators in expression are right-associative: p = p = p ∨ p = p → p = p = (p ∨ p = p).
Proof incomplete. Current state: p = p = (p ∨ p = p).
3. Substitute p ∨ p = p ≡ true into right of expression.
Proof incomplete. Current state: p = p = true.
4. Logical operators in expression are commutative: p = p = true → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
In [20]:
let ``3.39`` = proof prop_calculus <@ (p |&| true) = p @> [
LR GoldenRule
LR RightAssoc
zero_or <@ p @> |> R
R Commute
]
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] p ∨ true = true:
1. Substitute true ≡ p = p into expression.
Proof incomplete. Current state: p ∨ (p = p) = (p = p).
2. Distribute logical terms in expression: p ∨ (p = p) = (p = p) → p ∨ p = p ∨ p = (p = p).
Proof incomplete. Current state: p ∨ p = p ∨ p = (p = p).
3. Substitute idempotent logical terms in expression: p ∨ p = p ∨ p = (p = p) → p = p = (p = p).
⊢ p = p = (p = p). [Axiom of Symbolic Equality]
Proof complete.
Proof of p ∧ true = p:
1. Logical terms in expression satisfy the golden rule: p ∧ true = p → p = true = p ∨ true = p.
Proof incomplete. Current state: p = true = p ∨ true = p.
2. Logical operators in expression are right-associative: p = true = p ∨ true = p → p = true = (p ∨ true = p).
Proof incomplete. Current state: p = true = (p ∨ true = p).
3. Substitute p ∨ true ≡ true into right of expression.
Proof incomplete. Current state: p = true = (true = p).
4. Logical operators in right of expression are commutative: p = true = (true = p) → p = true = (p = true).
⊢ p = true = (p = true). [Axiom of Symbolic Equality]
Proof complete.
In [21]:
let ``3.40`` = proof prop_calculus <@ (p |&| false) = false @> [
LR GoldenRule
ident_or <@ p @> |> L
LR RightAssoc
]
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] p = p = true:
1. Logical operators in expression are commutative: p = p = true → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] false = (¬ p = p):
1. Collect distributed logical terms in expression: false = (¬ p = p) → false = ¬ (p = p).
Proof incomplete. Current state: false = ¬ (p = p).
2. Substitute p = p ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] p ∨ false = p:
1. Substitute false ≡ ¬ p = p into expression.
Proof incomplete. Current state: p ∨ (¬ p = p) = p.
2. Distribute logical terms in left of expression: p ∨ (¬ p = p) = p → p ∨ ¬ p = p ∨ p = p.
Proof incomplete. Current state: p ∨ ¬ p = p ∨ p = p.
3. Logical operators in expression are right-associative: p ∨ ¬ p = p ∨ p = p → p ∨ ¬ p = (p ∨ p = p).
Proof incomplete. Current state: p ∨ ¬ p = (p ∨ p = p).
4. Substitute idempotent logical terms in right of expression: p ∨ ¬ p = (p ∨ p = p) → p ∨ ¬ p = (p = p).
Proof incomplete. Current state: p ∨ ¬ p = (p = p).
5. Substitute true ≡ p = p into expression: No change.
Proof incomplete. Current state: p ∨ ¬ p = (p = p).
6. Logical terms in left of expression satisfy the law of excluded middle: p ∨ ¬ p = (p = p) → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
Proof of p ∧ false = false:
1. Logical terms in expression satisfy the golden rule: p ∧ false = false → p = false = p ∨ false = false.
Proof incomplete. Current state: p = false = p ∨ false = false.
2. Substitute p ∨ false ≡ p into left of expression.
Proof incomplete. Current state: p = false = p = false.
3. Logical operators in expression are right-associative: p = false = p = false → p = false = (p = false).
⊢ p = false = (p = false). [Axiom of Symbolic Equality]
Proof complete.
In [22]:
// Theorem 3.41
let ``3.41`` = proof prop_calculus <@ (p |&| (q |&| r)) = ((p |&| q) |&| (p |&| r)) @> [
LeftAssoc |> R
right_assoc_and <@ p @> <@ q @> <@ p @> |> R
commute_and <@ q @> <@ p @> |> R
LeftAssoc |> R
idemp_and <@ p @> |> R
LeftAssoc |> L
]
[Lemma] p ∧ q = (p = q = p ∨ q):
⊢ p ∧ q = (p = q = p ∨ q). [Axiom of the Golden Rule]
Proof complete.
[Lemma] PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q ∧ p = (PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q = p = (PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q) ∨ p):
⊢ PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q ∧ p = (PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q = p = (PropertyGet (None, p, []) = PropertyGet (None, q, []) = p ∨ q) ∨ p). [Axiom of the Golden Rule]
Proof complete.
[Lemma] (p = q = p ∨ q) ∨ p = p ∨ (p = q = p ∨ q):
⊢ (p = q = p ∨ q) ∨ p = p ∨ (p = q = p ∨ q). [Axiom of Commutativity]
Proof complete.
[Lemma] p ∨ (p = q = p ∨ q) = (p ∨ (p = q) = p ∨ (p ∨ q)):
⊢ p ∨ (p = q = p ∨ q) = (p ∨ (p = q) = p ∨ (p ∨ q)). [Axiom of Distributivity]
Proof complete.
[Lemma] p ∨ (p = q) = (p ∨ p = p ∨ q):
⊢ p ∨ (p = q) = (p ∨ p = p ∨ q). [Axiom of Distributivity]
Proof complete.
[Lemma] p = q = (p ∨ q = p) = (p = q = p ∨ q = p):
1. Logical operators in right of expression are right-associative: p = q = (p ∨ q = p) = (p = q = p ∨ q = p) → p = q = (p ∨ q = p) = (p = q = (p ∨ q = p)).
⊢ p = q = (p ∨ q = p) = (p = q = (p ∨ q = p)). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p = q = p ∨ q = p = (p = q = (p ∨ q = p)):
⊢ p = q = p ∨ q = p = (p = q = (p ∨ q = p)). [Axiom of Associativity]
Proof complete.
[Lemma] p ∨ q = p = (p = p ∨ q):
1. Logical operators in expression are left-associative: p ∨ q = p = (p = p ∨ q) → p ∨ q = p = p = p ∨ q.
⊢ p ∨ q = p = p = p ∨ q. [Axiom of Symmetry]
Proof complete.
[Lemma] p ∨ q = q ∨ p:
⊢ p ∨ q = q ∨ p. [Axiom of Commutativity]
Proof complete.
[Lemma] p ∨ p = q ∨ p = (q ∨ p = p ∨ p):
1. Logical operators in expression are left-associative: p ∨ p = q ∨ p = (q ∨ p = p ∨ p) → p ∨ p = q ∨ p = q ∨ p = p ∨ p.
⊢ p ∨ p = q ∨ p = q ∨ p = p ∨ p. [Axiom of Symmetry]
Proof complete.
[Lemma] p ∨ (p ∨ q) = p ∨ q ∨ p:
⊢ p ∨ (p ∨ q) = p ∨ q ∨ p. [Axiom of Commutativity]
Proof complete.
[Lemma] (q ∧ p) ∨ p = p ∨ (q ∧ p):
⊢ (q ∧ p) ∨ p = p ∨ (q ∧ p). [Axiom of Commutativity]
Proof complete.
[Lemma] q ∧ p = p = (p = (q ∧ p)):
1. Logical operators in expression are left-associative: q ∧ p = p = (p = (q ∧ p)) → q ∧ p = p = p = (q ∧ p).
⊢ q ∧ p = p = p = (q ∧ p). [Axiom of Symmetry]
Proof complete.
[Lemma] p ∧ (q ∧ p) = (q ∧ p ∧ p):
1. Logical terms in expression satisfy the golden rule: p ∧ (q ∧ p) = (q ∧ p ∧ p) → p = (q ∧ p) = p ∨ (q ∧ p) = (q ∧ p = p = (q ∧ p) ∨ p).
Proof incomplete. Current state: p = (q ∧ p) = p ∨ (q ∧ p) = (q ∧ p = p = (q ∧ p) ∨ p).
2. Substitute (q ∧ p) ∨ p ≡ p ∨ (q ∧ p) into right of expression.
Proof incomplete. Current state: p = (q ∧ p) = p ∨ (q ∧ p) = (q ∧ p = p = p ∨ (q ∧ p)).
3. Substitute q ∧ p = p ≡ p = (q ∧ p) into right of expression.
⊢ p = (q ∧ p) = p ∨ (q ∧ p) = (p = (q ∧ p) = p ∨ (q ∧ p)). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] q ∧ p = (q = p = q ∨ p):
⊢ q ∧ p = (q = p = q ∨ p). [Axiom of the Golden Rule]
Proof complete.
[Lemma] q = p = q ∨ p ∧ p = (q = p = q ∨ p = p = (q = p = q ∨ p) ∨ p):
⊢ q = p = q ∨ p ∧ p = (q = p = q ∨ p = p = (q = p = q ∨ p) ∨ p). [Axiom of the Golden Rule]
Proof complete.
[Lemma] (q = p = q ∨ p) ∨ p = p ∨ (q = p = q ∨ p):
⊢ (q = p = q ∨ p) ∨ p = p ∨ (q = p = q ∨ p). [Axiom of Commutativity]
Proof complete.
[Lemma] p ∨ (q = p = q ∨ p) = (p ∨ (q = p) = p ∨ (q ∨ p)):
⊢ p ∨ (q = p = q ∨ p) = (p ∨ (q = p) = p ∨ (q ∨ p)). [Axiom of Distributivity]
Proof complete.
[Lemma] p ∨ (q = p) = (p ∨ q = p ∨ p):
⊢ p ∨ (q = p) = (p ∨ q = p ∨ p). [Axiom of Distributivity]
Proof complete.
[Lemma] q = p = (q ∨ p = p) = (q = p = q ∨ p = p):
1. Logical operators in right of expression are right-associative: q = p = (q ∨ p = p) = (q = p = q ∨ p = p) → q = p = (q ∨ p = p) = (q = p = (q ∨ p = p)).
⊢ q = p = (q ∨ p = p) = (q = p = (q ∨ p = p)). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] q = p = q ∨ p = p = (q = p = (q ∨ p = p)):
⊢ q = p = q ∨ p = p = (q = p = (q ∨ p = p)). [Axiom of Associativity]
Proof complete.
[Lemma] q ∨ p = p = (p = q ∨ p):
1. Logical operators in expression are left-associative: q ∨ p = p = (p = q ∨ p) → q ∨ p = p = p = q ∨ p.
⊢ q ∨ p = p = p = q ∨ p. [Axiom of Symmetry]
Proof complete.
[Lemma] p ∨ p = p ∨ p:
⊢ p ∨ p = p ∨ p. [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p ∨ q = p ∨ p = (p ∨ p = p ∨ q):
1. Logical operators in expression are left-associative: p ∨ q = p ∨ p = (p ∨ p = p ∨ q) → p ∨ q = p ∨ p = p ∨ p = p ∨ q.
⊢ p ∨ q = p ∨ p = p ∨ p = p ∨ q. [Axiom of Symmetry]
Proof complete.
[Lemma] p ∨ (q ∨ p) = q ∨ p ∨ p:
⊢ p ∨ (q ∨ p) = q ∨ p ∨ p. [Axiom of Commutativity]
Proof complete.
[Lemma] q ∧ p ∧ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p):
1. Substitute q ∧ p ≡ q = p = q ∨ p into left of expression.
Proof incomplete. Current state: q = p = q ∨ p ∧ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
2. Substitute q = p = q ∨ p ∧ p ≡ q = p = q ∨ p = p = (q = p = q ∨ p) ∨ p into left of expression.
Proof incomplete. Current state: q = p = q ∨ p = p = (q = p = q ∨ p) ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
3. Substitute (q = p = q ∨ p) ∨ p ≡ p ∨ (q = p = q ∨ p) into left of expression.
Proof incomplete. Current state: q = p = q ∨ p = p = p ∨ (q = p = q ∨ p) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
4. Substitute p ∨ (q = p = q ∨ p) ≡ p ∨ (q = p) = p ∨ (q ∨ p) into left of expression.
Proof incomplete. Current state: q = p = q ∨ p = p = (p ∨ (q = p) = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
5. Substitute p ∨ (q = p) ≡ p ∨ q = p ∨ p into left of expression.
Proof incomplete. Current state: q = p = q ∨ p = p = (p ∨ q = p ∨ p = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
6. Substitute q = p = q ∨ p = p ≡ q = p = (q ∨ p = p) into left of expression.
Proof incomplete. Current state: q = p = (q ∨ p = p) = (p ∨ q = p ∨ p = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
7. Substitute q ∨ p = p ≡ p = q ∨ p into left of expression.
Proof incomplete. Current state: q = p = (p = q ∨ p) = (p ∨ q = p ∨ p = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
8. Substitute p ∨ p ≡ p ∨ p into expression: No change.
Proof incomplete. Current state: q = p = (p = q ∨ p) = (p ∨ q = p ∨ p = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
9. Substitute p ∨ q = p ∨ p ≡ p ∨ p = p ∨ q into left of expression.
Proof incomplete. Current state: q = p = (p = q ∨ p) = (p ∨ p = p ∨ q = p ∨ (q ∨ p)) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
10. Substitute p ∨ (q ∨ p) ≡ q ∨ p ∨ p into left of expression.
Proof incomplete. Current state: q = p = (p = q ∨ p) = (p ∨ p = p ∨ q = q ∨ p ∨ p) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
11. Logical operators in left of expression are left-associative: q = p = (p = q ∨ p) = (p ∨ p = p ∨ q = q ∨ p ∨ p) = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p) → q = p = (p = q ∨ p) = (p ∨ p = p ∨ q) = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
Proof incomplete. Current state: q = p = (p = q ∨ p) = (p ∨ p = p ∨ q) = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
12. Logical operators in left of expression are left-associative: q = p = (p = q ∨ p) = (p ∨ p = p ∨ q) = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p) → q = p = (p = q ∨ p) = p ∨ p = p ∨ q = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
Proof incomplete. Current state: q = p = (p = q ∨ p) = p ∨ p = p ∨ q = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
13. Logical operators in left of expression are left-associative: q = p = (p = q ∨ p) = p ∨ p = p ∨ q = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p) → q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p).
⊢ q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p = (q = p = p = q ∨ p = p ∨ p = p ∨ q = q ∨ p ∨ p). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] q = p = p = (p = (q = p)):
1. Logical operators in expression are left-associative: q = p = p = (p = (q = p)) → q = p = p = p = (q = p).
⊢ q = p = p = p = (q = p). [Axiom of Symmetry]
Proof complete.
[Lemma] p = (q = p) = (p = q = p):
1. Logical operators in right of expression are right-associative: p = (q = p) = (p = q = p) → p = (q = p) = (p = (q = p)).
⊢ p = (q = p) = (p = (q = p)). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] q ∨ p ∨ p = p ∨ (q ∨ p):
⊢ q ∨ p ∨ p = p ∨ (q ∨ p). [Axiom of Commutativity]
Proof complete.
[Lemma] p ∨ (q ∨ p) = p ∨ q ∨ p:
1. Logical operators in expression are left-associative: p ∨ (q ∨ p) = p ∨ q ∨ p → p ∨ q ∨ p = p ∨ q ∨ p.
⊢ p ∨ q ∨ p = p ∨ q ∨ p. [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p = q = p = (q ∨ p = p ∨ p) = (p = q = p = q ∨ p = p ∨ p):
1. Logical operators in right of expression are right-associative: p = q = p = (q ∨ p = p ∨ p) = (p = q = p = q ∨ p = p ∨ p) → p = q = p = (q ∨ p = p ∨ p) = (p = q = p = (q ∨ p = p ∨ p)).
⊢ p = q = p = (q ∨ p = p ∨ p) = (p = q = p = (q ∨ p = p ∨ p)). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p = q = p = q ∨ p = p ∨ p = (p = q = p = (q ∨ p = p ∨ p)):
⊢ p = q = p = q ∨ p = p ∨ p = (p = q = p = (q ∨ p = p ∨ p)). [Axiom of Associativity]
Proof complete.
[Lemma] p = q = p = q ∨ p = (p ∨ p = p ∨ q) = (p = q = p = q ∨ p = p ∨ p = p ∨ q):
1. Logical operators in right of expression are right-associative: p = q = p = q ∨ p = (p ∨ p = p ∨ q) = (p = q = p = q ∨ p = p ∨ p = p ∨ q) → p = q = p = q ∨ p = (p ∨ p = p ∨ q) = (p = q = p = q ∨ p = (p ∨ p = p ∨ q)).
⊢ p = q = p = q ∨ p = (p ∨ p = p ∨ q) = (p = q = p = q ∨ p = (p ∨ p = p ∨ q)). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p = q = p = q ∨ p = p ∨ p = p ∨ q = (p = q = p = q ∨ p = (p ∨ p = p ∨ q)):
⊢ p = q = p = q ∨ p = p ∨ p = p ∨ q = (p = q = p = q ∨ p = (p ∨ p = p ∨ q)). [Axiom of Associativity]
Proof complete.
[Lemma] p ∨ p = p ∨ q = (p ∨ q = p ∨ p):
1. Logical operators in expression are left-associative: p ∨ p = p ∨ q = (p ∨ q = p ∨ p) → p ∨ p = p ∨ q = p ∨ q = p ∨ p.
⊢ p ∨ p = p ∨ q = p ∨ q = p ∨ p. [Axiom of Symmetry]
Proof complete.
[Lemma] p = q = p = (q ∨ p = p ∨ q) = (p = q = p = q ∨ p = p ∨ q):
1. Logical operators in right of expression are right-associative: p = q = p = (q ∨ p = p ∨ q) = (p = q = p = q ∨ p = p ∨ q) → p = q = p = (q ∨ p = p ∨ q) = (p = q = p = (q ∨ p = p ∨ q)).
⊢ p = q = p = (q ∨ p = p ∨ q) = (p = q = p = (q ∨ p = p ∨ q)). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p = q = p = q ∨ p = p ∨ q = (p = q = p = (q ∨ p = p ∨ q)):
⊢ p = q = p = q ∨ p = p ∨ q = (p = q = p = (q ∨ p = p ∨ q)). [Axiom of Associativity]
Proof complete.
[Lemma] q ∨ p = p ∨ q = (p ∨ q = q ∨ p):
1. Logical operators in expression are left-associative: q ∨ p = p ∨ q = (p ∨ q = q ∨ p) → q ∨ p = p ∨ q = p ∨ q = q ∨ p.
⊢ q ∨ p = p ∨ q = p ∨ q = q ∨ p. [Axiom of Symmetry]
Proof complete.
Unhandled Exception The expression p |&| q |&| p = p |&| (q |&| p) is not an identity at Microsoft.FSharp.Core.PrintfModule.PrintFormatToStringThenFail@1637.Invoke(String message) in F:\workspace.1\_work\1\s\src\fsharp\FSharp.Core\printf.fs:line 1637 at Sylvester.ProofModule.ident[t](Theory theory, FSharpExpr`1 e, FSharpList`1 steps) at Sylvester.PropCalculus.right_assoc_and(FSharpExpr`1 p, FSharpExpr`1 q, FSharpExpr`1 r) at <StartupCode$FSI_0027>.$FSI_0027.main@()
In [23]:
let ``3.42`` = proof prop_calculus <@p |&| not p = false@> [
GoldenRule |> L
ExcludedMiddle |> L
commute_eq <@ p @> <@ not p @> |> L
def_false <@ p @> |> Trn |> L
commute_eq <@ false @> <@ true @> |> L
RightAssoc |> LR
]
[Lemma] p = ¬ p = (¬ p = p):
1. Logical operators in expression are left-associative: p = ¬ p = (¬ p = p) → p = ¬ p = ¬ p = p.
⊢ p = ¬ p = ¬ p = p. [Axiom of Symmetry]
Proof complete.
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] p = p = true:
1. Logical operators in expression are commutative: p = p = true → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] false = (¬ p = p):
1. Collect distributed logical terms in expression: false = (¬ p = p) → false = ¬ (p = p).
Proof incomplete. Current state: false = ¬ (p = p).
2. Substitute p = p ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] ¬ p = p = false:
1. Logical operators in expression are commutative: ¬ p = p = false → false = (¬ p = p).
Proof incomplete. Current state: false = (¬ p = p).
2. Collect distributed logical terms in expression: false = (¬ p = p) → false = ¬ (p = p).
Proof incomplete. Current state: false = ¬ (p = p).
3. Substitute p = p ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] false = true = (true = false):
1. Logical operators in expression are left-associative: false = true = (true = false) → false = true = true = false.
⊢ false = true = true = false. [Axiom of Symmetry]
Proof complete.
Proof of p ∧ ¬ p = false:
1. Logical terms in left of expression satisfy the golden rule: p ∧ ¬ p = false → p = ¬ p = p ∨ ¬ p = false.
Proof incomplete. Current state: p = ¬ p = p ∨ ¬ p = false.
2. Logical terms in left of expression satisfy the law of excluded middle: p = ¬ p = p ∨ ¬ p = false → p = ¬ p = true = false.
Proof incomplete. Current state: p = ¬ p = true = false.
3. Substitute p = ¬ p ≡ ¬ p = p into left of expression.
Proof incomplete. Current state: ¬ p = p = true = false.
4. Substitute ¬ p = p ≡ false into left of expression.
Proof incomplete. Current state: false = true = false.
5. Substitute false = true ≡ true = false into left of expression.
Proof incomplete. Current state: true = false = false.
6. Logical operators in expression are right-associative: true = false = false → true = (false = false).
⊢ true = (false = false). [Definition of true]
Proof complete.
In [24]:
let ``3.43a`` = proof prop_calculus <@ (p |&| (p ||| q)) = p @> [
GoldenRule |> L
left_assoc_or <@ p @> <@ p @> <@ q @> |> L
idemp_or <@ p @> |> L
]
[Lemma] p ∨ (p ∨ q) = p ∨ p ∨ q:
1. Logical operators in expression are left-associative: p ∨ (p ∨ q) = p ∨ p ∨ q → p ∨ p ∨ q = p ∨ p ∨ q.
⊢ p ∨ p ∨ q = p ∨ p ∨ q. [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p ∨ p = p:
⊢ p ∨ p = p. [Axiom of Idempotency]
Proof complete.
Proof of p ∧ p ∨ q = p:
1. Logical terms in left of expression satisfy the golden rule: p ∧ p ∨ q = p → p = p ∨ q = p ∨ (p ∨ q) = p.
Proof incomplete. Current state: p = p ∨ q = p ∨ (p ∨ q) = p.
2. Substitute p ∨ (p ∨ q) ≡ p ∨ p ∨ q into left of expression.
Proof incomplete. Current state: p = p ∨ q = p ∨ p ∨ q = p.
3. Substitute p ∨ p ≡ p into left of expression.
⊢ p = p ∨ q = p ∨ q = p. [Axiom of Symmetry]
Proof complete.
In [25]:
let ``3.43b`` = proof prop_calculus <@ (p ||| (p |&| q)) = p @> [
GoldenRule |> L
Distrib |> L
left_assoc_or <@ p @> <@ p @> <@ q @> |> L
idemp_or <@ p @> |> L
Distrib |> L
idemp_or <@ p @> |> L
]
[Lemma] p ∨ (p ∨ q) = p ∨ p ∨ q:
1. Logical operators in expression are left-associative: p ∨ (p ∨ q) = p ∨ p ∨ q → p ∨ p ∨ q = p ∨ p ∨ q.
⊢ p ∨ p ∨ q = p ∨ p ∨ q. [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p ∨ p = p:
⊢ p ∨ p = p. [Axiom of Idempotency]
Proof complete.
[Lemma] p ∨ p = p:
⊢ p ∨ p = p. [Axiom of Idempotency]
Proof complete.
Proof of p ∨ (p ∧ q) = p:
1. Logical terms in left of expression satisfy the golden rule: p ∨ (p ∧ q) = p → p ∨ (p = q = p ∨ q) = p.
Proof incomplete. Current state: p ∨ (p = q = p ∨ q) = p.
2. Distribute logical terms in left of expression: p ∨ (p = q = p ∨ q) = p → p ∨ (p = q) = p ∨ (p ∨ q) = p.
Proof incomplete. Current state: p ∨ (p = q) = p ∨ (p ∨ q) = p.
3. Substitute p ∨ (p ∨ q) ≡ p ∨ p ∨ q into left of expression.
Proof incomplete. Current state: p ∨ (p = q) = p ∨ p ∨ q = p.
4. Substitute p ∨ p ≡ p into left of expression.
Proof incomplete. Current state: p ∨ (p = q) = p ∨ q = p.
5. Distribute logical terms in left of expression: p ∨ (p = q) = p ∨ q = p → p ∨ p = p ∨ q = p ∨ q = p.
Proof incomplete. Current state: p ∨ p = p ∨ q = p ∨ q = p.
6. Substitute p ∨ p ≡ p into left of expression.
⊢ p = p ∨ q = p ∨ q = p. [Axiom of Symmetry]
Proof complete.
In [37]:
let ``3.44a`` = proof prop_calculus <@ p |&| (not p ||| q) = (p |&| q) @> [
GoldenRule |> L
left_assoc_or <@ p @> <@ not p @> <@ q @> |> L
ExcludedMiddle |> L
zero_or <@ q @> |> TrnL |> L
ident_eq <@ p = (not p ||| q) @> |> L
commute_or <@ not p@> <@ q @> |> L
ident_or_not_or <@ q @> <@ p @> |> L
LeftAssoc |> L
commute_or <@ q @> <@ p @> |> L
golden_rule <@ p @> <@ q @> |> Trn |> L
]
[Lemma] p ∨ (¬ p ∨ q) = p ∨ ¬ p ∨ q:
1. Logical operators in expression are left-associative: p ∨ (¬ p ∨ q) = p ∨ ¬ p ∨ q → p ∨ ¬ p ∨ q = p ∨ ¬ p ∨ q.
⊢ p ∨ ¬ p ∨ q = p ∨ ¬ p ∨ q. [Axiom of Symbolic Equality]
Proof complete.
[Lemma] true = (q = q):
⊢ true = (q = q). [Definition of true]
Proof complete.
[Lemma] q ∨ true = true:
1. Substitute true ≡ q = q into expression.
Proof incomplete. Current state: q ∨ (q = q) = (q = q).
2. Distribute logical terms in expression: q ∨ (q = q) = (q = q) → q ∨ q = q ∨ q = (q = q).
Proof incomplete. Current state: q ∨ q = q ∨ q = (q = q).
3. Substitute idempotent logical terms in expression: q ∨ q = q ∨ q = (q = q) → q = q = (q = q).
⊢ q = q = (q = q). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] true ∨ q = true:
1. Logical operators in left of expression are commutative: true ∨ q = true → q ∨ true = true.
Proof incomplete. Current state: q ∨ true = true.
2. Substitute true ≡ q = q into expression.
Proof incomplete. Current state: q ∨ (q = q) = (q = q).
3. Distribute logical terms in expression: q ∨ (q = q) = (q = q) → q ∨ q = q ∨ q = (q = q).
Proof incomplete. Current state: q ∨ q = q ∨ q = (q = q).
4. Substitute idempotent logical terms in expression: q ∨ q = q ∨ q = (q = q) → q = q = (q = q).
⊢ q = q = (q = q). [Axiom of Symbolic Equality]
Proof complete.
[Lemma] p = ¬ p ∨ q = true = (p = ¬ p ∨ q):
1. Logical operators in left of expression are commutative: p = ¬ p ∨ q = true = (p = ¬ p ∨ q) → true = (p = ¬ p ∨ q) = (p = ¬ p ∨ q).
Proof incomplete. Current state: true = (p = ¬ p ∨ q) = (p = ¬ p ∨ q).
2. Logical operators in expression are right-associative: true = (p = ¬ p ∨ q) = (p = ¬ p ∨ q) → true = (p = ¬ p ∨ q = (p = ¬ p ∨ q)).
⊢ true = (p = ¬ p ∨ q = (p = ¬ p ∨ q)). [Definition of true]
Proof complete.
[Lemma] ¬ p ∨ q = q ∨ ¬ p:
⊢ ¬ p ∨ q = q ∨ ¬ p. [Axiom of Commutativity]
Proof complete.
[Lemma] q ∨ (¬ p = p) = (q ∨ ¬ p = q ∨ p):
⊢ q ∨ (¬ p = p) = (q ∨ ¬ p = q ∨ p). [Axiom of Distributivity]
Proof complete.
[Lemma] q ∨ ¬ p = q ∨ p = q ∨ (¬ p = p):
1. Logical operators in expression are commutative: q ∨ ¬ p = q ∨ p = q ∨ (¬ p = p) → q ∨ (¬ p = p) = (q ∨ ¬ p = q ∨ p).
⊢ q ∨ (¬ p = p) = (q ∨ ¬ p = q ∨ p). [Axiom of Distributivity]
Proof complete.
[Lemma] true = (p = p):
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] p = p = true:
1. Logical operators in expression are commutative: p = p = true → true = (p = p).
⊢ true = (p = p). [Definition of true]
Proof complete.
[Lemma] false = (¬ p = p):
1. Collect distributed logical terms in expression: false = (¬ p = p) → false = ¬ (p = p).
Proof incomplete. Current state: false = ¬ (p = p).
2. Substitute p = p ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] ¬ p = p = false:
1. Logical operators in expression are commutative: ¬ p = p = false → false = (¬ p = p).
Proof incomplete. Current state: false = (¬ p = p).
2. Collect distributed logical terms in expression: false = (¬ p = p) → false = ¬ (p = p).
Proof incomplete. Current state: false = ¬ (p = p).
3. Substitute p = p ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] true = (q = q):
⊢ true = (q = q). [Definition of true]
Proof complete.
[Lemma] q = q = true:
1. Logical operators in expression are commutative: q = q = true → true = (q = q).
⊢ true = (q = q). [Definition of true]
Proof complete.
[Lemma] false = (¬ q = q):
1. Collect distributed logical terms in expression: false = (¬ q = q) → false = ¬ (q = q).
Proof incomplete. Current state: false = ¬ (q = q).
2. Substitute q = q ≡ true into right of expression.
⊢ false = ¬ true. [Definition of false]
Proof complete.
[Lemma] true = (q = q):
⊢ true = (q = q). [Definition of true]
Proof complete.
[Lemma] q ∨ false = q:
1. Substitute false ≡ ¬ q = q into expression.
Proof incomplete. Current state: q ∨ (¬ q = q) = q.
2. Distribute logical terms in left of expression: q ∨ (¬ q = q) = q → q ∨ ¬ q = q ∨ q = q.
Proof incomplete. Current state: q ∨ ¬ q = q ∨ q = q.
3. Logical operators in expression are right-associative: q ∨ ¬ q = q ∨ q = q → q ∨ ¬ q = (q ∨ q = q).
Proof incomplete. Current state: q ∨ ¬ q = (q ∨ q = q).
4. Substitute idempotent logical terms in right of expression: q ∨ ¬ q = (q ∨ q = q) → q ∨ ¬ q = (q = q).
Proof incomplete. Current state: q ∨ ¬ q = (q = q).
5. Substitute true ≡ q = q into expression: No change.
Proof incomplete. Current state: q ∨ ¬ q = (q = q).
6. Logical terms in left of expression satisfy the law of excluded middle: q ∨ ¬ q = (q = q) → true = (q = q).
⊢ true = (q = q). [Definition of true]
Proof complete.
[Lemma] q ∨ ¬ p = (q = q ∨ p):
1. Logical operators in right of expression are commutative: q ∨ ¬ p = (q = q ∨ p) → q ∨ ¬ p = (q ∨ p = q).
Proof incomplete. Current state: q ∨ ¬ p = (q ∨ p = q).
2. Logical operators in expression are left-associative: q ∨ ¬ p = (q ∨ p = q) → q ∨ ¬ p = q ∨ p = q.
Proof incomplete. Current state: q ∨ ¬ p = q ∨ p = q.
3. Substitute q ∨ ¬ p = q ∨ p ≡ q ∨ (¬ p = p) into left of expression.
Proof incomplete. Current state: q ∨ (¬ p = p) = q.
4. Substitute ¬ p = p ≡ false into left of expression.
Proof incomplete. Current state: q ∨ false = q.
5. Substitute q ∨ false ≡ q into left of expression.
⊢ q = q. [Axiom of Symbolic Equality]
Proof complete.
[Lemma] q ∨ p = p ∨ q:
⊢ q ∨ p = p ∨ q. [Axiom of Commutativity]
Proof complete.
[Lemma] p ∧ q = (p = q = p ∨ q):
⊢ p ∧ q = (p = q = p ∨ q). [Axiom of the Golden Rule]
Proof complete.
[Lemma] p = q = p ∨ q = (p ∧ q):
1. Logical operators in expression are commutative: p = q = p ∨ q = (p ∧ q) → p ∧ q = (p = q = p ∨ q).
⊢ p ∧ q = (p = q = p ∨ q). [Axiom of the Golden Rule]
Proof complete.
Proof of p ∧ ¬ p ∨ q = (p ∧ q):
1. Logical terms in left of expression satisfy the golden rule: p ∧ ¬ p ∨ q = (p ∧ q) → p = ¬ p ∨ q = p ∨ (¬ p ∨ q) = (p ∧ q).
Proof incomplete. Current state: p = ¬ p ∨ q = p ∨ (¬ p ∨ q) = (p ∧ q).
2. Substitute p ∨ (¬ p ∨ q) ≡ p ∨ ¬ p ∨ q into left of expression.
Proof incomplete. Current state: p = ¬ p ∨ q = p ∨ ¬ p ∨ q = (p ∧ q).
3. Logical terms in left of expression satisfy the law of excluded middle: p = ¬ p ∨ q = p ∨ ¬ p ∨ q = (p ∧ q) → p = ¬ p ∨ q = true ∨ q = (p ∧ q).
Proof incomplete. Current state: p = ¬ p ∨ q = true ∨ q = (p ∧ q).
4. Substitute true ∨ q ≡ true into left of expression.
Proof incomplete. Current state: p = ¬ p ∨ q = true = (p ∧ q).
5. Substitute p = ¬ p ∨ q = true ≡ p = ¬ p ∨ q into left of expression.
Proof incomplete. Current state: p = ¬ p ∨ q = (p ∧ q).
6. Substitute ¬ p ∨ q ≡ q ∨ ¬ p into left of expression.
Proof incomplete. Current state: p = q ∨ ¬ p = (p ∧ q).
7. Substitute q ∨ ¬ p ≡ q = q ∨ p into left of expression.
Proof incomplete. Current state: p = (q = q ∨ p) = (p ∧ q).
8. Logical operators in left of expression are left-associative: p = (q = q ∨ p) = (p ∧ q) → p = q = q ∨ p = (p ∧ q).
Proof incomplete. Current state: p = q = q ∨ p = (p ∧ q).
9. Substitute q ∨ p ≡ p ∨ q into left of expression.
Proof incomplete. Current state: p = q = p ∨ q = (p ∧ q).
10. Substitute p = q = p ∨ q ≡ p ∧ q into left of expression.
⊢ p ∧ q = (p ∧ q). [Axiom of Symbolic Equality]
Proof complete.