layoff-logic.md

Layoff Logic

This is a tounge-in-cheek illustration of formal logic used refute the claim that high performers are never laid off, using that claim itself (made by an executive) as evidence that judgements are sometimes made without context.

In reality, there is no need to prove such an obvious point because by definition layoffs are not "for cause" terminations, the company has no legal responsibility to justify them as related to the impacted individuals.

Propositional Logic (Zeroth Order)

The proof proceeds by first assuming P1 and showing that it leads to contradiction.

P1 High performers are never laid off
P2 Layoff decisions are substantially made by executives
P1 ∧ P2 → P3
P3 Executives always assess performance accurately
P4 Performance can't be accurately assessed without context
P5 An executive made a performance assesment without context
P4 ∧ P5 → P6
P6 Executives do not always assess performance accurately
P3 ^ P6 ⊥
This leads to contradiction

QED

For good measure we can run this in a Sat solver, Z3 / SMTLIB2:

You can run things like this in Z3 Playground or install Z3.

(declare-const P1 Bool)
(declare-const P2 Bool)
(declare-const P3 Bool)
(declare-const P4 Bool)
(declare-const P5 Bool)
(declare-const P6 Bool)

; Assertions based on the logical structure
(assert P1) ; High performers are never laid off
(assert P2) ; Layoff decisions are substantially made by executives

; P1 ∧ P2 → P3
; If P1 and P2 are true, then P3 must be true
; Executives always assess performance accurately
(assert (=> (and P1 P2) P3))

(assert P4) ; Performance can't be accurately assessed without context
(assert P5) ; An executive made a performance assessment without context

; P4 ∧ P5 → P6
; If P4 and P5 are true, then !P3 must be true
; Executives do not always assess performance accurately
(assert (=> (and P4 P5) (not P3)))

; Check for satisfiability
(check-sat)

Result is unsatifyable, confirming we have modeled the contradiction.

unsat

Commenting out P5 would satisfy.

Predicate Logic (First Order)

For practice, we sketch the same proof by contradiction in predicate logic, which is more expressive capturing objects and relations directly.

P1: ∀x (HighPerformer(x) → ¬LaidOff(x))
P3: ∀x (Executive(x) → AccurateAssessment(x))
P4:  ∀x (AccurateAssessment(x) → HadContext(x))
P5: ∃x (Executive(x) ∧ MadeAssessment(x) ∧ ¬HadContext(x))

(declare-sort Person 0)

; Declare predicates
(declare-fun HighPerformer (Person) Bool)
(declare-fun LaidOff (Person) Bool)
(declare-fun Executive (Person) Bool)
(declare-fun AccurateAssessment (Person) Bool)
(declare-fun MadeAssessment (Person) Bool)
(declare-fun HadContext (Person) Bool)

; P1: High performers are never laid off
(assert (forall ((x Person)) (=> (HighPerformer x) (not (LaidOff x)))))

; P3: Executives always assess performance accurately
(assert (forall ((x Person)) (=> (Executive x) (AccurateAssessment x))))

; P4: Performance can't be accurately assessed without context
(assert (forall ((x Person)) (=>  (AccurateAssessment x) (HadContext x))))

; P5: An executive made a performance assessment without context
(assert (exists ((x Person)) (and (Executive x) (MadeAssessment x) (not (HadContext x)))))

; Check for satisfiability
(check-sat)

Result:

unsat

Again, unsatisfiable but commenting out P5 would satisfy.