Proof of `Local formulas are evaluated in any superset of the ball`
groundedproofs/Lax185574Proofs/LocalSubstructure.lean · lax-185574
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
In the paper
- page 62 of this submission's paper
Description
An -local formula holds of a tuple in a structure if and only if it holds of the tuple in an induced substructure that contains the ball of radius around the tuple. The quantifiers of the formula are guarded by balls of radius at most around the tuple, and these balls are the same in the structure and in the substructure, since a walk of length at most from the tuple uses only relation tuples whose entries lie in the ball.