Introduction

@plaivy/logic is an interactive way to write proofs using formal rules of inference.

It supports propositional logic, first-order (predicate) logic, and first-order logic with equality.

Usage

To begin, run:

$ npx @plaivy/logic

You will see > appear below, indicating that the interface is waiting for user input. You can start by entering your premises/suppositions:

> suppose (P implies Q)
   1 ┌ (P → Q)    Supp
> supp not (not P or Q)
   1 ┌ (P → Q)        Supp
   2 │ ┌ ¬(¬P ∨ Q)    Supp

Here, suppose and supp mean the same thing. Other synonyms are supposition, presume, premise, and premiss.

You can leave out suppose etc. and just write the wff, in which case it will be interpreted as a supposition:

> (P->Q)
   1 ┌ (P → Q)    Supp

The interface understands many ways of expressing the same inference rules. Commas and many keywords are optional: write them if you find it helpful.

To end a subproof, enter end.

...
   1 ┌ (P → Q)        Supp
   2 │ ┌ ¬(¬P ∨ Q)    Supp
> end
   1 ┌ (P → Q)        Supp
   2 │ ┌ ¬(¬P ∨ Q)    Supp
   3 │

Entering end at the top level of a proof will exit the interface.

To undo a line, enter undo:

...
   1 ┌ (P → Q)        Supp
   2 │ ┌ ¬(¬P ∨ Q)    Supp
> undo
   1 ┌ (P → Q)    Supp

To undo everything, enter clear:

...
   1 ┌ (P → Q)        Supp
   2 │ ┌ ¬(¬P ∨ Q)    Supp
> clear
>

If a command violates the rules of inference, the interface will display an error message.

...
   1 ┌ P    Supp
   2
> raa 1
Subproof from line 1 does not end with ⊥ (P).

To reiterate (repeat) a previous line, enter the line number:

> suppose (if P then Q)
   1 ┌ (P → Q)    Supp
> 1
   1 ┌ (P → Q)    Supp
   2 │ (P → Q)    Iter 1

Well-Formed Formulas (Wffs)

Propositions

A predicate starts with an uppercase letter and can contain uppercase letters, digits, and underscores (_).

> P
   1 ┌ P    Supp
> clear
> LOVE
   1 ┌ LOVE    Supp

Predicates may take objects. An object starts with a lowercase letter, and its remainder can contain digits and underscores (_).

> Pa
   1 ┌ Pa    Supp
> clear
> LOVESab
   1 ┌ LOVESab    Supp
> clear
> TRIOa0a1a2
   1 ┌ TRIOa0a1a2    Supp

Conjunctions (∧)

> (P and Q)
   1 ┌ (P ∧ Q)    Supp

and and & are synonyms.

Disjunctions (∨)

> (P or Q)
   1 ┌ (P ∨ Q)    Supp

or and | are synonyms.

Negation (¬)

> not P
   1 ┌ ¬P    Supp

not, ~, and ! are synonyms.

Material Conditional (→)

> (P implies Q)
   1 ┌ (P → Q)    Supp

implies, imply, and -> are synonyms. You can also write (if P then Q).

Quantification and Equality

See the sections "First-Order Logic" and "First-Order Logic with Equality".

Propositional Logic

Contradiction (Absurdity)

> P
   1 ┌ P    Supp
> !P
   1 ┌ P       Supp
   2 │ ┌ ¬P    Supp
> abs 1 2
   1 ┌ P       Supp
   2 │ ┌ ¬P    Supp
   3 │ │ ⊥     Abs 1,2

abs, absurd, and absurdity are synonyms.

Explosion (Ex Falso Quodlibet)

To derive anything from $⊥$ (ex falso quodlibet):

...
   1 ┌ P       Supp
   2 │ ┌ ¬P    Supp
   3 │ │ ⊥     Abs 1,2
> efq 3 (Q & !R)
   1 ┌ P             Supp
   2 │ ┌ ¬P          Supp
   3 │ │ ⊥           Abs 1,2
   4 │ │ (Q ∧ ¬R)    EFQ 3

Reductio ad Absurdum

...
   1 ┌ P       Supp
   2 │ ┌ ¬P    Supp
   3 │ │ ⊥     Abs 1,2
> end
   1 ┌ P       Supp
   2 │ ┌ ¬P    Supp
   3 │ │ ⊥     Abs 1,2
   4 │
> raa 2
   1 ┌ P       Supp
   2 │ ┌ ¬P    Supp
   3 │ │ ⊥     Abs 1,2
   4 │
   5 │ ¬¬P     RAA 2

Conjunction Introduction (∧-Introduction)

> P
   1 ┌ P    Supp
> Q
   1 ┌ P      Supp
   2 │ ┌ Q    Supp
> 1 and 2
   1 ┌ P            Supp
   2 │ ┌ Q          Supp
   3 │ │ (P ∧ Q)    ∧I 1,2

Conjunction Elimination (∧-Elimination)

> (P and Q)
   1 ┌ (P ∧ Q)    Supp
> left 1
   1 ┌ (P ∧ Q)    Supp
   2 │ P          ∧E 1
> right 1
   1 ┌ (P ∧ Q)    Supp
   2 │ P          ∧E 1
   3 │ Q          ∧E 1

left and l are synonyms. right and r are synonyms.

Disjunction Introduction (∨-Introduction)

> P
   1 ┌ P    Supp
> 1 or Q
   1 ┌ P          Supp
   2 │ (P ∨ Q)    ∨I 1
> R or 2
   1 ┌ P                Supp
   2 │ (P ∨ Q)          ∨I 1
   3 │ (R ∨ (P ∨ Q))    ∨I 2

Disjunction Elimination (∨-Elimination)

To prove that $(((P ∧ Q) ∨ (Q ∧ R)) → Q)$:

> ((P and Q) or (Q and R))
   1 ┌ ((P ∧ Q) ∨ (Q ∧ R))    Supp
> (P and Q)
   1 ┌ ((P ∧ Q) ∨ (Q ∧ R))    Supp
   2 │ ┌ (P ∧ Q)              Supp
> right 2
   1 ┌ ((P ∧ Q) ∨ (Q ∧ R))    Supp
   2 │ ┌ (P ∧ Q)              Supp
   3 │ │ Q                    ∧E 2
> end
   1 ┌ ((P ∧ Q) ∨ (Q ∧ R))    Supp
   2 │ ┌ (P ∧ Q)              Supp
   3 │ │ Q                    ∧E 2
   4 │
> (Q and R)
   1 ┌ ((P ∧ Q) ∨ (Q ∧ R))    Supp
   2 │ ┌ (P ∧ Q)              Supp
   3 │ │ Q                    ∧E 2
   4 │
   5 │ ┌ (Q ∧ R)              Supp
> left 5
   1 ┌ ((P ∧ Q) ∨ (Q ∧ R))    Supp
   2 │ ┌ (P ∧ Q)              Supp
   3 │ │ Q                    ∧E 2
   4 │
   5 │ ┌ (Q ∧ R)              Supp
   6 │ │ Q                    ∧E 5
> end
   1 ┌ ((P ∧ Q) ∨ (Q ∧ R))    Supp
   2 │ ┌ (P ∧ Q)              Supp
   3 │ │ Q                    ∧E 2
   4 │
   5 │ ┌ (Q ∧ R)              Supp
   6 │ │ Q                    ∧E 5
   7 │
> eliminate or 1 using 2, 5
   1 ┌ ((P ∧ Q) ∨ (Q ∧ R))    Supp
   2 │ ┌ (P ∧ Q)              Supp
   3 │ │ Q                    ∧E 2
   4 │
   5 │ ┌ (Q ∧ R)              Supp
   6 │ │ Q                    ∧E 5
   7 │
   8 │ Q                      ∨E 1,2,5

eliminate and elim are synonyms. using, with, and by are synonyms, and they are optional. You can also write a comma. (Commas are always optional.)

Conditional Proof (Implication Introduction)

...
   1 ┌ (P ∧ ¬P)    Supp
   2 │ P           ∧E 1
   3 │ ¬P          ∧E 1
   4 │ ⊥           Abs 2,3
> end
   1 ┌ (P ∧ ¬P)    Supp
   2 │ P           ∧E 1
   3 │ ¬P          ∧E 1
   4 │ ⊥           Abs 2,3
   5
> cp 1
   1 ┌ (P ∧ ¬P)        Supp
   2 │ P               ∧E 1
   3 │ ¬P              ∧E 1
   4 │ ⊥               Abs 2,3
   5
   6 ((P ∧ ¬P) → ⊥)    CP 1

Modus Ponens (Implication Elimination)

> (P -> Q)
   1 ┌ (P → Q)    Supp
> P
   1 ┌ (P → Q)    Supp
   2 │ ┌ P        Supp
> mp 1 2
   1 ┌ (P → Q)    Supp
   2 │ ┌ P        Supp
   3 │ │ Q        MP 1,2

Double Negation Elimination

> not not P
   1 ┌ ¬¬P    Supp
> dn 1
   1 ┌ ¬¬P    Supp
   2 │ P      DN 1

Examples

To prove that $((P → Q) → (¬P ∨ Q))$:

> (P->Q)
   1 ┌ (P → Q)    Supp
> ~(~P|Q)
   1 ┌ (P → Q)        Supp
   2 │ ┌ ¬(¬P ∨ Q)    Supp
> P
   1 ┌ (P → Q)        Supp
   2 │ ┌ ¬(¬P ∨ Q)    Supp
   3 │ │ ┌ P          Supp
> mp 1, 3
   1 ┌ (P → Q)        Supp
   2 │ ┌ ¬(¬P ∨ Q)    Supp
   3 │ │ ┌ P          Supp
   4 │ │ │ Q          MP 1,3
> not P or 4
   1 ┌ (P → Q)         Supp
   2 │ ┌ ¬(¬P ∨ Q)     Supp
   3 │ │ ┌ P           Supp
   4 │ │ │ Q           MP 1,3
   5 │ │ │ (¬P ∨ Q)    ∨I 4
> absurd 2, 5
   1 ┌ (P → Q)         Supp
   2 │ ┌ ¬(¬P ∨ Q)     Supp
   3 │ │ ┌ P           Supp
   4 │ │ │ Q           MP 1,3
   5 │ │ │ (¬P ∨ Q)    ∨I 4
   6 │ │ │ ⊥           Abs 2,5
> end
   1 ┌ (P → Q)         Supp
   2 │ ┌ ¬(¬P ∨ Q)     Supp
   3 │ │ ┌ P           Supp
   4 │ │ │ Q           MP 1,3
   5 │ │ │ (¬P ∨ Q)    ∨I 4
   6 │ │ │ ⊥           Abs 2,5
   7 │ │
> raa 3
   1 ┌ (P → Q)         Supp
   2 │ ┌ ¬(¬P ∨ Q)     Supp
   3 │ │ ┌ P           Supp
   4 │ │ │ Q           MP 1,3
   5 │ │ │ (¬P ∨ Q)    ∨I 4
   6 │ │ │ ⊥           Abs 2,5
   7 │ │
   8 │ │ ¬P            RAA 3
> 8 or Q
   1 ┌ (P → Q)         Supp
   2 │ ┌ ¬(¬P ∨ Q)     Supp
   3 │ │ ┌ P           Supp
   4 │ │ │ Q           MP 1,3
   5 │ │ │ (¬P ∨ Q)    ∨I 4
   6 │ │ │ ⊥           Abs 2,5
   7 │ │
   8 │ │ ¬P            RAA 3
   9 │ │ (¬P ∨ Q)      ∨I 8
> absurd 2, 9
   1 ┌ (P → Q)         Supp
   2 │ ┌ ¬(¬P ∨ Q)     Supp
   3 │ │ ┌ P           Supp
   4 │ │ │ Q           MP 1,3
   5 │ │ │ (¬P ∨ Q)    ∨I 4
   6 │ │ │ ⊥           Abs 2,5
   7 │ │
   8 │ │ ¬P            RAA 3
   9 │ │ (¬P ∨ Q)      ∨I 8
  10 │ │ ⊥             Abs 2,9
> end
   1 ┌ (P → Q)         Supp
   2 │ ┌ ¬(¬P ∨ Q)     Supp
   3 │ │ ┌ P           Supp
   4 │ │ │ Q           MP 1,3
   5 │ │ │ (¬P ∨ Q)    ∨I 4
   6 │ │ │ ⊥           Abs 2,5
   7 │ │
   8 │ │ ¬P            RAA 3
   9 │ │ (¬P ∨ Q)      ∨I 8
  10 │ │ ⊥             Abs 2,9
  11 │
> raa 2
   1 ┌ (P → Q)         Supp
   2 │ ┌ ¬(¬P ∨ Q)     Supp
   3 │ │ ┌ P           Supp
   4 │ │ │ Q           MP 1,3
   5 │ │ │ (¬P ∨ Q)    ∨I 4
   6 │ │ │ ⊥           Abs 2,5
   7 │ │
   8 │ │ ¬P            RAA 3
   9 │ │ (¬P ∨ Q)      ∨I 8
  10 │ │ ⊥             Abs 2,9
  11 │
  12 │ ¬¬(¬P ∨ Q)      RAA 2
> dn 12
   1 ┌ (P → Q)         Supp
   2 │ ┌ ¬(¬P ∨ Q)     Supp
   3 │ │ ┌ P           Supp
   4 │ │ │ Q           MP 1,3
   5 │ │ │ (¬P ∨ Q)    ∨I 4
   6 │ │ │ ⊥           Abs 2,5
   7 │ │
   8 │ │ ¬P            RAA 3
   9 │ │ (¬P ∨ Q)      ∨I 8
  10 │ │ ⊥             Abs 2,9
  11 │
  12 │ ¬¬(¬P ∨ Q)      RAA 2
  13 │ (¬P ∨ Q)        DN 12
> end
   1 ┌ (P → Q)         Supp
   2 │ ┌ ¬(¬P ∨ Q)     Supp
   3 │ │ ┌ P           Supp
   4 │ │ │ Q           MP 1,3
   5 │ │ │ (¬P ∨ Q)    ∨I 4
   6 │ │ │ ⊥           Abs 2,5
   7 │ │
   8 │ │ ¬P            RAA 3
   9 │ │ (¬P ∨ Q)      ∨I 8
  10 │ │ ⊥             Abs 2,9
  11 │
  12 │ ¬¬(¬P ∨ Q)      RAA 2
  13 │ (¬P ∨ Q)        DN 12
  14
> cp 1
   1 ┌ (P → Q)               Supp
   2 │ ┌ ¬(¬P ∨ Q)           Supp
   3 │ │ ┌ P                 Supp
   4 │ │ │ Q                 MP 1,3
   5 │ │ │ (¬P ∨ Q)          ∨I 4
   6 │ │ │ ⊥                 Abs 2,5
   7 │ │
   8 │ │ ¬P                  RAA 3
   9 │ │ (¬P ∨ Q)            ∨I 8
  10 │ │ ⊥                   Abs 2,9
  11 │
  12 │ ¬¬(¬P ∨ Q)            RAA 2
  13 │ (¬P ∨ Q)              DN 12
  14
  15 ((P → Q) → (¬P ∨ Q))    CP 1

To prove that $(¬(P ∨ Q) → (¬P ∧ ¬Q))$:

> not (P or Q)
   1 ┌ ¬(P ∨ Q)    Supp
> P
   1 ┌ ¬(P ∨ Q)    Supp
   2 │ ┌ P         Supp
> 2 or Q
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
> abs 1 3
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
   4 │ │ ⊥          Abs 1,3
> end
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
   4 │ │ ⊥          Abs 1,3
   5 │
> raa 2
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
   4 │ │ ⊥          Abs 1,3
   5 │
   6 │ ¬P           RAA 2
> Q
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
   4 │ │ ⊥          Abs 1,3
   5 │
   6 │ ¬P           RAA 2
   7 │ ┌ Q          Supp
> P or 7
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
   4 │ │ ⊥          Abs 1,3
   5 │
   6 │ ¬P           RAA 2
   7 │ ┌ Q          Supp
   8 │ │ (P ∨ Q)    ∨I 7
> abs 1 8
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
   4 │ │ ⊥          Abs 1,3
   5 │
   6 │ ¬P           RAA 2
   7 │ ┌ Q          Supp
   8 │ │ (P ∨ Q)    ∨I 7
   9 │ │ ⊥          Abs 1,8
> end
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
   4 │ │ ⊥          Abs 1,3
   5 │
   6 │ ¬P           RAA 2
   7 │ ┌ Q          Supp
   8 │ │ (P ∨ Q)    ∨I 7
   9 │ │ ⊥          Abs 1,8
  10 │
> raa 7
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
   4 │ │ ⊥          Abs 1,3
   5 │
   6 │ ¬P           RAA 2
   7 │ ┌ Q          Supp
   8 │ │ (P ∨ Q)    ∨I 7
   9 │ │ ⊥          Abs 1,8
  10 │
  11 │ ¬Q           RAA 7
> 6 and 11
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
   4 │ │ ⊥          Abs 1,3
   5 │
   6 │ ¬P           RAA 2
   7 │ ┌ Q          Supp
   8 │ │ (P ∨ Q)    ∨I 7
   9 │ │ ⊥          Abs 1,8
  10 │
  11 │ ¬Q           RAA 7
  12 │ (¬P ∧ ¬Q)    ∧I 6,11
> end
   1 ┌ ¬(P ∨ Q)     Supp
   2 │ ┌ P          Supp
   3 │ │ (P ∨ Q)    ∨I 2
   4 │ │ ⊥          Abs 1,3
   5 │
   6 │ ¬P           RAA 2
   7 │ ┌ Q          Supp
   8 │ │ (P ∨ Q)    ∨I 7
   9 │ │ ⊥          Abs 1,8
  10 │
  11 │ ¬Q           RAA 7
  12 │ (¬P ∧ ¬Q)    ∧I 6,11
  13
> cp 1
   1 ┌ ¬(P ∨ Q)                Supp
   2 │ ┌ P                     Supp
   3 │ │ (P ∨ Q)               ∨I 2
   4 │ │ ⊥                     Abs 1,3
   5 │
   6 │ ¬P                      RAA 2
   7 │ ┌ Q                     Supp
   8 │ │ (P ∨ Q)               ∨I 7
   9 │ │ ⊥                     Abs 1,8
  10 │
  11 │ ¬Q                      RAA 7
  12 │ (¬P ∧ ¬Q)               ∧I 6,11
  13
  14 (¬(P ∨ Q) → (¬P ∧ ¬Q))    CP 1

First-Order Logic

To write quantified wffs, use forall/for all/all and exists/exist/ex:

> forall x Px
   1 ┌ ∀x Px    Supp

> exists x Px
   1 ┌ ∃x Px    Supp

Universal Instantiation (∀-Elimination):

> forall x Px
   1 ┌ ∀x Px    Supp
> elim forall 1, a
   1 ┌ ∀x Px    Supp
   2 │ Pa       ∀E 1

Existential Generalization (∃-Introduction):

> Pa
   1 ┌ Pa    Supp
> exists 1, a to x
   1 ┌ Pa       Supp
   2 │ ∃x Px    ∃I 1

If not quantifying on all references, provide the resulting wff at the end:

> all x Pxx
   1 ┌ ∀x Pxx    Supp
> elim all 1 a
   1 ┌ ∀x Pxx    Supp
   2 │ Paa       ∀E 1
> ex 2 a x Pxa
   1 ┌ ∀x Pxx    Supp
   2 │ Paa       ∀E 1
   3 │ ∃x Pxa    ∃I 2

Universal Generalization (∀-Introduction):

...
   1 ┌ ¬∃x ¬Px     Supp
   2 │ ┌ ¬Pa       Supp
   3 │ │ ∃x ¬Px    ∃I 2
   4 │ │ ⊥         Abs 1,3
   5 │
   6 │ ¬¬Pa        RAA 2
   7 │ Pa          DN 6
> forall 7, a to x
   1 ┌ ¬∃x ¬Px     Supp
   2 │ ┌ ¬Pa       Supp
   3 │ │ ∃x ¬Px    ∃I 2
   4 │ │ ⊥         Abs 1,3
   5 │
   6 │ ¬¬Pa        RAA 2
   7 │ Pa          DN 6
   8 │ ∀x Px       ∀I 7

Existential Instantiation (∃-Elimination):

...
   1 ┌ ∀x Px       Supp
   2 │ ┌ ∃x ¬Px    Supp
   3 │ │ ┌ ¬Pa     Supp
   4 │ │ │ Pa      ∀E 1
   5 │ │ │ ⊥       Abs 3,4
   6 │ │
> elim exists 2 using 3, a
   1 ┌ ∀x Px       Supp
   2 │ ┌ ∃x ¬Px    Supp
   3 │ │ ┌ ¬Pa     Supp
   4 │ │ │ Pa      ∀E 1
   5 │ │ │ ⊥       Abs 3,4
   6 │ │
   7 │ │ ⊥         ∃E 2,3

Examples

From $∀x Fx, ∀x (Fx → Gx)$, to prove that $∀x Gx$:

> all x Fx
   1 ┌ ∀x Fx    Supp
> all x (Fx -> Gx)
   1 ┌ ∀x Fx             Supp
   2 │ ┌ ∀x (Fx → Gx)    Supp
> elim all 1 a
   1 ┌ ∀x Fx             Supp
   2 │ ┌ ∀x (Fx → Gx)    Supp
   3 │ │ Fa              ∀E 1
> elim all 2 a
   1 ┌ ∀x Fx             Supp
   2 │ ┌ ∀x (Fx → Gx)    Supp
   3 │ │ Fa              ∀E 1
   4 │ │ (Fa → Ga)       ∀E 2
> mp 3 4
   1 ┌ ∀x Fx             Supp
   2 │ ┌ ∀x (Fx → Gx)    Supp
   3 │ │ Fa              ∀E 1
   4 │ │ (Fa → Ga)       ∀E 2
   5 │ │ Ga              MP 3,4
> all 5 a x
   1 ┌ ∀x Fx             Supp
   2 │ ┌ ∀x (Fx → Gx)    Supp
   3 │ │ Fa              ∀E 1
   4 │ │ (Fa → Ga)       ∀E 2
   5 │ │ Ga              MP 3,4
   6 │ │ ∀x Gx           ∀I 5

From $∃x (Fx ∧ Gx), ∀x (Hx → ¬Gx)$, to prove that $∃x (Fx ∧ ¬Hx)$:

> ex x (Fx and Gx)
   1 ┌ ∃x (Fx ∧ Gx)    Supp
> all x (Hx -> ~Gx)
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
> (Fa and Ga)
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
   3 │ │ ┌ (Fa ∧ Ga)      Supp
> elim all 2 a
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
   3 │ │ ┌ (Fa ∧ Ga)      Supp
   4 │ │ │ (Ha → ¬Ga)     ∀E 2
> left 3
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
   3 │ │ ┌ (Fa ∧ Ga)      Supp
   4 │ │ │ (Ha → ¬Ga)     ∀E 2
   5 │ │ │ Fa             ∧E 3
> right 3
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
   3 │ │ ┌ (Fa ∧ Ga)      Supp
   4 │ │ │ (Ha → ¬Ga)     ∀E 2
   5 │ │ │ Fa             ∧E 3
   6 │ │ │ Ga             ∧E 3
> Ha
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
   3 │ │ ┌ (Fa ∧ Ga)      Supp
   4 │ │ │ (Ha → ¬Ga)     ∀E 2
   5 │ │ │ Fa             ∧E 3
   6 │ │ │ Ga             ∧E 3
   7 │ │ │ ┌ Ha           Supp
> mp 4 7
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
   3 │ │ ┌ (Fa ∧ Ga)      Supp
   4 │ │ │ (Ha → ¬Ga)     ∀E 2
   5 │ │ │ Fa             ∧E 3
   6 │ │ │ Ga             ∧E 3
   7 │ │ │ ┌ Ha           Supp
   8 │ │ │ │ ¬Ga          MP 4,7
> abs 6 8
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
   3 │ │ ┌ (Fa ∧ Ga)      Supp
   4 │ │ │ (Ha → ¬Ga)     ∀E 2
   5 │ │ │ Fa             ∧E 3
   6 │ │ │ Ga             ∧E 3
   7 │ │ │ ┌ Ha           Supp
   8 │ │ │ │ ¬Ga          MP 4,7
   9 │ │ │ │ ⊥            Abs 6,8
> end
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
   3 │ │ ┌ (Fa ∧ Ga)      Supp
   4 │ │ │ (Ha → ¬Ga)     ∀E 2
   5 │ │ │ Fa             ∧E 3
   6 │ │ │ Ga             ∧E 3
   7 │ │ │ ┌ Ha           Supp
   8 │ │ │ │ ¬Ga          MP 4,7
   9 │ │ │ │ ⊥            Abs 6,8
  10 │ │ │
> raa 7
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
   3 │ │ ┌ (Fa ∧ Ga)      Supp
   4 │ │ │ (Ha → ¬Ga)     ∀E 2
   5 │ │ │ Fa             ∧E 3
   6 │ │ │ Ga             ∧E 3
   7 │ │ │ ┌ Ha           Supp
   8 │ │ │ │ ¬Ga          MP 4,7
   9 │ │ │ │ ⊥            Abs 6,8
  10 │ │ │
  11 │ │ │ ¬Ha            RAA 7
> 5 and 11
   1 ┌ ∃x (Fx ∧ Gx)       Supp
   2 │ ┌ ∀x (Hx → ¬Gx)    Supp
   3 │ │ ┌ (Fa ∧ Ga)      Supp
   4 │ │ │ (Ha → ¬Ga)     ∀E 2
   5 │ │ │ Fa             ∧E 3
   6 │ │ │ Ga             ∧E 3
   7 │ │ │ ┌ Ha           Supp
   8 │ │ │ │ ¬Ga          MP 4,7
   9 │ │ │ │ ⊥            Abs 6,8
  10 │ │ │
  11 │ │ │ ¬Ha            RAA 7
  12 │ │ │ (Fa ∧ ¬Ha)     ∧I 5,11
> ex 12 a x
   1 ┌ ∃x (Fx ∧ Gx)         Supp
   2 │ ┌ ∀x (Hx → ¬Gx)      Supp
   3 │ │ ┌ (Fa ∧ Ga)        Supp
   4 │ │ │ (Ha → ¬Ga)       ∀E 2
   5 │ │ │ Fa               ∧E 3
   6 │ │ │ Ga               ∧E 3
   7 │ │ │ ┌ Ha             Supp
   8 │ │ │ │ ¬Ga            MP 4,7
   9 │ │ │ │ ⊥              Abs 6,8
  10 │ │ │
  11 │ │ │ ¬Ha              RAA 7
  12 │ │ │ (Fa ∧ ¬Ha)       ∧I 5,11
  13 │ │ │ ∃x (Fx ∧ ¬Hx)    ∃I 12
> end
   1 ┌ ∃x (Fx ∧ Gx)         Supp
   2 │ ┌ ∀x (Hx → ¬Gx)      Supp
   3 │ │ ┌ (Fa ∧ Ga)        Supp
   4 │ │ │ (Ha → ¬Ga)       ∀E 2
   5 │ │ │ Fa               ∧E 3
   6 │ │ │ Ga               ∧E 3
   7 │ │ │ ┌ Ha             Supp
   8 │ │ │ │ ¬Ga            MP 4,7
   9 │ │ │ │ ⊥              Abs 6,8
  10 │ │ │
  11 │ │ │ ¬Ha              RAA 7
  12 │ │ │ (Fa ∧ ¬Ha)       ∧I 5,11
  13 │ │ │ ∃x (Fx ∧ ¬Hx)    ∃I 12
  14 │ │
> elim ex 1 using 3 a
   1 ┌ ∃x (Fx ∧ Gx)         Supp
   2 │ ┌ ∀x (Hx → ¬Gx)      Supp
   3 │ │ ┌ (Fa ∧ Ga)        Supp
   4 │ │ │ (Ha → ¬Ga)       ∀E 2
   5 │ │ │ Fa               ∧E 3
   6 │ │ │ Ga               ∧E 3
   7 │ │ │ ┌ Ha             Supp
   8 │ │ │ │ ¬Ga            MP 4,7
   9 │ │ │ │ ⊥              Abs 6,8
  10 │ │ │
  11 │ │ │ ¬Ha              RAA 7
  12 │ │ │ (Fa ∧ ¬Ha)       ∧I 5,11
  13 │ │ │ ∃x (Fx ∧ ¬Hx)    ∃I 12
  14 │ │
  15 │ │ ∃x (Fx ∧ ¬Hx)      ∃E 1,3

First-Order Logic with Equality

$(a = b)$ is a wff:

> (a = b)
   1 ┌ a = b    Supp

equals, equal, eq, and = are synonyms.

You can also write !=, does not equal, not equal, etc.:

> (a != b)
   1 ┌ ¬a = b    Supp

Identity (=-Introduction)

To introduce $(a = a)$ for any $a$:

> equals a
   1 a = a    =I
> all 1 a x
   1 a = a       =I
   2 ∀x x = x    ∀I 1

Substitution (=-Elimination or Leibniz's Law)

To prove that $((a = b ∧ b = c) → a = c)$:

> ((a = b) and (b = c))
   1 ┌ (a = b ∧ b = c)    Supp
> left 1
   1 ┌ (a = b ∧ b = c)    Supp
   2 │ a = b              ∧E 1
> right 1
   1 ┌ (a = b ∧ b = c)    Supp
   2 │ a = b              ∧E 1
   3 │ b = c              ∧E 1
> replace 2 using 3 left
   1 ┌ (a = b ∧ b = c)    Supp
   2 │ a = b              ∧E 1
   3 │ b = c              ∧E 1
   4 │ a = c              =E 2,3

replace, substitute, and sub are synonyms.

The left means to substitute occurrences of the left side of the equality with the right. (right vice versa.)

You can also partially substitute by providing the resulting wff at the end:

> Paa
   1 ┌ Paa    Supp
> (a = b)
   1 ┌ Paa        Supp
   2 │ ┌ a = b    Supp
> replace 1 using 2 Pab
   1 ┌ Paa        Supp
   2 │ ┌ a = b    Supp
   3 │ │ Pab      =E 1,2

Examples

Now let's prove that $1 + 1 = 2$.

From $∃x (Fx ∧ ∀y (Fy → y = x)), ∃x (Gx ∧ ∀y (Gy → y = x)), ¬∃x (Fx ∧ Gx)$, to prove that $∃x ∃y ((((Fx ∨ Gx) ∧ (Fy ∨ Gy)) ∧ ¬x = y) ∧ ∀z ((Fz ∨ Gz) → (z = x ∨ z = y)))$:

> ex x (Fx and all y (Fy -> (y = x)))
...
> ex x (Gx and all y (Gy -> (y = x)))
...
> ~ex x (Fx and Gx)
...
> (Fa and all y (Fy -> (y = a)))
...
> (Gb and all y (Gy->(y=b)))
   1 ┌ ∃x (Fx ∧ ∀y (Fy → y = x))         Supp
   2 │ ┌ ∃x (Gx ∧ ∀y (Gy → y = x))       Supp
   3 │ │ ┌ ¬∃x (Fx ∧ Gx)                 Supp
   4 │ │ │ ┌ (Fa ∧ ∀y (Fy → y = a))      Supp
   5 │ │ │ │ ┌ (Gb ∧ ∀y (Gy → y = b))    Supp
> left 4
...
> right 4
...
> left 5
...
> right 5
...
> 6 or Ga
   1 ┌ ∃x (Fx ∧ ∀y (Fy → y = x))         Supp
   2 │ ┌ ∃x (Gx ∧ ∀y (Gy → y = x))       Supp
   3 │ │ ┌ ¬∃x (Fx ∧ Gx)                 Supp
   4 │ │ │ ┌ (Fa ∧ ∀y (Fy → y = a))      Supp
   5 │ │ │ │ ┌ (Gb ∧ ∀y (Gy → y = b))    Supp
   6 │ │ │ │ │ Fa                        ∧E 4
   7 │ │ │ │ │ ∀y (Fy → y = a)           ∧E 4
   8 │ │ │ │ │ Gb                        ∧E 5
   9 │ │ │ │ │ ∀y (Gy → y = b)           ∧E 5
  10 │ │ │ │ │ (Fa ∨ Ga)                 ∨I 6
> Fb or 8
...
> (a = b)
...
> replace 6 using 12, Fb
...
> 13 and 8
...
> ex 14 b x
   1 ┌ ∃x (Fx ∧ ∀y (Fy → y = x))         Supp
   2 │ ┌ ∃x (Gx ∧ ∀y (Gy → y = x))       Supp
   3 │ │ ┌ ¬∃x (Fx ∧ Gx)                 Supp
   4 │ │ │ ┌ (Fa ∧ ∀y (Fy → y = a))      Supp
   5 │ │ │ │ ┌ (Gb ∧ ∀y (Gy → y = b))    Supp
   6 │ │ │ │ │ Fa                        ∧E 4
   7 │ │ │ │ │ ∀y (Fy → y = a)           ∧E 4
   8 │ │ │ │ │ Gb                        ∧E 5
   9 │ │ │ │ │ ∀y (Gy → y = b)           ∧E 5
  10 │ │ │ │ │ (Fa ∨ Ga)                 ∨I 6
  11 │ │ │ │ │ (Fb ∨ Gb)                 ∨I 8
  12 │ │ │ │ │ ┌ a = b                   Supp
  13 │ │ │ │ │ │ Fb                      =E 6,12
  14 │ │ │ │ │ │ (Fb ∧ Gb)               ∧I 13,8
  15 │ │ │ │ │ │ ∃x (Fx ∧ Gx)            ∃I 14
> abs 3 15
...
> end
...
> raa 12
...
> (Fc or Gc)
...
> Fc
   1 ┌ ∃x (Fx ∧ ∀y (Fy → y = x))         Supp
   2 │ ┌ ∃x (Gx ∧ ∀y (Gy → y = x))       Supp
   3 │ │ ┌ ¬∃x (Fx ∧ Gx)                 Supp
   4 │ │ │ ┌ (Fa ∧ ∀y (Fy → y = a))      Supp
   5 │ │ │ │ ┌ (Gb ∧ ∀y (Gy → y = b))    Supp
   6 │ │ │ │ │ Fa                        ∧E 4
   7 │ │ │ │ │ ∀y (Fy → y = a)           ∧E 4
   8 │ │ │ │ │ Gb                        ∧E 5
   9 │ │ │ │ │ ∀y (Gy → y = b)           ∧E 5
  10 │ │ │ │ │ (Fa ∨ Ga)                 ∨I 6
  11 │ │ │ │ │ (Fb ∨ Gb)                 ∨I 8
  12 │ │ │ │ │ ┌ a = b                   Supp
  13 │ │ │ │ │ │ Fb                      =E 6,12
  14 │ │ │ │ │ │ (Fb ∧ Gb)               ∧I 13,8
  15 │ │ │ │ │ │ ∃x (Fx ∧ Gx)            ∃I 14
  16 │ │ │ │ │ │ ⊥                       Abs 3,15
  17 │ │ │ │ │
  18 │ │ │ │ │ ¬a = b                    RAA 12
  19 │ │ │ │ │ ┌ (Fc ∨ Gc)               Supp
  20 │ │ │ │ │ │ ┌ Fc                    Supp
> elim all 7 c
...
> mp 20 21
...
> 22 or (c = b)
...
> end
...
> Gc
   1 ┌ ∃x (Fx ∧ ∀y (Fy → y = x))         Supp
   2 │ ┌ ∃x (Gx ∧ ∀y (Gy → y = x))       Supp
   3 │ │ ┌ ¬∃x (Fx ∧ Gx)                 Supp
   4 │ │ │ ┌ (Fa ∧ ∀y (Fy → y = a))      Supp
   5 │ │ │ │ ┌ (Gb ∧ ∀y (Gy → y = b))    Supp
   6 │ │ │ │ │ Fa                        ∧E 4
   7 │ │ │ │ │ ∀y (Fy → y = a)           ∧E 4
   8 │ │ │ │ │ Gb                        ∧E 5
   9 │ │ │ │ │ ∀y (Gy → y = b)           ∧E 5
  10 │ │ │ │ │ (Fa ∨ Ga)                 ∨I 6
  11 │ │ │ │ │ (Fb ∨ Gb)                 ∨I 8
  12 │ │ │ │ │ ┌ a = b                   Supp
  13 │ │ │ │ │ │ Fb                      =E 6,12
  14 │ │ │ │ │ │ (Fb ∧ Gb)               ∧I 13,8
  15 │ │ │ │ │ │ ∃x (Fx ∧ Gx)            ∃I 14
  16 │ │ │ │ │ │ ⊥                       Abs 3,15
  17 │ │ │ │ │
  18 │ │ │ │ │ ¬a = b                    RAA 12
  19 │ │ │ │ │ ┌ (Fc ∨ Gc)               Supp
  20 │ │ │ │ │ │ ┌ Fc                    Supp
  21 │ │ │ │ │ │ │ (Fc → c = a)          ∀E 7
  22 │ │ │ │ │ │ │ c = a                 MP 20,21
  23 │ │ │ │ │ │ │ (c = a ∨ c = b)       ∨I 22
  24 │ │ │ │ │ │
  25 │ │ │ │ │ │ ┌ Gc                    Supp
> elim all 9 c
...
> mp 25 26
...
> (c = a) or 27
...
> end
...
> elim or 19 using 20, 25
   1 ┌ ∃x (Fx ∧ ∀y (Fy → y = x))         Supp
   2 │ ┌ ∃x (Gx ∧ ∀y (Gy → y = x))       Supp
   3 │ │ ┌ ¬∃x (Fx ∧ Gx)                 Supp
   4 │ │ │ ┌ (Fa ∧ ∀y (Fy → y = a))      Supp
   5 │ │ │ │ ┌ (Gb ∧ ∀y (Gy → y = b))    Supp
   6 │ │ │ │ │ Fa                        ∧E 4
   7 │ │ │ │ │ ∀y (Fy → y = a)           ∧E 4
   8 │ │ │ │ │ Gb                        ∧E 5
   9 │ │ │ │ │ ∀y (Gy → y = b)           ∧E 5
  10 │ │ │ │ │ (Fa ∨ Ga)                 ∨I 6
  11 │ │ │ │ │ (Fb ∨ Gb)                 ∨I 8
  12 │ │ │ │ │ ┌ a = b                   Supp
  13 │ │ │ │ │ │ Fb                      =E 6,12
  14 │ │ │ │ │ │ (Fb ∧ Gb)               ∧I 13,8
  15 │ │ │ │ │ │ ∃x (Fx ∧ Gx)            ∃I 14
  16 │ │ │ │ │ │ ⊥                       Abs 3,15
  17 │ │ │ │ │
  18 │ │ │ │ │ ¬a = b                    RAA 12
  19 │ │ │ │ │ ┌ (Fc ∨ Gc)               Supp
  20 │ │ │ │ │ │ ┌ Fc                    Supp
  21 │ │ │ │ │ │ │ (Fc → c = a)          ∀E 7
  22 │ │ │ │ │ │ │ c = a                 MP 20,21
  23 │ │ │ │ │ │ │ (c = a ∨ c = b)       ∨I 22
  24 │ │ │ │ │ │
  25 │ │ │ │ │ │ ┌ Gc                    Supp
  26 │ │ │ │ │ │ │ (Gc → c = b)          ∀E 9
  27 │ │ │ │ │ │ │ c = b                 MP 25,26
  28 │ │ │ │ │ │ │ (c = a ∨ c = b)       ∨I 27
  29 │ │ │ │ │ │
  30 │ │ │ │ │ │ (c = a ∨ c = b)         ∨E 19,20,25
> end
...
> cp 19
...
> all 32 c z
...
> 10 and 11
...
> 34 and 18
   1 ┌ ∃x (Fx ∧ ∀y (Fy → y = x))                     Supp
   2 │ ┌ ∃x (Gx ∧ ∀y (Gy → y = x))                   Supp
   3 │ │ ┌ ¬∃x (Fx ∧ Gx)                             Supp
   4 │ │ │ ┌ (Fa ∧ ∀y (Fy → y = a))                  Supp
   5 │ │ │ │ ┌ (Gb ∧ ∀y (Gy → y = b))                Supp
   6 │ │ │ │ │ Fa                                    ∧E 4
   7 │ │ │ │ │ ∀y (Fy → y = a)                       ∧E 4
   8 │ │ │ │ │ Gb                                    ∧E 5
   9 │ │ │ │ │ ∀y (Gy → y = b)                       ∧E 5
  10 │ │ │ │ │ (Fa ∨ Ga)                             ∨I 6
  11 │ │ │ │ │ (Fb ∨ Gb)                             ∨I 8
  12 │ │ │ │ │ ┌ a = b                               Supp
  13 │ │ │ │ │ │ Fb                                  =E 6,12
  14 │ │ │ │ │ │ (Fb ∧ Gb)                           ∧I 13,8
  15 │ │ │ │ │ │ ∃x (Fx ∧ Gx)                        ∃I 14
  16 │ │ │ │ │ │ ⊥                                   Abs 3,15
  17 │ │ │ │ │
  18 │ │ │ │ │ ¬a = b                                RAA 12
  19 │ │ │ │ │ ┌ (Fc ∨ Gc)                           Supp
  20 │ │ │ │ │ │ ┌ Fc                                Supp
  21 │ │ │ │ │ │ │ (Fc → c = a)                      ∀E 7
  22 │ │ │ │ │ │ │ c = a                             MP 20,21
  23 │ │ │ │ │ │ │ (c = a ∨ c = b)                   ∨I 22
  24 │ │ │ │ │ │
  25 │ │ │ │ │ │ ┌ Gc                                Supp
  26 │ │ │ │ │ │ │ (Gc → c = b)                      ∀E 9
  27 │ │ │ │ │ │ │ c = b                             MP 25,26
  28 │ │ │ │ │ │ │ (c = a ∨ c = b)                   ∨I 27
  29 │ │ │ │ │ │
  30 │ │ │ │ │ │ (c = a ∨ c = b)                     ∨E 19,20,25
  31 │ │ │ │ │
  32 │ │ │ │ │ ((Fc ∨ Gc) → (c = a ∨ c = b))         CP 19
  33 │ │ │ │ │ ∀z ((Fz ∨ Gz) → (z = a ∨ z = b))      ∀I 32
  34 │ │ │ │ │ ((Fa ∨ Ga) ∧ (Fb ∨ Gb))               ∧I 10,11
  35 │ │ │ │ │ (((Fa ∨ Ga) ∧ (Fb ∨ Gb)) ∧ ¬a = b)    ∧I 34,18
> 35 and 33
...
> ex 36 b y
...
> ex 37 a x
...
> end
...
> elim ex 2 using 5 b
...
> end
...
> elim ex 1 using 4 a
   1 ┌ ∃x (Fx ∧ ∀y (Fy → y = x))                                                                Supp
   2 │ ┌ ∃x (Gx ∧ ∀y (Gy → y = x))                                                              Supp
   3 │ │ ┌ ¬∃x (Fx ∧ Gx)                                                                        Supp
   4 │ │ │ ┌ (Fa ∧ ∀y (Fy → y = a))                                                             Supp
   5 │ │ │ │ ┌ (Gb ∧ ∀y (Gy → y = b))                                                           Supp
   6 │ │ │ │ │ Fa                                                                               ∧E 4
   7 │ │ │ │ │ ∀y (Fy → y = a)                                                                  ∧E 4
   8 │ │ │ │ │ Gb                                                                               ∧E 5
   9 │ │ │ │ │ ∀y (Gy → y = b)                                                                  ∧E 5
  10 │ │ │ │ │ (Fa ∨ Ga)                                                                        ∨I 6
  11 │ │ │ │ │ (Fb ∨ Gb)                                                                        ∨I 8
  12 │ │ │ │ │ ┌ a = b                                                                          Supp
  13 │ │ │ │ │ │ Fb                                                                             =E 6,12
  14 │ │ │ │ │ │ (Fb ∧ Gb)                                                                      ∧I 13,8
  15 │ │ │ │ │ │ ∃x (Fx ∧ Gx)                                                                   ∃I 14
  16 │ │ │ │ │ │ ⊥                                                                              Abs 3,15
  17 │ │ │ │ │
  18 │ │ │ │ │ ¬a = b                                                                           RAA 12
  19 │ │ │ │ │ ┌ (Fc ∨ Gc)                                                                      Supp
  20 │ │ │ │ │ │ ┌ Fc                                                                           Supp
  21 │ │ │ │ │ │ │ (Fc → c = a)                                                                 ∀E 7
  22 │ │ │ │ │ │ │ c = a                                                                        MP 20,21
  23 │ │ │ │ │ │ │ (c = a ∨ c = b)                                                              ∨I 22
  24 │ │ │ │ │ │
  25 │ │ │ │ │ │ ┌ Gc                                                                           Supp
  26 │ │ │ │ │ │ │ (Gc → c = b)                                                                 ∀E 9
  27 │ │ │ │ │ │ │ c = b                                                                        MP 25,26
  28 │ │ │ │ │ │ │ (c = a ∨ c = b)                                                              ∨I 27
  29 │ │ │ │ │ │
  30 │ │ │ │ │ │ (c = a ∨ c = b)                                                                ∨E 19,20,25
  31 │ │ │ │ │
  32 │ │ │ │ │ ((Fc ∨ Gc) → (c = a ∨ c = b))                                                    CP 19
  33 │ │ │ │ │ ∀z ((Fz ∨ Gz) → (z = a ∨ z = b))                                                 ∀I 32
  34 │ │ │ │ │ ((Fa ∨ Ga) ∧ (Fb ∨ Gb))                                                          ∧I 10,11
  35 │ │ │ │ │ (((Fa ∨ Ga) ∧ (Fb ∨ Gb)) ∧ ¬a = b)                                               ∧I 34,18
  36 │ │ │ │ │ ((((Fa ∨ Ga) ∧ (Fb ∨ Gb)) ∧ ¬a = b) ∧ ∀z ((Fz ∨ Gz) → (z = a ∨ z = b)))          ∧I 35,33
  37 │ │ │ │ │ ∃y ((((Fa ∨ Ga) ∧ (Fy ∨ Gy)) ∧ ¬a = y) ∧ ∀z ((Fz ∨ Gz) → (z = a ∨ z = y)))       ∃I 36
  38 │ │ │ │ │ ∃x ∃y ((((Fx ∨ Gx) ∧ (Fy ∨ Gy)) ∧ ¬x = y) ∧ ∀z ((Fz ∨ Gz) → (z = x ∨ z = y)))    ∃I 37
  39 │ │ │ │
  40 │ │ │ │ ∃x ∃y ((((Fx ∨ Gx) ∧ (Fy ∨ Gy)) ∧ ¬x = y) ∧ ∀z ((Fz ∨ Gz) → (z = x ∨ z = y)))      ∃E 2,5
  41 │ │ │
  42 │ │ │ ∃x ∃y ((((Fx ∨ Gx) ∧ (Fy ∨ Gy)) ∧ ¬x = y) ∧ ∀z ((Fz ∨ Gz) → (z = x ∨ z = y)))        ∃E 1,4