Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Counting possible worlds is in #P

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

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    For every first-order sentence of the schema, counting its possible worlds and counting its weighted possible worlds are in #P: a world is a choice of one relation per symbol of the schema, and a weighted witness adds the numbers below the weights, both guessed by an existential second-order sentence.

    Concept map
    23 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 possibleWorlds_mem_sharpP proven

    2 weightedWorlds_mem_sharpP proven

    Lean source view on GitHub

    1import Lax366625.CountingClasses
    2import Lax366625.CountingProblems
    3import Lax366625.QuantitativeLogic
    4import Lax366625.WitnessCounting
    5import Lax799700.Common
    6import Lax859101.OneCallReductions
    7import Lax904597.Machines
    8import Lax904597.SecondOrder
    9import Mathlib.Algebra.BigOperators.Field
    10import Mathlib.Algebra.BigOperators.Fin
    11import Mathlib.Algebra.BigOperators.Finprod
    12import Mathlib.Algebra.BigOperators.Group.Finset.Basic
    13import Mathlib.Algebra.BigOperators.Pi
    14import Mathlib.Algebra.BigOperators.Ring.Finset
    15import Mathlib.Algebra.Group.Action.Defs
    16import Mathlib.Algebra.Order.BigOperators.Group.Finset
    17import Mathlib.Algebra.Order.BigOperators.Ring.Finset
    18import Mathlib.Algebra.Order.Field.Basic
    19import Mathlib.Algebra.Order.Ring.Rat
    20import Mathlib.Data.Finite.Sigma
    21import Mathlib.Data.Finset.Max
    22import Mathlib.Data.Fintype.BigOperators
    23import Mathlib.Data.Fintype.Card
    24import Mathlib.Data.Fintype.EquivFin
    25import Mathlib.Data.Fintype.Lattice
    26import Mathlib.Data.Fintype.Pi
    27import Mathlib.Data.Fintype.Pigeonhole
    28import Mathlib.Data.Fintype.Sort
    29import Mathlib.Data.Nat.Bitwise
    30import Mathlib.Data.Prod.Lex
    31import Mathlib.Data.Set.Card
    32import Mathlib.Data.Set.Finite.Lemmas
    33import Mathlib.Dynamics.FixedPoints.Basic
    34import Mathlib.Logic.Equiv.Fin.Basic
    35import Mathlib.Logic.Equiv.Prod
    36import Mathlib.ModelTheory.Complexity
    37import Mathlib.ModelTheory.Graph
    38import Mathlib.ModelTheory.Order
    39import Mathlib.ModelTheory.Semantics
    40import Mathlib.ModelTheory.Syntax
    41import Mathlib.Order.Hom.Set
    42import Mathlib.Order.Lattice.Nat
    43import Mathlib.Order.PiLex
    44import Mathlib.SetTheory.Cardinal.Finite
    45import Mathlib.Tactic.FieldSimp
    46import Mathlib.Tactic.FinCases
    47import Mathlib.Tactic.Linarith
    48import Mathlib.Tactic.Ring
    49import Lax794877.PossibleWorlds
    50import Lax794877.WeightedWorlds
    51import Lax794877.Queries
    52import Lax794877.ExampleDatabase
    53
    54/-!
    55---
    56title: Counting possible worlds is in #P
    57type: theorem
    58---
    59For every first-order sentence of the schema, counting its possible worlds
    60and counting its weighted possible worlds are in #P: a world is a choice of
    61one relation per symbol of the schema, and a weighted witness adds the
    62numbers below the weights, both guessed by an existential second-order
    63sentence.
    64-/
    65
    66namespace Lax794877.WorldsInSharpP
    67
    68open Lax904597.SecondOrder
    69open FirstOrder
    70open Language Structure
    71open Lax794877.PossibleWorlds Lax799700.Common Lax904597.SecondOrder
    72open FirstOrder.Language
    73open Lax366625.CountingProblems Lax366625.CountingClasses Lax366625.WitnessCounting
    74 Lax366625.QuantitativeLogic
    75open Lax859101.OneCallReductions Lax904597.Machines
    76open Lax794877.PossibleWorlds Lax794877.WeightedWorlds Lax794877.Queries Lax794877.ExampleDatabase
    77
    78/-- Counting possible worlds is in #P. -/
    79axiom possibleWorlds_mem_sharpP :
    80 ∀ {L : Language.{0, 0}} [Finite (Σ n, L.Relations n)] [L.IsRelational]
    81 (φ : L.Sentence), SharpP.Mem (PossibleWorlds φ)
    82
    83/-- Counting weighted possible worlds is in #P. -/
    84axiom weightedWorlds_mem_sharpP :
    85 ∀ {L : Language.{0, 0}} [Finite (Σ n, L.Relations n)] [L.IsRelational]
    86 (φ : L.Sentence), SharpP.Mem (WeightedWorlds φ)
    87
    88end Lax794877.WorldsInSharpP
    89
    Show 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…