Ehrenfeucht’s theorem on linear orders

Lax945089.GamesOnLinearOrders · concepts/Lax945089/GamesOnLinearOrders.lean · lax-945089

proven

Loading review…

Natural Language Statement

Theorem

Two finite linear orders with at least $2^n$ elements each are $n$ -round equivalent, as structures over the vocabulary of the order. The duplicator maintains that the distances between pebbled points, the two ends of the order included, are equal up to truncation at a threshold that halves at each round.

Concept map

27 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax945089.GamesOnLinearOrders

⊢Lax945089Proofs.Bridge.efEquiv_linearOrder

Lean source view on GitHub

Show types on hover

1	import Mathlib.ModelTheory.Order
2	import Mathlib.Order.Defs.LinearOrder
3	import Lax904597.Problems
4	import Lax904597.Interpretations
5	import Lax904597.Relativized
6	import Lax904597.SecondOrder
7	import Lax904597.Classes
8	import Lax485149.Problems
9	import Lax485149.FirstOrderDefinability
10	import Lax485149.TransitiveClosure
11	import Lax485149.DeterministicTransitiveClosure
12	import Lax485149.ClassNL
13	import Lax485149.ClassL
14	import Lax535992.InflationaryFixedPoint
15	import Lax535992.ClassPTIME
16	import Lax134656.PartialFixedPoint
17	import Lax895169.ArithmeticLogic
18	import Lax945089.OrderFreeFirstOrder
19	import Lax945089.EhrenfeuchtGames
20	import Lax945089.PebbleGames
21	import Lax945089.Even
22	import Lax945089.Parity
23	import Lax945089.TransitiveClosureReductions
24
25	/-!
26	---
27	title: Ehrenfeucht’s theorem on linear orders
28	type: theorem
29	---
30	Two finite linear orders with at least $2^n$ elements each are $n$ -round
31	equivalent, as structures over the vocabulary of the order. The duplicator
32	maintains that the distances between pebbled points, the two ends of the
33	order included, are equal up to truncation at a threshold that halves at
34	each round.
35	-/
36
37	namespace Lax945089.GamesOnLinearOrders
38
39	open FirstOrder FirstOrder.Language
40	open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.SecondOrder
41	open Lax904597.Classes
42	open Lax485149.Problems Lax485149.FirstOrderDefinability Lax485149.TransitiveClosure
43	open Lax485149.DeterministicTransitiveClosure Lax485149.ClassNL Lax485149.ClassL
44	open Lax535992.InflationaryFixedPoint Lax535992.ClassPTIME
45	open Lax134656.PartialFixedPoint Lax895169.ArithmeticLogic
46	open Lax945089.OrderFreeFirstOrder Lax945089.EhrenfeuchtGames Lax945089.PebbleGames
47	open Lax945089.Even Lax945089.Parity
48	open Lax945089.TransitiveClosureReductions
49
50	/-- Two linear orders with at least `2 ^ n` elements are `n`-round equivalent. -/
51	axiom efEquiv_linearOrder :
52	∀ {A B : Type} [Language.empty.Structure A] [Language.empty.Structure B] [LinearOrder A]
53	[LinearOrder B]
54	[Finite A] [Finite B] (n : ℕ), 2 ^ n ≤ Nat.card A → 2 ^ n ≤ Nat.card B →
55	EFEquiv (Language.empty.sum Language.order) A B n
56
57	end Lax945089.GamesOnLinearOrders
58

Show Proof

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Ehrenfeucht’s theorem on linear orders

Flags

Flag this concept

Natural Language Statement

Theorem

Lean source view on GitHub

Discussion

Settings

Your comments