 The table suggests an interesting correspondence between the typed \(\lambda\)-calculus and formal logic. Could it really be that the types assigned to formulas, when understood as logical formulas, are valid? Yes, though ‘validity’ needs to understood not as classical validity: