Order-free FO(IFP) does not capture PTIME

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

proven

Loading review…

Natural Language Statement

Theorem

EVEN is not order-free FO(IFP) definable: an inflationary induction with variable budget $k$ cannot separate two bare sets with at least $k$ elements, by the $k$ -pebble game. EVEN being in PTIME, the inflationary fixed-point logic without an order does not capture polynomial time; the order in the capture theorems is necessary.

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 `even_not_ifpDefinableFree` proven

no assumptions

thm✓Lax945089.OrderFreeInductionMissesPTIME (1st statement)

⊢Lax945089Proofs.Bridge.even_not_ifpDefinableFree

2 `exists_mem_PTIME_not_ifpDefinableFree` proven

- thm✓Lax945089.FirstOrderBelowTransitiveClosure
- thm✓Lax945089.OrderFreeInductionMissesPTIME
→
thm✓Lax945089.OrderFreeInductionMissesPTIME (2nd statement)
⊢Lax945089Proofs.Bridge.exists_mem_PTIME_not_ifpDefinableFree

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: Order-free FO(IFP) does not capture PTIME
28	type: theorem
29	---
30	EVEN is not order-free FO(IFP) definable: an inflationary induction with
31	variable budget $k$ cannot separate two bare sets with at least $k$
32	elements, by the $k$ -pebble game. EVEN being in PTIME, the inflationary
33	fixed-point logic without an order does not capture polynomial time; the
34	order in the capture theorems is necessary.
35	-/
36
37	namespace Lax945089.OrderFreeInductionMissesPTIME
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	/-- EVEN is not order-free FO(IFP) definable. -/
51	axiom even_not_ifpDefinableFree : ¬IFPDefinableFree EVEN
52
53	/-- Some problem of PTIME is not order-free FO(IFP) definable. -/
54	axiom exists_mem_PTIME_not_ifpDefinableFree :
55	∃ P : DecisionProblem Language.empty, PTIME.Mem P ∧ ¬IFPDefinableFree P
56
57	end Lax945089.OrderFreeInductionMissesPTIME
58

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

Order-free FO(IFP) does not capture PTIME

Flags

Flag this concept

Natural Language Statement

Theorem

1 `even_not_ifpDefinableFree` proven

2 `exists_mem_PTIME_not_ifpDefinableFree` proven

Lean source view on GitHub

Discussion

Settings

Your comments

Order-free FO(IFP) does not capture PTIME

Natural Language Statement

Theorem

1 even_not_ifpDefinableFree proven

2 exists_mem_PTIME_not_ifpDefinableFree proven

Lean source view on GitHub

Discussion

1 `even_not_ifpDefinableFree` proven

2 `exists_mem_PTIME_not_ifpDefinableFree` proven