Prove that
	∀x . ∃ y . C(x) ∧ L(x,y) 	⊨ 	∀x . C(x)
	[(∀x . ∃ y . C(x) ∧ L(x,y)) → (∀x . C(x))] is true
Direct proof: use proof rules
Entailment: assume left-hand side, prove right-hand side
For all: instantiate with an "unknown" variable
Exists: instantiate with a value of my choice
Cases: disjunction, assume each side on its own

Either ∀x . C(x) or ¬∀x . C(x)
case 1: ∀x . C(x)
	In this case,
		∀x . ∃ y . C(x) ∧ L(x,y) 	⊨ 	∀x . C(x)
	is equivalent to
		∀x . ∃ y . True ∧ L(x,y) 	⊨ 	True
	Because anything ⊨ True, the entailment holds in this case
case 2: ¬∀x . C(x)
	In this case,
		∀x . ∃ y . C(x) ∧ L(x,y) 	⊨ 	∀x . C(x)
	is equivalent to
		∀x . ∃ y . C(x) ∧ L(x,y) 	⊨ 	False
		∀x . C(x) ∧ ∃ y . L(x,y) 	⊨ 	False
		∀x . C(x) ∧ ∀x . ∃ y . L(x,y) 	⊨ 	False
		False ∧ ∀x . ∃ y . L(x,y) 	⊨ 	False
		False 	⊨ 	False
	Because False ⊨ False, the entailment holds in this case
Because the entailment held in both cases, it must hold in general.





Assume 	∀x . ∃ y . C(x) ∧ L(x,y)
	∀x . C(x) ∧ ∃ y . L(x,y)
	∀x . (C(x) ∧ ∃ y . (L(x,y)))
	(∀x . C(x)) ∧ (∀x . ∃ y . (L(x,y)))
	(∀x . C(x))
	(∀x . ∃ y . (L(x,y)))

Proof.
	Assume ∀x . ∃ y . C(x) ∧ L(x,y). We can move the ∃ across a term to get ∀x . C(x) ∧ ∃ y . L(x,y); we then distribute the ∀ to get (∀x . C(x)) ∧ (∀x . ∃ y . (L(x,y))), which is a conjunction and thus entails its conjuncts, including (∀x . C(x)).
	Because assuming ∀x . ∃ y . C(x) ∧ L(x,y) let us prove ∀x . C(x), it must be that 
	∀x . ∃ y . C(x) ∧ L(x,y) 	⊨ 	∀x . C(x)









—————————————————————————————————
Prove that
	∀x . ∃ y . C(y) ∧ L(x,y) 	⊭ 	∀x . C(x)

—————————————————————————————————
function signOf(x)
	if x < 0, then return -1			(x < 0)
	if x == 0, then return 0			(x = 0) ∧ ¬(x<0)
	if x > 0, then return 1			(x > 0) ∧ (x ≠ 0) ∧ ¬(x < 0)
	crash with an error			¬(x > 0) ∧ (x ≠ 0) ∧ ¬(x < 0)

Prove the above function never crashes with an error
	∄ x . ((¬(x > 0)) ∧ (x ≠ 0)) ∧ (¬(x < 0))
	G(x,y) : x > y
	E(x,y) : x = y
	L(x,y) : x < y
	∄ x . ((¬G(x,0)) ∧ (¬E(x,0))) ∧ (¬L(x,0))
	∀ x . ¬(((¬G(x,0)) ∧ (¬E(x,0))) ∧ (¬L(x,0)))
via arithmetic,
	exactly one of G(x,0), E(x,0), and L(x,0) must be true










—————————————————————————————————
Defn: an addition-safe number is a positive number made up of n copies of the nth digit where repeated summing of digits yields n.
1 is addition-safe because it is 1 1-digit that sums to 1.
22 is not addition-safe because it sums to 4.
4444 is not addition-safe because it sums to 7.

Prove there is an addition-safe number > 1.
∃ x . A(x) ∧ (x > 1)










—————————————————————————————————

Write the following in prose
Theorem: (A → B) ∧ (B → A) ≡ (A ↔ B)
Proof:
	A = ⊤ means 
		(A → B) ∧ (B → A) ≡ 
		(⊤ → B) ∧ (B → ⊤) ≡ 
		(B) ∧ (⊤) ≡ 
		B ≡ 
		(⊤ ↔ B) ≡ 
		(A ↔ B)
	A = ⊥ means 
		(A → B) ∧ (B → A) ≡ 
		(⊥ → B) ∧ (B → ⊥) ≡ 
		(⊤) ∧ (¬B) ≡ 
		¬B ≡ 
		(⊥ ↔ B) ≡ 
		(A ↔ B)



—————————————————————————————————