First-order definability travels backward along reductions

The bottom of the ladder is closed under reductions, exactly as every class above it is: pull the defining sentence of the target back through the interpretation (DescriptiveComplexity.FOInterpretation.pullSentence) and it defines the source. For the order-invariant notion the interpretation is first extended with the lexicographic order of its tagged tuples (DescriptiveComplexity.FOInterpretation.ordExtend), so that the pulled sentence may mention the order the target's sentence mentions.

The point of these lemmas is their contrapositive (DescriptiveComplexity.not_le_of_not_foDefinable and its order-free twin): a problem that is not first-order definable reduces to no problem that is. This is what turns an inexpressibility result into a non-reducibility result, and so the only route this library has to a negative statement about the reduction order – everything else it proves is the existence of a reduction. It is applied to DescriptiveComplexity.EVEN (DescriptiveComplexity.even_not_foDefinable), whence DescriptiveComplexity.even_not_le_of_foDefinable.

Closure under reductions

theorem DescriptiveComplexity.FODefinableFree.of_foReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (h : FODefinableFree Q) (f : FOReduction P Q) : FODefinableFree P

Order-free first-order definability travels backward along FO reductions: the defining sentence of the target, pulled back through the interpretation, defines the source.

theorem DescriptiveComplexity.FODefinable.of_orderedReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (h : FODefinable Q) (f : OrderedFOReduction P Q) : FODefinable P

Order-invariant first-order definability travels backward along ordered FO reductions. The interpretation is extended with the lexicographic order on its tagged tuples, so the pulled sentence can still read an order; the extension is definable from the order of the input, which is what keeps the result inside FO(≤).

theorem DescriptiveComplexity.FODefinable.of_foReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (h : FODefinable Q) (f : FOReduction P Q) : FODefinable P

Order-invariant definability travels backward along plain FO reductions too, a plain reduction being an ordered one.

Non-reducibility

theorem DescriptiveComplexity.not_le_of_not_foDefinable {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (hP : ¬FODefinable P) (hQ : FODefinable Q) : IsEmpty (OrderedFOReduction P Q)

A problem that is not FO(≤)-definable reduces to no problem that is. The contrapositive of DescriptiveComplexity.FODefinable.of_orderedReduction, and the shape in which an inexpressibility result becomes a statement about the reduction order.

theorem DescriptiveComplexity.not_le_of_not_foDefinableFree {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (hP : ¬FODefinableFree P) (hQ : FODefinableFree Q) : IsEmpty (FOReduction P Q)

The order-free twin.