npm package: @plaivy/logic
Description: `@plaivy/logic` is an interactive way to write proofs using formal rules of inference.
Author: Plaivy
Latest version: 1.1.1

# 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
```