The values of the world counts

Lax794877.WorldsValues · concepts/Lax794877/WorldsValues.lean · lax-794877

proven

Loading review…

Natural Language Statement

Lemma

The number of possible worlds of an instance in which a sentence holds, and the number of weighted witnesses of the worlds in which it holds, are invariant under isomorphism of instances, so they are the values of the two counting problems.

Concept map

23 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

Lean source view on GitHub

Show types on hover

1	import Lax366625.CountingClasses
2	import Lax366625.CountingProblems
3	import Lax366625.QuantitativeLogic
4	import Lax366625.WitnessCounting
5	import Lax799700.Common
6	import Lax859101.OneCallReductions
7	import Lax904597.Machines
8	import Lax904597.SecondOrder
9	import Mathlib.Algebra.BigOperators.Field
10	import Mathlib.Algebra.BigOperators.Fin
11	import Mathlib.Algebra.BigOperators.Finprod
12	import Mathlib.Algebra.BigOperators.Group.Finset.Basic
13	import Mathlib.Algebra.BigOperators.Pi
14	import Mathlib.Algebra.BigOperators.Ring.Finset
15	import Mathlib.Algebra.Group.Action.Defs
16	import Mathlib.Algebra.Order.BigOperators.Group.Finset
17	import Mathlib.Algebra.Order.BigOperators.Ring.Finset
18	import Mathlib.Algebra.Order.Field.Basic
19	import Mathlib.Algebra.Order.Ring.Rat
20	import Mathlib.Data.Finite.Sigma
21	import Mathlib.Data.Finset.Max
22	import Mathlib.Data.Fintype.BigOperators
23	import Mathlib.Data.Fintype.Card
24	import Mathlib.Data.Fintype.EquivFin
25	import Mathlib.Data.Fintype.Lattice
26	import Mathlib.Data.Fintype.Pi
27	import Mathlib.Data.Fintype.Pigeonhole
28	import Mathlib.Data.Fintype.Sort
29	import Mathlib.Data.Nat.Bitwise
30	import Mathlib.Data.Prod.Lex
31	import Mathlib.Data.Set.Card
32	import Mathlib.Data.Set.Finite.Lemmas
33	import Mathlib.Dynamics.FixedPoints.Basic
34	import Mathlib.Logic.Equiv.Fin.Basic
35	import Mathlib.Logic.Equiv.Prod
36	import Mathlib.ModelTheory.Complexity
37	import Mathlib.ModelTheory.Graph
38	import Mathlib.ModelTheory.Order
39	import Mathlib.ModelTheory.Semantics
40	import Mathlib.ModelTheory.Syntax
41	import Mathlib.Order.Hom.Set
42	import Mathlib.Order.Lattice.Nat
43	import Mathlib.Order.PiLex
44	import Mathlib.SetTheory.Cardinal.Finite
45	import Mathlib.Tactic.FieldSimp
46	import Mathlib.Tactic.FinCases
47	import Mathlib.Tactic.Linarith
48	import Mathlib.Tactic.Ring
49	import Lax794877.PossibleWorlds
50	import Lax794877.WeightedWorlds
51	import Lax794877.Queries
52	import Lax794877.ExampleDatabase
53
54	/-!
55	---
56	title: The values of the world counts
57	type: lemma
58	---
59	The number of possible worlds of an instance in which a sentence holds, and
60	the number of weighted witnesses of the worlds in which it holds, are
61	invariant under isomorphism of instances, so they are the values of the two
62	counting problems.
63	-/
64
65	namespace Lax794877.WorldsValues
66
67	open Lax904597.SecondOrder
68	open FirstOrder
69	open Language Structure
70	open Lax794877.PossibleWorlds Lax799700.Common Lax904597.SecondOrder
71	open FirstOrder.Language
72	open Lax366625.CountingProblems Lax366625.CountingClasses Lax366625.WitnessCounting
73	Lax366625.QuantitativeLogic
74	open Lax859101.OneCallReductions Lax904597.Machines
75	open Lax794877.PossibleWorlds Lax794877.WeightedWorlds Lax794877.Queries Lax794877.ExampleDatabase
76
77	/-- The number of possible worlds satisfying a sentence is isomorphism-invariant. -/
78	axiom possibleWorlds_count_iso :
79	∀ {L : Language.{0, 0}} [Finite (Σ n, L.Relations n)] [L.IsRelational] (φ : L.Sentence)
80	{A B : Type}
81	[(L.sum L).Structure A] [(L.sum L).Structure B], (A ≃[L.sum L] B) →
82	Nat.card {ρ : (worldBlock L).Assignment A // IsWorld ρ ∧ @Sentence.Realize L A
83	(worldStructure ρ) φ} =
84	Nat.card {ρ : (worldBlock L).Assignment B // IsWorld ρ ∧ @Sentence.Realize L B
85	(worldStructure ρ) φ}
86
87	/-- The value of counting possible worlds is the number it counts. -/
88	axiom possibleWorlds_eq :
89	∀ {L : Language.{0, 0}} [Finite (Σ n, L.Relations n)] [L.IsRelational] (φ : L.Sentence)
90	(A : Type) [(L.sum L).Structure A],
91	PossibleWorlds φ A = Nat.card {ρ :
92	(worldBlock L).Assignment A // IsWorld ρ ∧ @Sentence.Realize L A (worldStructure ρ) φ}
93
94	/-- The number of weighted witnesses is isomorphism-invariant. -/
95	axiom weightedWorlds_count_iso :
96	∀ {L : Language.{0, 0}} [Finite (Σ n, L.Relations n)] [L.IsRelational] (φ : L.Sentence)
97	{A B : Type}
98	[(weightedLang L).Structure A] [(weightedLang L).Structure B], (A ≃[weightedLang L] B) →
99	Nat.card {σ : (weightBlock L).Assignment A // IsLinOrd (WLe L A) ∧
100	(∀ (p : Σ n, L.Relations n) (x : Fin p.1 → A), WeightCond σ p x) ∧
101	@Sentence.Realize L A (worldStructure (worldOf σ)) φ} =
102	Nat.card {σ : (weightBlock L).Assignment B // IsLinOrd (WLe L B) ∧
103	(∀ (p : Σ n, L.Relations n) (x : Fin p.1 → B), WeightCond σ p x) ∧
104	@Sentence.Realize L B (worldStructure (worldOf σ)) φ}
105
106	/-- The value of counting weighted possible worlds is the number it counts. -/
107	axiom weightedWorlds_eq :
108	∀ {L : Language.{0, 0}} [Finite (Σ n, L.Relations n)] [L.IsRelational] (φ : L.Sentence)
109	(A : Type) [(weightedLang L).Structure A],
110	WeightedWorlds φ A = Nat.card {σ : (weightBlock L).Assignment A // IsLinOrd (WLe L A) ∧
111	(∀ (p : Σ n, L.Relations n) (x : Fin p.1 → A), WeightCond σ p x) ∧
112	@Sentence.Realize L A (worldStructure (worldOf σ)) φ}
113
114	end Lax794877.WorldsValues
115

Show ProofShow ProofShow ProofShow Proof

Builds on

Used by

none

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

The values of the world counts

Flags

Flag this concept

Natural Language Statement

Lemma

1 `possibleWorlds_count_iso` proven

2 `possibleWorlds_eq` proven

3 `weightedWorlds_count_iso` proven

4 `weightedWorlds_eq` proven

Lean source view on GitHub

Discussion

Settings