First-order logic cannot count: games on bare sets

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

proven

Loading review…

Natural Language Statement

Theorem

Two finite sets with at least $n$ elements each, as structures over the empty vocabulary, are $n$ -round equivalent: the duplicator answers a new element by a new element and an old one by its match. Hence an order-free first-order definable property of bare sets is constant on the sets beyond some size: first-order logic counts up to its quantifier depth and no further.

Concept map

27 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

1 `efEquiv_bare` proven

no assumptions

thm✓Lax945089.GamesOnSets (1st statement)

⊢Lax945089Proofs.Bridge.efEquiv_bare

2 `exists_card_bound_of_foDefinableFree` proven

no assumptions

thm✓Lax945089.GamesOnSets (2nd statement)

⊢Lax945089Proofs.Bridge.exists_card_bound_of_foDefinableFree

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: First-order logic cannot count: games on bare sets
28	type: theorem
29	---
30	Two finite sets with at least $n$ elements each, as structures over the
31	empty vocabulary, are $n$ -round equivalent: the duplicator answers a new
32	element by a new element and an old one by its match. Hence an order-free
33	first-order definable property of bare sets is constant on the sets beyond
34	some size: first-order logic counts up to its quantifier depth and no
35	further.
36	-/
37
38	namespace Lax945089.GamesOnSets
39
40	open FirstOrder FirstOrder.Language
41	open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.SecondOrder
42	open Lax904597.Classes
43	open Lax485149.Problems Lax485149.FirstOrderDefinability Lax485149.TransitiveClosure
44	open Lax485149.DeterministicTransitiveClosure Lax485149.ClassNL Lax485149.ClassL
45	open Lax535992.InflationaryFixedPoint Lax535992.ClassPTIME
46	open Lax134656.PartialFixedPoint Lax895169.ArithmeticLogic
47	open Lax945089.OrderFreeFirstOrder Lax945089.EhrenfeuchtGames Lax945089.PebbleGames
48	open Lax945089.Even Lax945089.Parity
49	open Lax945089.TransitiveClosureReductions
50
51	/-- Two sets with at least `n` elements are `n`-round equivalent. -/
52	axiom efEquiv_bare :
53	∀ {M N : Type} [Language.empty.Structure M] [Language.empty.Structure N] [Finite M] [Finite N]
54	(n : ℕ),
55	n ≤ Nat.card M → n ≤ Nat.card N → EFEquiv Language.empty M N n
56
57	/-- An order-free first-order property of bare sets is eventually constant. -/
58	axiom exists_card_bound_of_foDefinableFree :
59	∀ {P : DecisionProblem Language.empty}, FODefinableFree P →
60	∃ N : ℕ, ∀ (A B : Type) [Language.empty.Structure A] [Language.empty.Structure B] [Finite A]
61	[Finite B]
62	[Nonempty A] [Nonempty B], N ≤ Nat.card A → N ≤ Nat.card B → (P A ↔ P B)
63
64	end Lax945089.GamesOnSets
65

Show ProofShow Proof

Discussion

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

Loading discussion…

Lax Lean Archive

First-order logic cannot count: games on bare sets

Flags

Flag this concept

Natural Language Statement

Theorem

1 `efEquiv_bare` proven

2 `exists_card_bound_of_foDefinableFree` proven

Lean source view on GitHub

Discussion

Settings

Your comments

First-order logic cannot count: games on bare sets

Natural Language Statement

Theorem

1 efEquiv_bare proven

2 exists_card_bound_of_foDefinableFree proven

Lean source view on GitHub

Discussion

1 `efEquiv_bare` proven

2 `exists_card_bound_of_foDefinableFree` proven