# Logic

In this section, we’ll introduce the basics of propositional logic. Even if you’re unfamiliar with the idea, you’ve almost certainly used it in programming before.

### \E

\E means “exists”. We write \E x \in S : P(x) to say “there is at least one x in the set such that P(x) is true.” It’s the equivalent of a python any() or a Ruby any?. If we wanted to check that a set had an even number in it, we could write HasEvenNumber(S) == \E x \in S : IsEven(x)

~\E is the opposite: it says that there are no such elements. \E x \in {}: Foo is always false, since there are no elements in {}.

Assuming Sum(S) returns the sum of the elements of S, write an operator that, for a given set of integers S and integer N, returns if there are N elements in S that sum to 0. eg

SumsToZero({1, 2, -7, 4, 11}, 2) = FALSE
SumsToZero({1, 2, -7, 4, 11}, 4) = TRUE
SumsToZero({1, 2, -7, 4, 11}, 5) = FALSE


SumsToZero(S, N) == \E s \in SUBSET S:
/\ Cardinality(s) = N
/\ Sum(s) = 0


### \A

\A means “all”. We write \A x \in S : P(x) to say “For every x in the set, P(x) is true.” If we wanted to check that a set had no odd numbers in it, we could write OnlyEvenNumbers(S) == \A x \in S : IsEven(x). If there are only even numbers, OnlyEvenNumbers is true. Otherwise it’s false. Simple.

~\A is the opposite: it says that there is at least one element where P(x) is false. \A x \in {}: Foo is always true, since there are no elements in {}, so all zero elements pass the test.

Given a set and an operator, determine whether the operator is commutative over all elements in the set.

IsCommutative(Op(,), S) == \A x \in S :
\A y \in S : Op(x,y) = Op(y,x)


Alternatively, we could put them on the same line:

IsCommutative(Op(,), S) == \A x \in S, y \in S : Op(x,y) = Op(y,x)


### => and <=>

P => Q means “If P is true, then Q must also be true.” Note that P can be false and Q can be true, or both can be false. It’s equivalent to writing ~P \/ Q, which is how TLC interprets it.

P <=> Q means “Either both P and Q are true or both are false.” It’s equivalent to writing (~P /\ ~Q) \/ (P /\ Q). P <=> ~Q is P XOR Q.

Without looking back at the introduction, write an operator that returns the maximum number of a set.

Max(S) == CHOOSE x \in S : \A y \in S : y <= x


Both => and <=> follow the same precedence rules as logical junctions. In other words, TLC interprets

/\ A
/\ B
=> C


as A /\ (B => C), whereas without the indent it’s interpreted as (A /\ B) => C.

### CHOOSE

While we introduced the CHOOSE operator back in sets, it really comes into its own when we add the logical operators. Many quantified properties, such as “the largest x such that P”, can be expressed as “the x where all larger elements don’t have P” or “the x where all of the other elements with P are smaller”. For example, what is the largest prime in a set S?

IsPrime(x) == x > 1 /\ ~\E d \in 2..(x-1) : x % d = 0

LargestPrime(S) == CHOOSE x \in S:
/\ IsPrime(x)
/\ \A y \in S:
IsPrime(y) => y <= x
\* or y > x => ~IsPrime(y)


A prime number p is a twin prime if p-2 is prime or p+2 is prime. Find the largest twin prime in S.

IsTwinPrime(x) == /\ IsPrime(x)
/\ \/ IsPrime(x + 2)
\/ IsPrime(x - 2)

LargestTwinPrime(S) == CHOOSE x \in S:
/\ IsTwinPrime(x)
/\ \A y \in S: IsTwinPrime(y) => y <= x
* or y > x => ~ IsTwinPrime(y)


Now return the largest pair of twin primes, ordered by value. Assume that S may be missing numbers and, if one of the twin primes is missing, the pair is invalid. For example, the largest pair in {3, 5, 13} is <<3, 5>>, not <<5, 13>>.

LargestTwinPair(S) == CHOOSE <<x, y>> \in S \X S:
/\ IsPrime(x)
/\ IsPrime(y)
/\ x = y - 2
/\ \A <<w, z>> \in S \X S:
/\ IsPrime(z)
/\ IsPrime(w)
/\ w = z - 2
=> z < y


Given stockprices is a tuple of positive integers representing the value of a stock at a given time of day, write an operator that determines the maximum profit you could make by buying and selling a single stock. Assume for this problem that you cannot short; you must buy before you sell.

MaxProfit(stockprices) ==
LET sp == stockprices \* clean it up a bit
TimePair == (1..Len(sp)) \X (1..Len(sp))
Profit[p \in TimePair] == sp[p[2]] - sp[p[1]]
best == CHOOSE best \in TimePair :
/\ best[2] > best[1] \* Buy after sell
/\ Profit[best] > 0 \* Make money plz
/\ \A worse \in TimePair :
worse[2] > worse[1] => Profit[best] >= Profit[worse]
IN Profit[best]
`

Note this will crash if there is no possible pair, which is preferrable to paying trading fees twice on a zero-dollar profit.