Predicate Logic with Equality

Pre: Predicate Logic, Statements and Quantifiers

Recall:

Syntax

Info

  • We use the symbol for the equality predicate
  • is a binary infix predicate. Its arguments must be terms.
  • Equality has a lower precedence than other functions

Formalization

Examples

  1. Joe's age it 5

\exists x \cdot \neg (\op{age}(x) = 10)

\op{Prime}(5)

\forall x \cdot \op{Lion}(x) \implies \op{Mammal}(x)

Examples - Number of..

  1. There is at least one solution

\exists x \cdot \op{soln}(x) \land \forall y \cdot \op{soln}(y) \implies x = y

You can't use 'macro parameter character #' in math modeOr try the contrapositive:

\exists x \cdot \op{soln}(x) \land \forall y \cdot x \ne y \implies \neg \op{soln}(y)

\forall x, y \cdot \op{soln}(x) \land \op{soln}(y) \implies x = y

\neg (\exists x, y \cdot \op{soln}(x) \land \op{soln}(y) \land x \ne y)

Examples

  1. There are at least two solutions

\neg (\exists x, y \cdot \op{soln}(x) \land \op{soln}(y) \land x \ne y)

\exists x, y \cdot \op{soln}(x) \land \op{soln}(y) \land x \ne y \land \forall z \cdot \op{soln}(z) \implies (z = x \lor z = y)

Examples - Exclusivity

  1. Alice likes only bubblegum ice cream
    Meaning: Alice only like bubblegum ice cream, and NOTHING ELSEthe contrapositive may be more intuitive:that is, Alice likes ice cream, and anything else that isn't ice cream, she doesn't like.
  2. Only Alice likes bubblegum ice cream
    Meaning: Alice is the only person who like bubblegum ice cream, but she can like other stuff too

\op{likes}(\text{Alice}, \text{bbg_ic}) \land \forall x \cdot \op{iceCream}(x) \land \op{likes}(\text{Alice}, x) \implies x = \text{bbg_ic}

Natural Deduction

See Natural Deduction (Predicate Logic)

List of Additional Rules

Reflexivity:

Substitution:

Since equality is an equivalence relation, it is also symmetric and transitive:

Property

Equality is symmetric:

Proof

Property

Equality is transitive:

Proof

Leibniz's Law

Law

If is a theorem, then so is

(if and only if)

Semantics

Info

The standard interpretations of equality are that is equality on the values of the domain.

Examples

Example

Prove:

proof

Example

Show that the following argument is not valid:

where and are constants.

solution

Domain:
Mapping:

Syntax Meaning

Premise 1:

Premise 2:

Premise 3:

Conclusion:

[!example]
From Harry Potter and the Philosopher's Stone, on page 206-207, Harry and Hermione must solve a puzzle:

   Danger lies before you, while safety lies behind,
   Two of us will help you, whichever you would find,
P1 One among us seven will let you move ahead,
P2 Another will transport the drinker back instead,
P3 Two among our number hold only nettle wine,
P4 Three of us are killers, waiting hidden in line.
   Choose, unless you wish to stay here forevermore,
   To help you in your choice, we give you these clues four:
P5 First, however slyly the poison tries to hide
   You will always find some on nettle wine’s left side;
P6 Second, different are those who stand at either end,
P7 But if you would move onwards, neither is your friend;
P8 Third, as you see clearly, all are different size,
   Neither dwarf nor giant holds death in their insides;
P9 Fourth, the second left and the second on the right
   Are twins once you taste them, though different at first sight.

The puzzle has multiple solutions, apparently the author forgot to include the sizes of the bottles standing in the row. Here are the sizes of the bottles at each position, where 1 is the smallest bottle and 7 is the largest bottle:

Position 1 2 3 4 5 6 7
Size 3 4 1 2 6 7 5

Now there is only one solution

  1. Formalize the clues in predicate logic with equality
  2. Use natural deduction to prove which bottle is the bottle that lets you move ahead
    • Break the proof into subproofs that each prove some information about one of the bottles

solution

Premises:

\forall i \cdot b(i + 1) = W \implies b(i) = P

b(1) \ne b(7)

b(2) = b(6)

\begin{align}
& (1)\quad b(2) = b(6) && \text{premise 9} \
& (2)\quad \exists i \cdot b(i) = A \land (\forall k \cdot b(k) = A \implies k = i) && \text{premise 1} \
& (3)\quad \text{disprove } b(z) = A\ { \
& \quad (4)\quad b(6) = A && \text{by eq_e on 1, 3} \
& \quad (5)\quad \text{for some } iu \text{ assume } b(iu) = a \land (\forall k \cdot b(k) = A \implies k = iu)\ { \
& \quad \quad (6)\quad \forall k \cdot b(k) = A \implies k = iu && \text{by and_e on 5} \
& \quad \quad (7)\quad b(2) = A \implies 2 = iu && \text{by forall_e on 6} \
& \quad \quad (8)\quad 2 = iu && \text{by imp_e on 3, 7} \
& \quad \quad (9)\quad b(6) = A \implies 6 = iu && \text{by forall_e on 6} \
& \quad \quad (10)\quad 6 = iu && \text{by imp_e on 4, 9} \
& \quad \quad (11)\quad 2 = 6 && \text{by eq_e on 8, 10} \
& \quad \quad (12)\quad \text{false} && \text{by arithmetic on 11} \
& \quad } \
& \quad (13)\quad \text{false} && \text{by exists_e on 5-12} \
& } \
& (14)\quad b(2) \ne A && \text{by raa on 3-13}
\end