EVEN is not first-order definable, even with an order

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

proven

Loading review…

Natural Language Statement

Theorem

EVEN is not order-free first-order definable, bare sets of different parities being equivalent for any number of rounds once they are large enough; and it is not FO( $\le$ ) definable either, by Ehrenfeucht's theorem on linear orders. An order-free definition is in particular an ordered one.

Concept map

27 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

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: EVEN is not first-order definable, even with an order
28	type: theorem
29	---
30	EVEN is not order-free first-order definable, bare sets of different
31	parities being equivalent for any number of rounds once they are large
32	enough; and it is not FO( $\le$ ) definable either, by Ehrenfeucht's theorem
33	on linear orders. An order-free definition is in particular an ordered
34	one.
35	-/
36
37	namespace Lax945089.EvenNotFirstOrder
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	/-- Every order-free first-order definable problem is FO(≤) definable. -/
51	axiom foDefinableFree_foDefinable :
52	∀ {L : Language.{0, 0}} [L.IsRelational] {P : DecisionProblem L},
53	FODefinableFree P → FODefinable P
54
55	/-- EVEN is not order-free first-order definable. -/
56	axiom even_not_foDefinableFree : ¬FODefinableFree EVEN
57
58	/-- EVEN is not FO(≤) definable. -/
59	axiom even_not_foDefinable : ¬FODefinable EVEN
60
61	end Lax945089.EvenNotFirstOrder
62

Show ProofShow 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

EVEN is not first-order definable, even with an order

Flags

Flag this concept

Natural Language Statement

Theorem

1 `even_not_foDefinable` proven

2 `even_not_foDefinableFree` proven

3 `foDefinableFree_foDefinable` proven

Lean source view on GitHub

Discussion

Settings