Possible worlds

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

definition

Loading review…

Natural Language Statement

Definition

An instance over a schema $L$ is a structure over two copies of $L$ : the certain facts and the uncertain ones. A possible world keeps every certain fact and some of the uncertain ones, and is read as an $L$ -structure. For a sentence $\varphi$ of the schema, counting possible worlds is the counting problem whose value on an instance is the number of its possible worlds in which $\varphi$ holds; with every uncertain fact present with probability $1/2$ , this number divided by the number of worlds is the probability of $\varphi$ .

Concept map

6 concepts; 9 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.BigOperators.Ring.Finset
2	import Mathlib.Algebra.Order.BigOperators.Group.Finset
3	import Mathlib.Data.Fintype.BigOperators
4	import Mathlib.SetTheory.Cardinal.Finite
5	import Mathlib.Algebra.Group.Action.Defs
6	import Mathlib.Tactic.Ring
7	import Mathlib.Tactic.FinCases
8	import Mathlib.Order.PiLex
9	import Mathlib.Data.Prod.Lex
10	import Mathlib.Data.Fintype.EquivFin
11	import Mathlib.ModelTheory.Order
12	import Mathlib.ModelTheory.Semantics
13	import Mathlib.ModelTheory.Complexity
14	import Mathlib.Logic.Equiv.Fin.Basic
15	import Mathlib.Data.Fintype.Lattice
16	import Mathlib.Data.Finite.Sigma
17	import Mathlib.Order.Lattice.Nat
18	import Mathlib.Data.Set.Card
19	import Mathlib.Data.Fintype.Pigeonhole
20	import Mathlib.Dynamics.FixedPoints.Basic
21	import Mathlib.ModelTheory.Syntax
22	import Mathlib.Data.Fintype.Card
23	import Lax904597.SecondOrder
24	import Lax366625.CountingProblems
25
26	/-!
27	---
28	title: Possible worlds
29	type: definition
30	---
31	An instance over a schema $L$ is a structure over two copies of $L$ : the
32	certain facts and the uncertain ones. A possible world keeps every certain
33	fact and some of the uncertain ones, and is read as an $L$ -structure. For a
34	sentence $\varphi$ of the schema, counting possible worlds is the counting
35	problem whose value on an instance is the number of its possible worlds in
36	which $\varphi$ holds; with every uncertain fact present with probability
37	$1/2$ , this number divided by the number of worlds is the probability of
38	$\varphi$ .
39	-/
40
41	namespace Lax794877.PossibleWorlds
42
43	open Lax904597.SecondOrder
44
45	open FirstOrder
46
47	open Language Structure
48
49	variable (L : Language.{0, 0})
50
51	/-- The block guessing a world: one relation variable per relation symbol of
52	the schema, of the same arity. -/
53	def worldBlock [Finite (Σ n, L.Relations n)] : SOBlock where
54	ι := Σ n, L.Relations n
55	arity := fun p => p.1
56
57	section Worlds
58
59	variable {L} [Finite (Σ n, L.Relations n)] {A : Type}
60
61	/-- The structure over the schema that a family of relations is. -/
62	@[reducible]
63	def worldStructure [L.IsRelational] (ρ : (worldBlock L).Assignment A) : L.Structure A where
64	funMap f := isEmptyElim f
65	RelMap := fun {n} R x => ρ ⟨n, R⟩ x
66
67	/-- The family of relations `ρ` is a possible world of the instance: it
68	contains every certain fact, and only certain or uncertain facts. -/
69	def IsWorld [(L.sum L).Structure A] (ρ : (worldBlock L).Assignment A) : Prop :=
70	∀ (p : Σ n, L.Relations n) (x : Fin p.1 → A),
71	(RelMap (L := L.sum L) (M := A) (Sum.inl p.2) x → ρ p x) ∧
72	(ρ p x → RelMap (L := L.sum L) (M := A) (Sum.inl p.2) x ∨
73	RelMap (L := L.sum L) (M := A) (Sum.inr p.2) x)
74
75	/-- A fact that is uncertain and not certain: the facts a world is free to
76	keep or to drop. -/
77	def IsOpenFact [(L.sum L).Structure A] (q : Σ p : Σ n, L.Relations n, Fin p.1 → A) : Prop :=
78	RelMap (L := L.sum L) (M := A) (Sum.inr q.1.2) q.2 ∧
79	¬RelMap (L := L.sum L) (M := A) (Sum.inl q.1.2) q.2
80
81	end Worlds
82
83	open Lax366625.CountingProblems
84
85	/-- Counting possible worlds: the number of possible worlds of the instance
86	in which the sentence `φ` of the schema holds. -/
87	noncomputable def PossibleWorlds {L : Language.{0, 0}} [Finite
88	(Σ n, L.Relations n)] [L.IsRelational]
89	(φ : L.Sentence) : CountingProblem (L.sum L) :=
90	CountingProblem.ofFun fun A _ =>
91	Nat.card {ρ : (worldBlock L).Assignment A // IsWorld ρ ∧ @Sentence.Realize L A
92	(worldStructure ρ) φ}
93
94	end Lax794877.PossibleWorlds
95

Builds on

Used by

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

Possible worlds

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments