PARITY is in L and not first-order definable

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

proven

Loading review…

Natural Language Statement

Theorem

PARITY is in L, by one deterministic walk along the order that carries a bit and flips it at each marked element. It is not FO( $\le$ ) definable: EVEN reduces to it by a first-order reduction that marks every element, and FO( $\le$ ) definability is closed under such reductions. That PARITY is not AC⁰ definable is the switching lemma, which is not proved here.

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: PARITY is in L and not first-order definable
28	type: theorem
29	---
30	PARITY is in L, by one deterministic walk along the order that carries a
31	bit and flips it at each marked element. It is not FO( $\le$ ) definable:
32	EVEN reduces to it by a first-order reduction that marks every element, and
33	FO( $\le$ ) definability is closed under such reductions. That PARITY is not
34	AC⁰ definable is the switching lemma, which is not proved here.
35	-/
36
37	namespace Lax945089.ParityInLogSpace
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	/-- PARITY is in L. -/
51	axiom parity_mem_LOGSPACE : LOGSPACE.Mem PARITY
52
53	/-- EVEN reduces to PARITY by a first-order reduction. -/
54	axiom even_fo_reduction_parity : Nonempty (FOReduction EVEN PARITY)
55
56	/-- PARITY is not FO(≤) definable. -/
57	axiom parity_not_foDefinable : ¬FODefinable PARITY
58
59	end Lax945089.ParityInLogSpace
60

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

PARITY is in L and not first-order definable

Flags

Flag this concept

Natural Language Statement

Theorem

1 `even_fo_reduction_parity` proven

2 `parity_mem_LOGSPACE` proven

3 `parity_not_foDefinable` proven

Lean source view on GitHub

Discussion

Settings