diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,727 +1,728 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod AOT Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory Balog_Szemeredi_Gowers BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel Cook_Levin CRYSTALS-Kyber CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport CHERI-C_Memory_Model Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DPRM_Theorem DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HoareForDivergence HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaNet Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Maximum_Segment_Sum Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multiset_Ordering_NPC Multi_Party_Computation Multirelations Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker Package_logic PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Padic_Field Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma SCC_Bloemen_Sequential Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sophomores_Dream Solidity Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc +Suppes_Theorem Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Turans_Graph_Theorem Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/Suppes_Theorem/Probability_Logic.thy b/thys/Suppes_Theorem/Probability_Logic.thy new file mode 100644 --- /dev/null +++ b/thys/Suppes_Theorem/Probability_Logic.thy @@ -0,0 +1,528 @@ +chapter \ Probability Logic \label{chapter:probability} \ + +theory Probability_Logic + imports + "Propositional_Logic_Class.Classical_Connectives" + HOL.Real + "HOL-Library.Countable" +begin + +no_notation FuncSet.funcset (infixr "\" 60) + +section \ Definition of Probability Logic \label{sec:definition-of-probability-logic} \ + +text \ Probability logic is defined in terms of an operator over + classical logic obeying certain postulates. Scholars often credit + George Boole for first conceiving this kind of formulation @{cite booleChapterXVITheory1853}. + Theodore Hailperin in particular has written extensively on this subject + @{cite hailperinProbabilityLogic1984 + and hailperinBooleLogicProbability1986 + and hailperinSententialProbabilityLogic1996}. \ + +text \ The presentation below roughly follows Kolmogorov's axiomatization + @{cite kolmogoroffChapterElementareWahrscheinlichkeitsrechnung1933}. + A key difference is that we only require \<^emph>\finite additivity\, rather + than \<^emph>\countable additivity\. Finite additivity is also defined in + terms of implication \<^term>\(\)\. \ + +class probability_logic = classical_logic + + fixes \

:: "'a \ real" + assumes probability_non_negative: "\

\ \ 0" + assumes probability_unity: "\ \ \ \

\ = 1" + assumes probability_implicational_additivity: + "\ \ \ \ \ \ \ \

((\ \ \) \ \) = \

\ + \

\" + +text \ A similar axiomatization may be credited to + Rescher @{cite \pg. 185\ rescherManyvaluedLogic1969}. + However, our formulation has fewer axioms. + While Rescher assumes \<^term>\\ \ \ \ \ \

\ = \

\\, we + show this is a lemma in \S\ref{sec:prob-logic-alt-def}. \ + +section \ Why Finite Additivity? \label{section:why-finite-additivity} \ + +text \ In this section we touch on why we have chosen to + employ finite additivity in our axiomatization of + @{class probability_logic} and deviate from conventional + probability theory. \ + +text \ Conventional probability obeys an axiom known as \<^emph>\countable additivity\. + Traditionally it states if \S\ is a countable set of sets which are + pairwise disjoint, then the limit \\ s \ S. \

s\ exists and + \\

(\ S) = (\ s \ S. \

s)\. This is more powerful than our + finite additivity axiom + @{lemma \\ \ \ \ \ \ \ \

((\ \ \) \ \) = \

\ + \

\\ + by (metis probability_implicational_additivity) }. \ + +text \ However, we argue that demanding countable additivity is not practical. \ + +text \ Historically, the statisticians Bruno de Finetti and Leonard Savage + gave the most well known critiques. In @{cite definettiSuiPassaggiLimite1930} + de Finetti shows various properties which are true for countably additive + probability measures may not hold for finitely additive measures. + Savage @{cite savageDifficultiesTheoryPersonal1967}, on the other hand, + develops probability based on choices prizes in lotteries. \ + +text \ We instead argue that if we demand countable additivity, then certain + properties of real world software would no longer be formally verifiable + as we demonstrate here. In particular, it prohibits conventional recursive + data structures for defining propositions. Our argument is derivative of + one given by Giangiacomo Gerla @{cite \Section 3\ gerlaInferencesProbabilityLogic1994}. \ + +text \ By taking equivalence classes modulo \<^term>\\ \ \ . \ \ \ \\, + any classical logic instance gives rise to a Boolean algebra known as + a \<^emph>\Lindenbaum Algebra\. In the case of @{typ "'a classical_propositional_formula"} + this Boolean algebra algebra is both countable and \<^emph>\atomless\. + A theorem of Horn and Tarski @{cite \Theorem 3.2\ hornMeasuresBooleanAlgebras1948} + asserts there can be no countably additive \<^term>\Pr\ for a countable + atomless Boolean algebra. \ + +text \ The above argument is not intended as a blanket refutation of conventional + probability theory. It is simply an impossibility result with respect + to software implementations of probability logic. Plenty of classic results + in probability rely on countable additivity. A nice example, formalized in + Isabelle/HOL, is Bouffon's needle @{cite eberlBuffonNeedleProblem2017}. \ + +section \ Basic Properties of Probability Logic \ + +lemma (in probability_logic) probability_additivity: + assumes "\ \ (\ \ \)" + shows "\

(\ \ \) = \

\ + \

\" + using + assms + unfolding + conjunction_def + disjunction_def + negation_def + by (simp add: probability_implicational_additivity) + +lemma (in probability_logic) probability_alternate_additivity: + assumes "\ \ \ \ \ \" + shows "\

(\ \ \) = \

\ + \

\" + using assms + by (metis + probability_additivity + double_negation_converse + modus_ponens + conjunction_def + negation_def) + +lemma (in probability_logic) complementation: + "\

(\ \) = 1 - \

\" + by (metis + probability_alternate_additivity + probability_unity + bivalence + negation_elimination + add.commute + add_diff_cancel_left') + +lemma (in probability_logic) unity_upper_bound: + "\

\ \ 1" + by (metis + (no_types) + diff_ge_0_iff_ge + probability_non_negative + complementation) + +section \ Alternate Definition of Probability Logic \label{sec:prob-logic-alt-def} \ + +text \ There is an alternate axiomatization of probability logic, + due to Brian Gaines @{cite \pg. 159, postulates P7, P8, and P8\ gainesFuzzyProbabilityUncertainty1978} + and independently formulated by Brian Weatherson @{cite weathersonClassicalIntuitionisticProbability2003}. + As Weatherson notes, this axiomatization is suited to formulating + \<^emph>\intuitionistic\ probability logic. In the case where the underlying + logic is classical the Gaines/Weatherson axiomatization is equivalent + to the traditional Kolmogorov axiomatization from + \S\ref{sec:definition-of-probability-logic}. \ + +class gaines_weatherson_probability = classical_logic + + fixes \

:: "'a \ real" + assumes gaines_weatherson_thesis: + "\

\ = 1" + assumes gaines_weatherson_antithesis: + "\

\ = 0" + assumes gaines_weatherson_monotonicity: + "\ \ \ \ \ \

\ \ \

\" + assumes gaines_weatherson_sum_rule: + "\

\ + \

\ = \

(\ \ \) + \

(\ \ \)" + +sublocale gaines_weatherson_probability \ probability_logic +proof + fix \ + have "\ \ \ \" + by (simp add: ex_falso_quodlibet) + thus "0 \ \

\" + using + gaines_weatherson_antithesis + gaines_weatherson_monotonicity + by fastforce +next + fix \ + assume "\ \" + thus "\

\ = 1" + by (metis + gaines_weatherson_thesis + gaines_weatherson_monotonicity + eq_iff + axiom_k + ex_falso_quodlibet + modus_ponens + verum_def) +next + fix \ \ + assume "\ \ \ \ \ \" + hence "\ \ (\ \ \)" + by (simp add: conjunction_def negation_def) + thus "\

((\ \ \) \ \) = \

\ + \

\" + by (metis + add.commute + add.right_neutral + eq_iff + disjunction_def + ex_falso_quodlibet + negation_def + gaines_weatherson_antithesis + gaines_weatherson_monotonicity + gaines_weatherson_sum_rule) +qed + +lemma (in probability_logic) monotonicity: + "\ \ \ \ \ \

\ \ \

\" +proof - + assume "\ \ \ \" + hence "\ \ (\ \ \ \)" + unfolding negation_def conjunction_def + by (metis + conjunction_def + exclusion_contrapositive_equivalence + negation_def + weak_biconditional_weaken) + hence "\

(\ \ \ \) = \

\ + \

(\ \)" + by (simp add: probability_additivity) + hence "\

\ + \

(\ \) \ 1" + by (metis unity_upper_bound) + hence "\

\ + 1 - \

\ \ 1" + by (simp add: complementation) + thus ?thesis by linarith +qed + +lemma (in probability_logic) biconditional_equivalence: + "\ \ \ \ \ \

\ = \

\" + by (meson + eq_iff + modus_ponens + biconditional_left_elimination + biconditional_right_elimination + monotonicity) + +lemma (in probability_logic) sum_rule: + "\

(\ \ \) + \

(\ \ \) = \

\ + \

\" +proof - + have "\ (\ \ \) \ (\ \ \ \ (\ \ \))" + proof - + have "\ \. \ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\) \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\ \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\))" + unfolding + classical_logic_class.subtraction_def + classical_logic_class.negation_def + classical_logic_class.biconditional_def + classical_logic_class.conjunction_def + classical_logic_class.disjunction_def + by simp + hence "\ \<^bold>\ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\) \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\ \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\)) \<^bold>\" + using propositional_semantics by blast + thus ?thesis by simp + qed + moreover have "\ \ \ (\ \ (\ \ \)) \ \" + proof - + have "\ \. \ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \<^bold>\\\<^bold>\ \ (\<^bold>\\\<^bold>\ \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\)) \ \" + unfolding + classical_logic_class.subtraction_def + classical_logic_class.negation_def + classical_logic_class.biconditional_def + classical_logic_class.conjunction_def + classical_logic_class.disjunction_def + by simp + hence "\ \<^bold>\ \<^bold>\\\<^bold>\ \ (\<^bold>\\\<^bold>\ \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\)) \ \ \<^bold>\" + using propositional_semantics by blast + thus ?thesis by simp + qed + hence "\

(\ \ \) = \

\ + \

(\ \ (\ \ \))" + using + probability_alternate_additivity + biconditional_equivalence + calculation + by auto + moreover have "\ \ \ (\ \ (\ \ \) \ (\ \ \))" + proof - + have "\ \. \ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \<^bold>\\\<^bold>\ \ (\<^bold>\\\<^bold>\ \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\) \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\))" + unfolding + classical_logic_class.subtraction_def + classical_logic_class.negation_def + classical_logic_class.biconditional_def + classical_logic_class.conjunction_def + classical_logic_class.disjunction_def + by auto + hence "\ \<^bold>\ \<^bold>\\\<^bold>\ \ (\<^bold>\\\<^bold>\ \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\) \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\)) \<^bold>\" + using propositional_semantics by + blast + thus ?thesis by simp + qed + moreover have "\ (\ \ (\ \ \)) \ (\ \ \) \ \" + unfolding + subtraction_def + negation_def + conjunction_def + using + conjunction_def + conjunction_right_elimination + by auto + hence "\

\ = \

(\ \ (\ \ \)) + \

(\ \ \)" + using + probability_alternate_additivity + biconditional_equivalence + calculation + by auto + ultimately show ?thesis + by simp +qed + +sublocale probability_logic \ gaines_weatherson_probability +proof + show "\

\ = 1" + by (simp add: probability_unity) +next + show "\

\ = 0" + by (metis + add_cancel_left_right + probability_additivity + ex_falso_quodlibet + probability_unity + bivalence + conjunction_right_elimination + negation_def) +next + fix \ \ + assume "\ \ \ \" + thus "\

\ \ \

\" + using monotonicity + by auto +next + fix \ \ + show "\

\ + \

\ = \

(\ \ \) + \

(\ \ \)" + by (metis sum_rule add.commute) +qed + +sublocale probability_logic \ consistent_classical_logic +proof + show "\ \ \" using probability_unity gaines_weatherson_antithesis by auto +qed + +lemma (in probability_logic) subtraction_identity: + "\

(\ \ \) = \

\ - \

(\ \ \)" +proof - + have "\ \ \ ((\ \ \) \ (\ \ \))" + proof - + have "\ \. \ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \<^bold>\\\<^bold>\ \ ((\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\) \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\))" + unfolding + classical_logic_class.subtraction_def + classical_logic_class.negation_def + classical_logic_class.biconditional_def + classical_logic_class.conjunction_def + classical_logic_class.disjunction_def + by (simp, blast) + hence "\ \<^bold>\ \<^bold>\\\<^bold>\ \ ((\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\) \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\)) \<^bold>\" + using propositional_semantics by blast + thus ?thesis by simp + qed + hence "\

\ = \

((\ \ \) \ (\ \ \))" + using biconditional_equivalence + by simp + moreover have "\ \((\ \ \) \ (\ \ \))" + proof - + have "\ \. \ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \((\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\) \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\))" + unfolding + classical_logic_class.subtraction_def + classical_logic_class.negation_def + classical_logic_class.conjunction_def + classical_logic_class.disjunction_def + by simp + hence "\ \<^bold>\ \((\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\) \ (\<^bold>\\\<^bold>\ \ \<^bold>\\\<^bold>\)) \<^bold>\" + using propositional_semantics by blast + thus ?thesis by simp + qed + ultimately show ?thesis + using probability_additivity + by auto +qed + +section \ Basic Probability Logic Inequality Results \label{sec:basic-probability-inequality-results}\ + +lemma (in probability_logic) disjunction_sum_inequality: + "\

(\ \ \) \ \

\ + \

\" +proof - + have "\

(\ \ \) + \

(\ \ \) = \

\ + \

\" + "0 \ \

(\ \ \)" + by (simp add: sum_rule, simp add: probability_non_negative) + thus ?thesis by linarith +qed + +lemma (in probability_logic) + arbitrary_disjunction_list_summation_inequality: + "\

(\ \) \ (\\\\. \

\)" +proof (induct \) + case Nil + then show ?case by (simp add: gaines_weatherson_antithesis) +next + case (Cons \ \) + have "\

(\ (\ # \)) \ \

\ + \

(\ \)" + using disjunction_sum_inequality + by simp + with Cons have "\

(\ (\ # \)) \ \

\ + (\\\\. \

\)" by linarith + then show ?case by simp +qed + +lemma (in probability_logic) implication_list_summation_inequality: + assumes "\ \ \ \ \" + shows "\

\ \ (\\\\. \

\)" + using + assms + arbitrary_disjunction_list_summation_inequality + monotonicity + order_trans + by blast + +lemma (in probability_logic) arbitrary_disjunction_set_summation_inequality: + "\

(\ \) \ (\\ \ set \. \

\)" + by (metis + arbitrary_disjunction_list_summation_inequality + arbitrary_disjunction_remdups + biconditional_equivalence + sum.set_conv_list) + +lemma (in probability_logic) implication_set_summation_inequality: + assumes "\ \ \ \ \" + shows "\

\ \ (\\ \ set \. \

\)" + using + assms + arbitrary_disjunction_set_summation_inequality + monotonicity + order_trans + by blast + +section \ Dirac Measures \label{sec:dirac-measures}\ + +text \ Before presenting \<^emph>\Dirac measures\ in probability logic, we first + give the set of all functions satisfying probability logic.\ + +definition (in classical_logic) probabilities :: "('a \ real) set" + where "probabilities = + {\

. class.probability_logic (\ \. \ \) (\) \ \

}" + +text \ Traditionally, a Dirac measure is a function \<^term>\\\<^sub>x\ where + \<^term>\\\<^sub>x(S) = (1::real)\ if \<^term>\x \ S\ and \<^term>\\\<^sub>x(S) = (0::real)\ + otherwise. This means that Dirac measures correspond to special + ultrafilters on their underlying \<^term>\\\-algebra which are + closed under countable unions. \ + +text \ Probability logic, as discussed in \S\ref{section:why-finite-additivity}, + may not have countable joins in its underlying logic. In the setting + of probability logic, Dirac measures are simple probability functions + that are either 0 or 1. \ + +definition (in classical_logic) dirac_measures :: "('a \ real) set" + where "dirac_measures = + { \

. class.probability_logic (\ \. \ \) (\) \ \

+ \ (\x. \

x = 0 \ \

x = 1) }" + +lemma (in classical_logic) dirac_measures_subset: + "dirac_measures \ probabilities" + unfolding + probabilities_def + dirac_measures_def + by fastforce + +text \ Maximally consistent sets correspond to Dirac measures. One direction + of this correspondence is established below. \ + +lemma (in classical_logic) MCS_dirac_measure: + assumes "MCS \" + shows "(\ \. if \\\ then (1 :: real) else 0) \ dirac_measures" + (is "?\

\ dirac_measures") +proof - + have "class.probability_logic (\ \. \ \) (\) \ ?\

" + proof (standard, simp, + meson + assms + formula_maximally_consistent_set_def_reflection + maximally_consistent_set_def + set_deduction_weaken) + fix \ \ + assume "\ \ \ \ \ \" + hence "\ \ \ \ \" + by (metis + assms + formula_consistent_def + formula_maximally_consistent_set_def_def + maximally_consistent_set_def + conjunction_def + set_deduction_modus_ponens + set_deduction_reflection + set_deduction_weaken) + hence "\ \ \ \ \ \ \" + using + assms + formula_maximally_consistent_set_def_reflection + maximally_consistent_set_def + conjunction_set_deduction_equivalence + by meson + have "\ \ \ \ \ = (\ \ \ \ \ \ \)" + by (metis + \\ \ \ \ \\ + assms + formula_maximally_consistent_set_def_implication + maximally_consistent_set_def + conjunction_def + disjunction_def) + have "?\

(\ \ \) = ?\

\ + ?\

\" + proof (cases "\ \ \ \ \") + case True + hence \: "1 = ?\

(\ \ \)" by simp + show ?thesis + proof (cases "\ \ \") + case True + hence "\ \ \" + using \\ \ \ \ \ \ \\ + by blast + have "?\

(\ \ \) = (1::real)" using \ by simp + also have "... = 1 + (0::real)" by linarith + also have "... = ?\

\ + ?\

\" + using \\ \ \\ \\ \ \\ by simp + finally show ?thesis . + next + case False + hence "\ \ \" + using \\ \ \ \ \\ \(\ \ \ \ \) = (\ \ \ \ \ \ \)\ + by blast + have "?\

(\ \ \) = (1::real)" using \ by simp + also have "... = (0::real) + 1" by linarith + also have "... = ?\

\ + ?\

\" + using \\ \ \\ \\ \ \\ by simp + finally show ?thesis . + qed + next + case False + moreover from this have "\ \ \" "\ \ \" + using \(\ \ \ \ \) = (\ \ \ \ \ \ \)\ by blast+ + ultimately show ?thesis by simp + qed + thus "?\

((\ \ \) \ \) = ?\

\ + ?\

\" + unfolding disjunction_def . + qed + thus ?thesis + unfolding dirac_measures_def + by simp +qed + +notation FuncSet.funcset (infixr "\" 60) + +end diff --git a/thys/Suppes_Theorem/ROOT b/thys/Suppes_Theorem/ROOT new file mode 100644 --- /dev/null +++ b/thys/Suppes_Theorem/ROOT @@ -0,0 +1,14 @@ +chapter AFP + +session Suppes_Theorem (AFP) = "HOL" + + options [timeout = 600] + sessions + "HOL-Combinatorics" + "HOL-Library" + Propositional_Logic_Class + theories + Probability_Logic + Suppes_Theorem + document_files + "root.tex" + "root.bib" diff --git a/thys/Suppes_Theorem/Suppes_Theorem.thy b/thys/Suppes_Theorem/Suppes_Theorem.thy new file mode 100644 --- /dev/null +++ b/thys/Suppes_Theorem/Suppes_Theorem.thy @@ -0,0 +1,597 @@ +chapter \ Suppes' Theorem \label{sec:suppes-theorem} \ + +theory Suppes_Theorem + imports Probability_Logic +begin + +no_notation FuncSet.funcset (infixr "\" 60) + +text \ An elementary completeness theorem for inequalities for probability logic + is due to Patrick Suppes @{cite suppesProbabilisticInferenceConcept1966}. \ + +text \ A consequence of this Suppes' theorem is an elementary form of \<^emph>\collapse\, + which asserts that inequalities for probabilities are logically + equivalent to the more restricted class of \<^emph>\Dirac measures\ as + defined in \S\ref{sec:dirac-measures}. \ + +section \ Suppes' List Theorem \label{sec:suppes-theorem-for-lists} \ + +text \ We first establish Suppes' theorem for lists of propositions. This + is done by establishing our first completeness theorem using + \<^emph>\Dirac measures\. \ + +text \ First, we use the result from \S\ref{sec:basic-probability-inequality-results} + that shows \\ \ \ \ \\ implies \\

\ \ (\\\\. \

\)\. + This can be understood as a \<^emph>\soundness\ result. \ + +text \ To show completeness, assume \\ \ \ \ \ \\. From this + obtain a maximally consistent \<^term>\\\ such that \\ \ \ \ \ \\. + We then define \<^term>\\ \ = (if (\ \ \) then 1 else 0)\ and + show \<^term>\\\ is a \<^emph>\Dirac measure\ such that \\ \ \ (\\\\. \ \)\. \ + +lemma (in classical_logic) dirac_list_summation_completeness: + "(\ \ \ dirac_measures. \ \ \ (\\\\. \ \)) = \ \ \ \ \" +proof - + { + fix \ :: "'a \ real" + assume "\ \ dirac_measures" + from this interpret probability_logic "(\ \. \ \)" "(\)" "\" "\" + unfolding dirac_measures_def + by auto + assume "\ \ \ \ \" + hence "\ \ \ (\\\\. \ \)" + using implication_list_summation_inequality + by auto + } + moreover { + assume "\ \ \ \ \ \" + from this obtain \ where \: + "MCS \" + "\ \ \" + "\ \ \ \" + by (meson + insert_subset + formula_consistent_def + formula_maximal_consistency + formula_maximally_consistent_extension + formula_maximally_consistent_set_def_def + set_deduction_base_theory + set_deduction_reflection + set_deduction_theorem) + hence"\ \ \ set \. \ \ \" + using arbitrary_disjunction_exclusion_MCS by blast + define \ where "\ = (\ \ . if \\\ then (1 :: real) else 0)" + from \\ \ \ set \. \ \ \\ have "(\\\\. \ \) = 0" + unfolding \_def + by (induct \, simp, simp) + hence "\ \ \ \ (\\\\. \ \)" + unfolding \_def + by (simp add: \(2)) + hence + "\ \ \ dirac_measures. \ (\ \ \ (\\\\. \ \))" + unfolding \_def + using \(1) MCS_dirac_measure by auto + } + ultimately show ?thesis by blast +qed + +theorem (in classical_logic) list_summation_completeness: + "(\ \

\ probabilities. \

\ \ (\\\\. \

\)) = \ \ \ \ \" + (is "?lhs = ?rhs") +proof + assume ?lhs + hence "\ \ \ dirac_measures. \ \ \ (\\\\. \ \)" + unfolding dirac_measures_def probabilities_def + by blast + thus ?rhs + using dirac_list_summation_completeness by blast +next + assume ?rhs + show ?lhs + proof + fix \

:: "'a \ real" + assume "\

\ probabilities" + from this interpret probability_logic "(\ \. \ \)" "(\)" \ \

+ unfolding probabilities_def + by auto + show "\

\ \ (\\\\. \

\)" + using \?rhs\ implication_list_summation_inequality + by simp + qed +qed + +text \ The collapse theorem asserts that to prove an inequalities for all + probabilities in probability logic, one only needs to consider the + case of functions which take on values of 0 or 1. \ + +lemma (in classical_logic) suppes_collapse: + "(\ \

\ probabilities. \

\ \ (\\\\. \

\)) + = (\ \ \ dirac_measures. \ \ \ (\\\\. \ \))" + by (simp add: + dirac_list_summation_completeness + list_summation_completeness) + +lemma (in classical_logic) probability_member_neg: + fixes \

+ assumes "\

\ probabilities" + shows "\

(\ \) = 1 - \

\" +proof - + from assms interpret probability_logic "(\ \. \ \)" "(\)" \ \

+ unfolding probabilities_def + by auto + show ?thesis + by (simp add: complementation) +qed + +text \ Suppes' theorem has a philosophical interpretation. + It asserts that if \<^term>\\ :\ \\, then our \<^emph>\uncertainty\ + in \<^term>\\\ is bounded above by our uncertainty in \<^term>\\\. + Here the uncertainty in the proposition \<^term>\\\ is \1 - \

\\. + Our uncertainty in \<^term>\\\, on the other hand, is + \\\\\. 1 - \

\\. \ + +theorem (in classical_logic) suppes_list_theorem: + "\ :\ \ = (\ \

\ probabilities. (\\\\. 1 - \

\) \ 1 - \

\)" +proof - + have + "\ :\ \ = (\ \

\ probabilities. (\\ \ \<^bold>\ \. \

\) \ \

(\ \))" + using + list_summation_completeness + weak_biconditional_weaken + contra_list_curry_uncurry + list_deduction_def + by blast + moreover have + "\ \

\ probabilities. (\\ \ (\<^bold>\ \). \

\) = (\\ \ \. \

(\ \))" + by (induct \, auto) + ultimately show ?thesis + using probability_member_neg + by (induct \, simp+) +qed + +section \ Suppes' Set Theorem \ + +text \ Suppes theorem also obtains for \<^emph>\sets\. \ + +lemma (in classical_logic) dirac_set_summation_completeness: + "(\ \ \ dirac_measures. \ \ \ (\\\ set \. \ \)) = \ \ \ \ \" + by (metis + dirac_list_summation_completeness + modus_ponens + arbitrary_disjunction_remdups + biconditional_left_elimination + biconditional_right_elimination + hypothetical_syllogism + sum.set_conv_list) + +theorem (in classical_logic) set_summation_completeness: + "(\ \ \ probabilities. \ \ \ (\\\ set \. \ \)) = \ \ \ \ \" + by (metis + dirac_list_summation_completeness + dirac_set_summation_completeness + list_summation_completeness + sum.set_conv_list) + +lemma (in classical_logic) suppes_set_collapse: + "(\ \

\ probabilities. \

\ \ (\\ \ set \. \

\)) + = (\ \ \ dirac_measures. \ \ \ (\\ \ set \. \ \))" + by (simp add: + dirac_set_summation_completeness + set_summation_completeness) + +text \ In our formulation of logic, there is not reason that \\ a = \ b\ + while \<^term>\a \ b\. As a consequence the Suppes theorem + for sets presented below is different than the one given in + \S\ref{sec:suppes-theorem-for-lists}. \ + +theorem (in classical_logic) suppes_set_theorem: + "\ :\ \ + = (\ \

\ probabilities. (\\ \ set (\<^bold>\ \). \

\) \ 1 - \

\)" +proof - + have "\ :\ \ + = (\ \

\ probabilities. (\\ \ set (\<^bold>\ \). \

\) \ \

(\ \))" + using + contra_list_curry_uncurry + list_deduction_def + set_summation_completeness + weak_biconditional_weaken + by blast + thus ?thesis + using probability_member_neg + by (induct \, auto) +qed + +section \ Converse Suppes' Theorem \ + +text \ A formulation of the converse of Suppes' theorem obtains + for lists/sets of \<^emph>\logically disjoint\ propositions. \ + +lemma (in probability_logic) exclusive_sum_list_identity: + assumes "\ \ \" + shows "\

(\ \) = (\\\\. \

\)" + using assms +proof (induct \) + case Nil + then show ?case + by (simp add: gaines_weatherson_antithesis) +next + case (Cons \ \) + assume "\ \ (\ # \)" + hence "\ \ (\ \ \ \)" "\ \ \" by simp+ + hence "\

(\(\ # \)) = \

\ + \

(\ \)" + "\

(\ \) = (\\\\. \

\)" + using Cons.hyps probability_additivity by auto + hence "\

(\(\ # \)) = \

\ + (\\\\. \

\)" by auto + thus ?case by simp +qed + +lemma sum_list_monotone: + fixes f :: "'a \ real" + assumes "\ x. f x \ 0" + and "set \ \ set \" + and "distinct \" + shows "(\\\\. f \) \ (\\\\. f \)" + using assms +proof - + assume "\ x. f x \ 0" + have "\\. set \ \ set \ + \ distinct \ + \ (\\\\. f \) \ (\\\\. f \)" + proof (induct \) + case Nil + then show ?case by simp + next + case (Cons \ \) + { + fix \ + assume "set \ \ set (\ # \)" + and "distinct \" + have "(\\\\. f \) \ (\\'\(\ # \). f \')" + proof - + { + assume "\ \ set \" + with \set \ \ set (\ # \)\ have "set \ \ set \" by auto + hence "(\\\\. f \) \ (\\\\. f \)" + using Cons.hyps \distinct \\ by auto + moreover have "f \ \ 0" using \\ x. f x \ 0\ by metis + ultimately have ?thesis by simp + } + moreover + { + assume "\ \ set \" + hence "set \ = insert \ (set (removeAll \ \))" + by auto + with \set \ \ set (\ # \)\ have "set (removeAll \ \) \ set \" + by (metis + insert_subset + list.simps(15) + set_removeAll + subset_insert_iff) + moreover from \distinct \\ have "distinct (removeAll \ \)" + by (meson distinct_removeAll) + ultimately have "(\\\(removeAll \ \). f \) \ (\\\\. f \)" + using Cons.hyps + by simp + moreover from \\ \ set \\ \distinct \\ + have "(\\\\. f \) = f \ + (\\\(removeAll \ \). f \)" + using distinct_remove1_removeAll sum_list_map_remove1 + by fastforce + ultimately have ?thesis using \\ x. f x \ 0\ + by simp + } + ultimately show ?thesis by blast + qed + } + thus ?case by blast + qed + moreover assume "set \ \ set \" and "distinct \" + ultimately show ?thesis by blast +qed + +lemma count_remove_all_sum_list: + fixes f :: "'a \ real" + shows "real (count_list xs x) * f x + (\x'\(removeAll x xs). f x') + = (\x\xs. f x)" + by (induct xs, simp, simp, metis combine_common_factor mult_cancel_right1) + +lemma (in classical_logic) dirac_exclusive_implication_completeness: + "(\ \ \ dirac_measures. (\\\\. \ \) \ \ \) = (\ \ \ \ \ \ \ \ \)" +proof - + { + fix \ + assume "\ \ dirac_measures" + from this interpret probability_logic "(\ \. \ \)" "(\)" "\" "\" + unfolding dirac_measures_def + by simp + assume "\ \ \" "\ \ \ \ \" + hence "(\\\\. \ \) \ \ \" + using exclusive_sum_list_identity monotonicity by fastforce + } + moreover + { + assume "\ \ \ \" + hence "(\ \ \ set \. \ \ \ set \. + \ \ \ \ \ \ \ (\ \ \)) \ (\ \ \ duplicates \. \ \ \ \)" + using exclusive_equivalence set_deduction_base_theory by blast + hence "\ (\ \ \ dirac_measures. (\\\\. \ \) \ \ \)" + proof (elim disjE) + assume "\ \ \ set \. \ \ \ set \. \ \ \ \ \ \ \ (\ \ \)" + from this obtain \ and \ + where \\_properties: + "\ \ set \" + "\ \ set \" + "\ \ \" + "\ \ \ (\ \ \)" + by blast + from this obtain \ where \: "MCS \" "\ (\ \ \) \ \" + by (meson + insert_subset + formula_consistent_def + formula_maximal_consistency + formula_maximally_consistent_extension + formula_maximally_consistent_set_def_def + set_deduction_base_theory + set_deduction_reflection + set_deduction_theorem) + let ?\ = "\ \. if \\\ then (1 :: real) else 0" + from \ have "\ \ \" "\ \ \" + by (metis + formula_maximally_consistent_set_def_implication + maximally_consistent_set_def + conjunction_def + negation_def)+ + with \\_properties have + "(\\\[\, \]. ?\ \) = 2" + "set [\, \] \ set \" + "distinct [\, \]" + "\\. ?\ \ \ 0" + by simp+ + hence "(\\\\. ?\ \) \ 2" using sum_list_monotone by metis + hence "\ (\\\\. ?\ \) \ ?\ (\)" by auto + thus ?thesis + using \(1) MCS_dirac_measure + by auto + next + assume "\ \ \ duplicates \. \ \ \ \" + from this obtain \ where \: "\ \ duplicates \" "\ \ \ \" + using + exclusive_equivalence [where \="{}"] + set_deduction_base_theory + by blast + from \ obtain \ where \: "MCS \" "\ \ \ \" + by (meson + insert_subset + formula_consistent_def + formula_maximal_consistency + formula_maximally_consistent_extension + formula_maximally_consistent_set_def_def + set_deduction_base_theory + set_deduction_reflection + set_deduction_theorem) + hence "\ \ \" + using negation_def by auto + let ?\ = "\ \. if \\\ then (1 :: real) else 0" + from \ have "count_list \ \ \ 2" + using duplicates_alt_def [where xs="\"] + by blast + hence "real (count_list \ \) * ?\ \ \ 2" using \\ \ \\ by simp + moreover + { + fix \ + have "(\\\\. ?\ \) \ 0" by (induct \, simp, simp) + } + moreover have "(0::real) + \ (\a\removeAll \ \. if a \ \ then 1 else 0)" + using \\\. 0 \ (\\\\. if \ \ \ then 1 else 0)\ + by presburger + ultimately have "real (count_list \ \) * ?\ \ + + (\ \ \ (removeAll \ \). ?\ \) \ 2" + using \2 \ real (count_list \ \) * (if \ \ \ then 1 else 0)\ + by linarith + hence "(\\\\. ?\ \) \ 2" by (metis count_remove_all_sum_list) + hence "\ (\\\\. ?\ \) \ ?\ (\)" by auto + thus ?thesis + using \(1) MCS_dirac_measure + by auto + qed + } + moreover + { + assume "\ \ \ \ \ \" + from this obtain \ \ + where + \: "MCS \" + and \: "\ \ \" + and \: "\ \ set \" "\ \ \" + by (meson + insert_subset + formula_consistent_def + formula_maximal_consistency + formula_maximally_consistent_extension + formula_maximally_consistent_set_def_def + arbitrary_disjunction_exclusion_MCS + set_deduction_base_theory + set_deduction_reflection + set_deduction_theorem) + let ?\ = "\ \. if \\\ then (1 :: real) else 0" + from \ have "(\\\\. ?\ \) \ 1" + proof (induct \) + case Nil + then show ?case by simp + next + case (Cons \' \) + obtain f :: "real list \ real" where f: + "\rs. f rs \ set rs \ \ 0 \ f rs \ 0 \ sum_list rs" + using sum_list_nonneg by moura + moreover have "f (map ?\ \) \ set (map ?\ \) \ 0 \ f (map ?\ \)" + by fastforce + ultimately show ?case + by (simp, metis Cons.hyps Cons.prems(1) \(2) set_ConsD) + qed + hence "\ (\\\\. ?\ \) \ ?\ (\)" using \ by auto + hence "\ (\ \ \ dirac_measures. (\\\\. \ \) \ \ \)" + using \(1) MCS_dirac_measure + by auto + } + ultimately show ?thesis by blast +qed + +theorem (in classical_logic) exclusive_implication_completeness: + "(\ \

\ probabilities. (\\\\. \

\) \ \

\) = (\ \ \ \ \ \ \ \ \)" + (is "?lhs = ?rhs") +proof + assume ?lhs + thus ?rhs + by (meson + dirac_exclusive_implication_completeness + dirac_measures_subset + subset_eq) +next + assume ?rhs + show ?lhs + proof + fix \

:: "'a \ real" + assume "\

\ probabilities" + from this interpret probability_logic "(\ \. \ \)" "(\)" \ \

+ unfolding probabilities_def + by simp + show "(\\\\. \

\) \ \

\" + using + \?rhs\ + exclusive_sum_list_identity + monotonicity + by fastforce + qed +qed + +lemma (in classical_logic) dirac_inequality_completeness: + "(\ \ \ dirac_measures. \ \ \ \ \) = \ \ \ \" +proof - + have "\ \ [\]" + by (simp add: conjunction_right_elimination negation_def) + hence "(\ \ [\] \ \ \ [\] \ \) = \ \ \ \" + by (metis + arbitrary_disjunction.simps(1) + arbitrary_disjunction.simps(2) + disjunction_def implication_equivalence + negation_def + weak_biconditional_weaken) + thus ?thesis + using dirac_exclusive_implication_completeness [where \="[\]"] + by auto +qed + +section \ Implication Inequality Completeness \ + +text \ The following theorem establishes the converse of + \\ \ \ \ \ \

\ \ \

\\, which was + proved in \S\ref{sec:prob-logic-alt-def}. \ + +theorem (in classical_logic) implication_inequality_completeness: + "(\ \

\ probabilities. \

\ \ \

\) = \ \ \ \" +proof - + have "\ \ [\]" + by (simp add: conjunction_right_elimination negation_def) + hence "(\ \ [\] \ \ \ [\] \ \) = \ \ \ \" + by (metis + arbitrary_disjunction.simps(1) + arbitrary_disjunction.simps(2) + disjunction_def implication_equivalence + negation_def + weak_biconditional_weaken) + thus ?thesis + using exclusive_implication_completeness [where \="[\]"] + by simp +qed + +section \ Characterizing Logical Exclusiveness In Probability Logic \ + +text \ Finally, we can say that \\

(\ \) = (\\\\. \

\)\ if and only + if the propositions in \<^term>\\\ are mutually exclusive (i.e. \\ \ \\). + This result also obtains for sets. \ + +lemma (in classical_logic) dirac_exclusive_list_summation_completeness: + "(\ \ \ dirac_measures. \ (\ \) = (\\\\. \ \)) = \ \ \" + by (metis + antisym_conv + dirac_exclusive_implication_completeness + dirac_list_summation_completeness + trivial_implication) + +theorem (in classical_logic) exclusive_list_summation_completeness: + "(\ \

\ probabilities. \

(\ \) = (\\\\. \

\)) = \ \ \" + by (metis + antisym_conv + exclusive_implication_completeness + list_summation_completeness + trivial_implication) + +lemma (in classical_logic) dirac_exclusive_set_summation_completeness: + "(\ \ \ dirac_measures. \ (\ \) = (\\ \ set \. \ \)) + = \ \ (remdups \)" + by (metis + (mono_tags) + eq_iff + dirac_exclusive_implication_completeness + dirac_set_summation_completeness + trivial_implication + set_remdups + sum.set_conv_list eq_iff + dirac_exclusive_implication_completeness + dirac_set_summation_completeness + trivial_implication + set_remdups + sum.set_conv_list + antisym_conv) + +theorem (in classical_logic) exclusive_set_summation_completeness: + "(\ \

\ probabilities. + \

(\ \) = (\\ \ set \. \

\)) = \ \ (remdups \)" + by (metis + (mono_tags, opaque_lifting) + antisym_conv + exclusive_list_summation_completeness + exclusive_implication_completeness + implication_inequality_completeness + set_summation_completeness + order.refl + sum.set_conv_list) + +lemma (in probability_logic) exclusive_list_set_inequality: + assumes "\ \ \" + shows "(\\\\. \

\) = (\\\set \. \

\)" +proof - + have "distinct (remdups \)" using distinct_remdups by auto + hence "duplicates (remdups \) = {}" + by (induct "\", simp+) + moreover have "set (remdups \) = set \" + by (induct "\", simp, simp add: insert_absorb) + moreover have "(\\ \ duplicates \. \ \ \) + \ (\ \ \ set \. \ \ \ set \. (\ \ \) \ \ \ (\ \ \))" + using + assms + exclusive_elimination1 + exclusive_elimination2 + set_deduction_base_theory + by blast + ultimately have + "(\\\duplicates (remdups \). \ \ \) + \ (\ \ \ set (remdups \). \ \ \ set (remdups \). + (\ \ \) \ \ \ (\ \ \))" + by auto + hence "\ \ (remdups \)" + by (meson exclusive_equivalence set_deduction_base_theory) + hence "(\\\set \. \

\) = \

(\ \)" + by (metis + arbitrary_disjunction_remdups + biconditional_equivalence + exclusive_sum_list_identity + sum.set_conv_list) + moreover have "(\\\\. \

\) = \

(\ \)" + by (simp add: assms exclusive_sum_list_identity) + ultimately show ?thesis by metis +qed + +notation FuncSet.funcset (infixr "\" 60) + +end diff --git a/thys/Suppes_Theorem/document/root.bib b/thys/Suppes_Theorem/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Suppes_Theorem/document/root.bib @@ -0,0 +1,632 @@ +@article{birkhoffRingsSets1937, + title = {Rings of Sets}, + author = {Birkhoff, Garrett}, + year = {1937}, + month = sep, + journal = {Duke Mathematical Journal}, + volume = {3}, + number = {3}, + pages = {443--454}, + issn = {0012-7094}, + doi = {10.1215/S0012-7094-37-00334-X}, + file = {/home/mpwd/Zotero/storage/M4UUX5SM/DPubS.html;/home/mpwd/Zotero/storage/UQ4MRUW9/S0012-7094-37-00334-X.html} +} + +@incollection{blackburnSectionCanonicalModels2001, + title = {Section 4.2 {{Canonical Models}}}, + booktitle = {Modal Logic}, + author = {Blackburn, Patrick and {de Rijke}, Maarten and Venema, Yde}, + year = {2001}, + pages = {196--201}, + abstract = {This is an advanced 2001 textbook on modal logic, a field which caught the attention of computer scientists in the late 1970s. Researchers in areas ranging from economics to computational linguistics have since realised its worth. The book is for novices and for more experienced readers, with two distinct tracks clearly signposted at the start of each chapter. The development is mathematical; prior acquaintance with first-order logic and its semantics is assumed, and familiarity with the basic mathematical notions of set theory is required. The authors focus on the use of modal languages as tools to analyze the properties of relational structures, including their algorithmic and algebraic aspects, and applications to issues in logic and computer science such as completeness, computability and complexity are considered. Three appendices supply basic background information and numerous exercises are provided. Ideal for anyone wanting to learn modern modal logic.}, + isbn = {978-1-107-05088-4 978-1-316-09752-6 978-1-316-09907-0}, + langid = {english} +} + +@article{bobenriethOriginsUseArgument2010, + ids = {bobenriethm.OriginsUseArgument2010}, + title = {The {{Origins}} of the {{Use}} of the {{Argument}} of {{Trivialization}} in the {{Twentieth Century}}}, + author = {Bobenrieth, Andrés}, + year = {2010}, + month = may, + journal = {History and Philosophy of Logic}, + volume = {31}, + number = {2}, + pages = {111--121}, + issn = {0144-5340, 1464-5149}, + doi = {10.1080/01445340903340033}, + langid = {english}, + file = {/home/mpwd/Zotero/storage/IICQTFGA/01445340903340033.html} +} + +@incollection{booleChapterXVIIGeneral1853, + title = {Chapter {{XVII}}. {{General Method In Probabilities}}}, + booktitle = {An {{Investigation}} of the {{Laws}} of {{Thought On}} Which Are Founded the Mathematical Theories of Logic and Probabilities}, + author = {Boole, George}, + year = {1853}, + pages = {253--275}, + langid = {english}, + keywords = {Logic,Logic; Symbolic and mathematical,Probabilities,Symbolic and mathematical,Thought and thinking} +} + +@incollection{booleChapterXVITheory1853, + title = {Chapter {{XVI}}. {{On The Theory Of Probabilities}}}, + booktitle = {An {{Investigation}} of the {{Laws}} of {{Thought On}} Which Are Founded the Mathematical Theories of Logic and Probabilities}, + author = {Boole, George}, + year = {1853}, + pages = {243--252}, + langid = {english}, + keywords = {Logic,Logic; Symbolic and mathematical,Probabilities,Symbolic and mathematical,Thought and thinking} +} + +@book{booleInvestigationLawsThought1853, + title = {An {{Investigation}} of the {{Laws}} of {{Thought On}} Which Are Founded the Mathematical Theories of Logic and Probabilities}, + author = {Boole, George}, + year = {1853}, + copyright = {Public domain in the USA.}, + langid = {english}, + lccn = {EBook-No. 15114}, + keywords = {Logic,Logic; Symbolic and mathematical,Probabilities,Symbolic and mathematical,Thought and thinking} +} + +@article{boolosDonEliminateCut1984, + ids = {boolosDonEliminateCut1984a}, + title = {Don't {{Eliminate Cut}}}, + author = {Boolos, George}, + year = {1984}, + journal = {Journal of Philosophical Logic}, + volume = {13}, + number = {4}, + pages = {373--378}, + publisher = {{Springer}}, + issn = {0022-3611}, + doi = {10.1007/BF00247711}, + langid = {english} +} + +@article{broderickBooleanAlgebraProbability1940, + title = {Boolean {{Algebra}} and {{Probability Theory}}}, + author = {Broderick, T. S. and Schrödinger, E.}, + year = {1940}, + journal = {Proceedings of the Royal Irish Academy. Section A: Mathematical and Physical Sciences}, + volume = {46}, + pages = {103--112}, + publisher = {{Royal Irish Academy}}, + issn = {0035-8975} +} + +@incollection{daveyChapterRepresentationFinite2002, + title = {Chapter 5. {{Representation}}: The Finite Case}, + booktitle = {Introduction to Lattices and Order}, + author = {Davey, B. A. and Priestley, H. A.}, + year = {2002}, + edition = {2nd ed}, + pages = {112--124}, + publisher = {{Cambridge University Press}}, + address = {{Cambridge, UK ; New York, NY}}, + isbn = {978-0-521-78451-1}, + lccn = {QA171.5 .D38 2002}, + keywords = {Lattice theory} +} + +@book{daveyIntroductionLatticesOrder2002, + ids = {daveyIntroductionLatticesOrder2002a}, + title = {Introduction to Lattices and Order}, + author = {Davey, B. A. and Priestley, H. A.}, + year = {2002}, + edition = {2nd ed}, + publisher = {{Cambridge University Press}}, + address = {{Cambridge, UK ; New York, NY}}, + isbn = {978-0-521-78451-1}, + lccn = {QA171.5 .D38 2002}, + keywords = {Lattice theory}, + file = {/Users/mpwd/Documents/Library/Davey and Priestley - 2002 - Introduction to lattices and order.pdf} +} + +@article{definettiLogicProbability1995, + ids = {DeFinettiLogicProbability1995}, + title = {The {{Logic}} of {{Probability}}}, + author = {De Finetti, Bruno and Angell, Brad}, + year = {1995}, + journal = {Philosophical Studies: An International Journal for Philosophy in the Analytic Tradition}, + volume = {77}, + number = {1}, + pages = {181--190}, + issn = {0031-8116} +} + +@article{definettiSuiPassaggiLimite1930, + title = {Sui Passaggi al Limite Nel Calcolo Delle Probabilità}, + author = {De Finetti, B.}, + year = {1930}, + journal = {Reale Istituto Lombardo di Scienze e Lettere}, + volume = {63}, + pages = {1--12} +} + +@article{dempsterUpperLowerProbabilities1967, + title = {Upper and {{Lower Probabilities Induced}} by a {{Multivalued Mapping}}}, + author = {Dempster, A. P.}, + year = {1967}, + journal = {The Annals of Mathematical Statistics}, + volume = {38}, + number = {2}, + pages = {325--339}, + publisher = {{Institute of Mathematical Statistics}}, + issn = {0003-4851}, + abstract = {A multivalued mapping from a space X to a space S carries a probability measure defined over subsets of X into a system of upper and lower probabilities over subsets of S. Some basic properties of such systems are explored in Sections 1 and 2. Other approaches to upper and lower probabilities are possible and some of these are related to the present approach in Section 3. A distinctive feature of the present approach is a rule for conditioning, or more generally, a rule for combining sources of information, as discussed in Sections 4 and 5. Finally, the context in statistical inference from which the present theory arose is sketched briefly in Section 6.} +} + +@article{eberlBuffonNeedleProblem2017, + ids = {Buffons\_Needle-AFP}, + title = {Buffon's Needle Problem}, + author = {Eberl, Manuel}, + year = {2017}, + month = jun, + journal = {Archive of Formal Proofs}, + issn = {2150-914x}, + abstract = {In the 18th century, Georges-Louis Leclerc, Comte de Buffon posed and later solved the following problem, which is often called the first problem ever solved in geometric probability: Given a floor divided into vertical strips of the same width, what is the probability that a needle thrown onto the floor randomly will cross two strips? This entry formally defines the problem in the case where the needle's position is chosen uniformly at random in a single strip around the origin (which is equivalent to larger arrangements due to symmetry). It then provides proofs of the simple solution in the case where the needle's length is no greater than the width of the strips and the more complicated solution in the opposite case.} +} + +@incollection{ellenbergChapter11What2014, + title = {Chapter 11. {{What}} to {{Expect When You}}'re {{Expecting}} to {{Win}} the {{Lottery}}}, + booktitle = {How {{Not To Be Wrong}}: {{The Power}} of {{Mathematical Thinking}}}, + author = {Ellenberg, Jordan}, + year = {2014}, + publisher = {{The Penguin Press}}, + address = {{New York}}, + abstract = {"In How Not to Be Wrong, Jordan Ellenberg shows us that math isn't confined to abstract incidents that never occur in real life, but rather touches everything we do--the whole world is shot through with it. Math allows us to see the hidden structures underneath the messy and chaotic surface of our world. It's a science of not being wrong, hammered out by centuries of hard work and argument. Armed with the tools of mathematics, we can see through to the true meaning of information we take for granted: How early should you get to the airport? What does "public opinion" really represent? Why do tall parents have shorter children? Who really won Florida in 2000? And how likely are you, really, to develop cancer? How Not to Be Wrong presents the surprising revelations behind all of these questions and many more, using the mathematician's method of analyzing life and exposing the hard-won insights of the academic community to the layman--minus the jargon. Ellenberg pulls from history as well as from the latest theoretical developments to provide those not trained in math with the knowledge they need. "--}, + isbn = {978-1-59420-522-4}, + lccn = {QA99 .E45 2014}, + keywords = {Mathematical analysis,Mathematics,MATHEMATICS / General,Miscellanea} +} + +@book{ellenbergHowNotBe2014, + title = {How Not to Be Wrong: The Power of Mathematical Thinking}, + shorttitle = {How Not to Be Wrong}, + author = {Ellenberg, Jordan}, + year = {2014}, + publisher = {{The Penguin Press}}, + address = {{New York}}, + abstract = {"In How Not to Be Wrong, Jordan Ellenberg shows us that math isn't confined to abstract incidents that never occur in real life, but rather touches everything we do--the whole world is shot through with it. Math allows us to see the hidden structures underneath the messy and chaotic surface of our world. It's a science of not being wrong, hammered out by centuries of hard work and argument. Armed with the tools of mathematics, we can see through to the true meaning of information we take for granted: How early should you get to the airport? What does "public opinion" really represent? Why do tall parents have shorter children? Who really won Florida in 2000? And how likely are you, really, to develop cancer? How Not to Be Wrong presents the surprising revelations behind all of these questions and many more, using the mathematician's method of analyzing life and exposing the hard-won insights of the academic community to the layman--minus the jargon. Ellenberg pulls from history as well as from the latest theoretical developments to provide those not trained in math with the knowledge they need. "--}, + isbn = {978-1-59420-522-4}, + lccn = {QA99 .E45 2014}, + keywords = {Mathematical analysis,Mathematics,MATHEMATICS / General,Miscellanea} +} + +@article{gainesFuzzyProbabilityUncertainty1978, + ids = {gainesFuzzyProbabilityUncertainty}, + title = {Fuzzy and Probability Uncertainty Logics}, + author = {Gaines, Brian R.}, + year = {1978}, + month = aug, + journal = {Information and Control}, + volume = {38}, + number = {2}, + pages = {154--169}, + issn = {0019-9958}, + doi = {10.1016/S0019-9958(78)90165-1}, + abstract = {Probability theory and fuzzy logic have been presented as quite distinct theoretical foundations for reasoning and decision making in situations of uncertainty. This paper establishes a common basis for both forms of logic of uncertainty in which a basic uncertainty logic is defined in terms of a valuation on a lattice of propositions. The (non-truth-functional) connectives for conjunction, disjunction, equivalence, implication, and negation are defined in terms which closely resemble those of probability theory. Addition of the axiom of the excluded middle to the basic logic gives a standard probability logic. Alternatively, addition of a requirement for strong truth-functionality (truth-value of connective determined by truth-value of constituents) gives a fuzzy logic with connectives, including implication, as in Lukasiewicz' infinitely valued logic. A common semantics for all such variants is given in terms of binary responses from a population. The type of population, e.g., physical events, people, or neurons, determines whether the model is of physical probability, subjective belief, or human decision-making. The formal theory and the semantics together illustrate clearly the precise similarities and differences between fuzzy and probability logics.}, + langid = {english}, + file = {/home/mpwd/Zotero/storage/M6W5EHV6/Gaines - Fuzzy and Probability Uncertainty Logics.pdf} +} + +@article{gareySimplifiedNPcompleteGraph1976, + title = {Some Simplified {{NP-complete}} Graph Problems}, + author = {Garey, M. R. and Johnson, D. S. and Stockmeyer, L.}, + year = {1976}, + month = feb, + journal = {Theoretical Computer Science}, + volume = {1}, + number = {3}, + pages = {237--267}, + issn = {0304-3975}, + doi = {10.1016/0304-3975(76)90059-1}, + abstract = {It is widely believed that showing a problem to be NP-complete is tantamount to proving its computational intractability. In this paper we show that a number of NP-complete problems remain NP-complete even when their domains are substantially restricted. First we show the completeness of Simple Max Cut (Max Cut with edge weights restricted to value 1), and, as a corollary, the completeness of the Optimal Linear Arrangement problem. We then show that even if the domains of the Node Cover and Directed Hamiltonian Path problems are restricted to planar graphs, the two problems remain NP-complete, and that these and other graph problems remain NP-complete even when their domains are restricted to graphs with low node degrees. For Graph 3-Colorability, Node Cover, and Undirected Hamiltonian Circuit, we determine essentially the lowest possible upper bounds on node degree for which the problems remain NP-complete.}, + langid = {english}, + file = {/home/mpwd/Zotero/storage/N5XBW7LE/Garey et al. - 1976 - Some simplified NP-complete graph problems.pdf;/home/mpwd/Zotero/storage/VTDZI6W9/0304397576900591.html} +} + +@article{gentzenUntersuchungenUeberLogische1935, + title = {{Untersuchungen über das logische Schließen. I}}, + author = {Gentzen, Gerhard}, + year = {1935}, + month = dec, + journal = {Mathematische Zeitschrift}, + volume = {39}, + number = {1}, + pages = {176--210}, + issn = {1432-1823}, + doi = {10.1007/BF01201353}, + langid = {ngerman} +} + +@article{gerlaInferencesProbabilityLogic1994, + ids = {gerlaInferencesProbabilityLogic1994a}, + title = {Inferences in Probability Logic}, + author = {Gerla, Giangiacomo}, + year = {1994}, + month = oct, + journal = {Artificial Intelligence}, + volume = {70}, + number = {1-2}, + pages = {33--52}, + issn = {00043702}, + doi = {10.1016/0004-3702(94)90102-3}, + langid = {english}, + file = {/home/mpwd/Zotero/storage/YCGIA5L4/Gerla - 1994 - Inferences in probability logic.pdf} +} + +@book{hailperinBooleLogicProbability1986, + title = {Boole's {{Logic}} and {{Probability}}: {{A Critical Exposition}} from the {{Standpoint}} of {{Contemporary Algebra}}, {{Logic}} and {{Probability Theory}}}, + shorttitle = {Boole's Logic and Probability}, + author = {Hailperin, Theodore}, + year = {1986}, + series = {Studies in Logic and the Foundations of Mathematics}, + edition = {2. ed, rev. and enl}, + number = {85}, + publisher = {{North-Holland}}, + address = {{Amsterdam}}, + isbn = {978-0-444-87952-3}, + annotation = {OCLC: 241617838}, + file = {/home/mpwd/Zotero/storage/ERMQ8GFR/Hailperin - 1986 - Boole's logic and probability a crit. exposition .pdf} +} + +@article{hailperinProbabilityLogic1984, + title = {Probability {{Logic}}}, + author = {Hailperin, Theodore}, + year = {1984}, + month = jul, + journal = {Notre Dame Journal of Formal Logic}, + volume = {25}, + number = {3}, + pages = {198--212}, + issn = {0029-4527}, + doi = {10.1305/ndjfl/1093870625}, + langid = {english}, + file = {/home/mpwd/Zotero/storage/3QKV65MU/Hailperin - 1984 - Probability logic..pdf} +} + +@book{hailperinSententialProbabilityLogic1996, + title = {Sentential {{Probability Logic}}: {{Origins}}, {{Development}}, {{Current Status}}, and {{Technical Applications}}}, + shorttitle = {Sentential {{Probability Logic}}}, + author = {Hailperin, Theodore}, + year = {1996}, + publisher = {{Lehigh University Press}}, + address = {{Bethlehem : London ; Cranbury, N.J}}, + abstract = {This study presents a logic in which probability values play a semantic role comparable to that of truth values in conventional logic. The difference comes in with the semantic definition of logical consequence. It will be of interest to logicians, both philosophical and mathematical, and to investigators making use of logical inference under uncertainty, such as in operations research, risk analysis, artificial intelligence, and expert systems.}, + googlebooks = {Iu8pSmBMg\_oC}, + isbn = {978-0-934223-45-4}, + langid = {english}, + keywords = {Algebra,Algebraic logic,Boolean,Mathematics / Logic,Probabilities} +} + +@article{harrisonMartingalesArbitrageMultiperiod1979, + title = {Martingales and Arbitrage in Multiperiod Securities Markets}, + author = {Harrison, J.Michael and Kreps, David M}, + year = {1979}, + month = jun, + journal = {Journal of Economic Theory}, + volume = {20}, + number = {3}, + pages = {381--408}, + issn = {00220531}, + doi = {10.1016/0022-0531(79)90043-7}, + langid = {english} +} + +@article{hornMeasuresBooleanAlgebras1948, + ids = {hornMEASURESBOOLEANALGEBRAS,hornMeasuresBooleanAlgebras1948a}, + title = {Measures in {{Boolean}} Algebras}, + author = {Horn, Alfred and Tarski, Alfred}, + year = {1948}, + month = mar, + journal = {Transactions of the American Mathematical Society}, + volume = {64}, + number = {3}, + pages = {467--467}, + issn = {0002-9947}, + doi = {10.1090/S0002-9947-1948-0028922-8}, + langid = {english}, + file = {/home/mpwd/Zotero/storage/HZVS3YWL/Horn and Tarski - MEASURES IN BOOLEAN ALGEBRAS.pdf} +} + +@article{johanssonMinimalkalkuelReduzierterIntuitionistischer1936, + ids = {JohanssonMinimal1936}, + title = {{Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus}}, + author = {Johansson, Ingebrigt}, + year = {1936}, + journal = {Compositio Mathematica}, + volume = {4}, + pages = {119--136}, + issn = {0010-437X; 1570-5846/e}, + langid = {german}, + keywords = {Foundations,logic,philosophy} +} + +@incollection{kolmogoroffChapterElementareWahrscheinlichkeitsrechnung1933, + title = {{Chapter 1. Die elementare Wahrscheinlichkeitsrechnung}}, + booktitle = {{Grundbegriffe der Wahrscheinlichkeitsrechnung}}, + author = {Kolmogoroff, A}, + year = {1933}, + series = {{Ergebnisse der Mathematik und Ihrer Grenzgebiete}}, + edition = {First}, + number = {2}, + pages = {1--12}, + publisher = {{Springer-Verlag Berlin Heidelberg}}, + isbn = {978-3-642-49888-6 978-3-642-49596-0}, + langid = {german}, + annotation = {OCLC: 913643439} +} + +@article{lehmanConfirmationRationalBetting1955, + title = {On {{Confirmation}} and {{Rational Betting}}}, + author = {Lehman, R. Sherman}, + year = {1955}, + journal = {The Journal of Symbolic Logic}, + volume = {20}, + number = {3}, + pages = {251--262}, + publisher = {{[Association for Symbolic Logic, Cambridge University Press]}}, + issn = {0022-4812}, + doi = {10.2307/2268221} +} + +@article{nilssonProbabilisticLogic1986, + title = {Probabilistic {{Logic}}}, + author = {Nilsson, Nils J.}, + year = {1986}, + month = feb, + journal = {Artificial Intelligence}, + volume = {28}, + number = {1}, + pages = {71--87}, + issn = {00043702}, + doi = {10.1016/0004-3702(86)90031-7}, + langid = {english} +} + +@incollection{pascucciDiscreteMarketModels2011, + title = {Discrete Market Models}, + booktitle = {{{PDE}} and {{Martingale Methods}} in {{Option Pricing}}}, + author = {Pascucci, Andrea}, + editor = {Pascucci, Andrea}, + year = {2011}, + series = {Bocconi \& {{Springer Series}}}, + pages = {15--96}, + publisher = {{Springer Milan}}, + address = {{Milano}}, + doi = {10.1007/978-88-470-1781-8_2}, + abstract = {In this chapter we describe market models in discrete time to price and hedge European and American-style derivatives. We present the classical model introduced by Cox, Ross and Rubinstein in [78] and we mention briefly the pricing problem in incomplete markets. General references on topics covered in this chapter are Dana and Jeanblanc [84], Föllmer and Schied [134], Lamberton and Lapeyre [226], Pliska [282], Shreve [310], van der Hoek and Elliott [329]: we also mention Pascucci and Runggaldier [277] where several examples and exercises can be found.}, + isbn = {978-88-470-1781-8}, + langid = {english}, + keywords = {American Option,Call Option,Hedging Strategy,Risky Asset,Underlying Asset} +} + +@article{peirceAlgebraLogicContribution1885, + title = {On the {{Algebra}} of {{Logic}}: {{A Contribution}} to the {{Philosophy}} of {{Notation}}}, + shorttitle = {On the {{Algebra}} of {{Logic}}}, + author = {Peirce, C. S.}, + year = {1885}, + month = jan, + journal = {American Journal of Mathematics}, + volume = {7}, + number = {2}, + pages = {180--196}, + publisher = {{Johns Hopkins University Press}}, + issn = {0002-9327}, + doi = {10.2307/2369451} +} + +@book{poundstoneFortuneFormulaUntold2006, + title = {Fortune's Formula: The Untold Story of the Scientific Betting System That Beat the Casinos and {{Wall Street}}}, + shorttitle = {Fortune's Formula}, + editor = {Poundstone, William}, + year = {2006}, + edition = {1. paperback ed}, + publisher = {{Hill and Wang}}, + address = {{New York}}, + isbn = {978-0-8090-4599-0}, + langid = {english} +} + +@book{poundstoneFortuneFormulaUntold2006a, + title = {Fortune's Formula: The Untold Story of the Scientific Betting System That Beat the Casinos and {{Wall Street}}}, + shorttitle = {Fortune's Formula}, + editor = {Poundstone, William}, + year = {2006}, + edition = {1. paperback ed}, + publisher = {{Hill and Wang}}, + address = {{New York}}, + isbn = {978-0-8090-4599-0}, + langid = {english} +} + +@misc{PredictIt, + title = {{{PredictIt}}}, + howpublished = {https://www.predictit.org/}, + file = {/home/mpwd/Zotero/storage/ULUCIITW/www.predictit.org.html} +} + +@incollection{ramseyChapterTruthProbability1931, + title = {Chapter 3. {{Truth}} and {{Probability}}}, + booktitle = {The Foundations of Mathematics and Other Logical Essays}, + author = {Ramsey, Frank Plumpton}, + editor = {Braithwaite, Joseph Bevan}, + year = {1931}, + series = {The International Library of Philosophy \$ {{Philosophy}} of Logic and Mathematics 32, {{Philosophy}} of Logic and Mathematics : In 8 Volumes}, + number = {5}, + publisher = {{Routledge}}, + address = {{London}}, + isbn = {978-0-415-22546-5}, + langid = {english} +} + +@book{rescherManyvaluedLogic1969, + title = {Many-Valued Logic.}, + author = {Rescher, Nicholas}, + year = {1969}, + month = jan, + edition = {First}, + publisher = {{McGraw-Hill}}, + address = {{New York}}, + isbn = {978-0-07-051893-3}, + langid = {english}, + annotation = {OCLC: 11761} +} + +@article{savageDifficultiesTheoryPersonal1967, + title = {Difficulties in the {{Theory}} of {{Personal Probability}}}, + author = {Savage, Leonard J.}, + year = {1967}, + journal = {Philosophy of Science}, + volume = {34}, + number = {4}, + pages = {305--310}, + publisher = {{[The University of Chicago Press, Philosophy of Science Association]}}, + issn = {0031-8248} +} + +@incollection{suppesProbabilisticInferenceConcept1966, + ids = {suppesProbabilisticInferenceConcept1966a}, + title = {Probabilistic {{Inference}} and the {{Concept}} of {{Total Evidence}}}, + booktitle = {Studies in {{Logic}} and the {{Foundations}} of {{Mathematics}}}, + author = {Suppes, Patrick}, + editor = {Hintikka, Jaakko and Suppes, Patrick}, + year = {1966}, + month = jan, + series = {Aspects of {{Inductive Logic}}}, + volume = {43}, + pages = {49--65}, + publisher = {{Elsevier}}, + doi = {10.1016/S0049-237X(08)71662-8}, + abstract = {This chapter examines a cluster of issues centering on the statistical syllogism and the concept of total evidence. A kind of paradox is alleged to arise from the uninhibited use of a statistical syllogism. It is possible to assign probabilities to at least three kinds of entities: sentences, propositions, and events. To avoid going back and forth between the sentence-approach of confirmation theory and the event-approach of standard probability theory, the chapter uses the event-language but standard sentential connectives to form terms denoting complex events. The chapter discusses the rule of detachment and explains that its application in an argument requires no query as to whether the total evidence has been considered; it has exactly the same status as the rule of detachment in deductive logic.}, + isbn = {978-0-444-53408-8}, + langid = {english} +} + +@book{troelstraBasicProofTheory2000, + title = {Basic Proof Theory}, + author = {Troelstra, A. S. and Schwichtenberg, Helmut}, + year = {2000}, + series = {Cambridge Tracts in Theoretical Computer Science}, + edition = {2nd ed}, + number = {43}, + publisher = {{Cambridge University Press}}, + isbn = {978-0-521-77911-1}, + lccn = {QA9.54 .T76 2000}, + keywords = {Proof theory} +} + +@article{turnerAnotherAlgorithmBracket1979, + title = {Another {{Algorithm}} for {{Bracket Abstraction}}}, + author = {Turner, D. A.}, + year = {1979}, + month = jun, + journal = {Journal of Symbolic Logic}, + volume = {44}, + number = {2}, + pages = {267--270}, + issn = {0022-4812, 1943-5886}, + doi = {10.2307/2273733}, + abstract = {This short article presents an algorithm for bracket abstraction [1] which avoids a combinatorial explosion in the size of the resulting expression when applied repeatedly for abstraction in a series of variables. It differs from a previous solution [2] in introducing only a finite number of additional combinators and in not requiring that all the variables to be abstracted be treated together in a single operation.}, + langid = {english} +} + +@article{urquhartImplicationalFormulasIntuitionistic1974, + title = {Implicational {{Formulas}} in {{Intuitionistic Logic}}}, + author = {Urquhart, Alasdair}, + year = {1974}, + journal = {The Journal of Symbolic Logic}, + volume = {39}, + number = {4}, + pages = {661--664}, + publisher = {{[Association for Symbolic Logic, Cambridge University Press]}}, + issn = {0022-4812}, + doi = {10.2307/2272850}, + langid = {english} +} + +@book{vandalenLogicStructure2013, + ids = {dalenLogicStructure2013,vandalenLogicStructure2013a}, + title = {Logic and {{Structure}}}, + author = {{van Dalen}, Dirk}, + year = {2013}, + series = {Universitext}, + edition = {Fifth}, + publisher = {{Springer-Verlag}}, + address = {{London}}, + doi = {10.1007/978-1-4471-4558-5}, + abstract = {Dirk van Dalen's popular textbook Logic and Structure, now in its fifth edition, provides a comprehensive introduction to the basics of classical and intuitionistic logic, model theory and Gödel's famous incompleteness theorem. Propositional and predicate logic are presented in an easy-to-read style using Gentzen's natural deduction. The book proceeds with some basic concepts and facts of model theory: a discussion on compactness, Skolem-Löwenheim, non-standard models and quantifier elimination. The discussion of classical logic is concluded with a concise exposition of second-order logic. In view of the growing recognition of constructive methods and principles, intuitionistic logic and Kripke semantics is carefully explored. A number of specific constructive features, such as apartness and equality, the Gödel translation, the disjunction and existence property are also included. The last chapter on Gödel's first incompleteness theorem is self-contained and provides a systematic exposition of the necessary recursion theory. This new edition has been properly revised and contains a new section on ultra-products.}, + isbn = {978-1-4471-4557-8}, + langid = {english}, + lccn = {QA9 .D16 2013}, + keywords = {Logic,Symbolic and mathematical}, + file = {/home/mpwd/Zotero/storage/587FH3RA/9781447145578.html} +} + +@misc{wangProjectionProbabilitySimplex2013, + title = {Projection onto the Probability Simplex: {{An}} Efficient Algorithm with a Simple Proof, and an Application}, + shorttitle = {Projection onto the Probability Simplex}, + author = {Wang, Weiran and {Carreira-Perpiñán}, Miguel Á}, + year = {2013}, + month = sep, + number = {arXiv:1309.1541}, + eprint = {1309.1541}, + eprinttype = {arxiv}, + primaryclass = {cs, math, stat}, + publisher = {{arXiv}}, + doi = {10.48550/arXiv.1309.1541}, + abstract = {We provide an elementary proof of a simple, efficient algorithm for computing the Euclidean projection of a point onto the probability simplex. We also show an application in Laplacian K-modes clustering.}, + archiveprefix = {arXiv}, + keywords = {Computer Science - Machine Learning,Mathematics - Optimization and Control,Statistics - Machine Learning}, + file = {/home/mpwd/Zotero/storage/AIEY7GNP/Wang and Carreira-Perpiñán - 2013 - Projection onto the probability simplex An effici.pdf;/home/mpwd/Zotero/storage/2K9UZM4V/1309.html} +} + +@inbook{wasilewskaChapterHilbertProof2018, + title = {Chapter 5. {{Hilbert Proof Systems Completeness}} of {{Classical Propositional Logic}}}, + booktitle = {Logics for {{Computer Science}}}, + author = {Wasilewska, Anita}, + year = {2018}, + pages = {179--232}, + publisher = {{Springer International Publishing}}, + address = {{Cham}}, + doi = {10.1007/978-3-319-92591-2_5}, + collaborator = {Wasilewska, Anita}, + isbn = {978-3-319-92590-5 978-3-319-92591-2}, + langid = {english} +} + +@article{weathersonClassicalIntuitionisticProbability2003, + title = {From {{Classical}} to {{Intuitionistic Probability}}}, + author = {Weatherson, Brian}, + year = {2003}, + month = apr, + journal = {Notre Dame Journal of Formal Logic}, + volume = {44}, + number = {2}, + pages = {111--123}, + issn = {0029-4527}, + doi = {10.1305/ndjfl/1082637807}, + abstract = {We generalize the Kolmogorov axioms for probability calculus to obtain conditions defining, for any given logic, a class of probability functions relative to that logic, coinciding with the standard probability functions in the special case of classical logic but allowing consideration of other classes of "essentially Kolmogorovian" probability functions relative to other logics. We take a broad view of the Bayesian approach as dictating inter alia that from the perspective of a given logic, rational degrees of belief are those representable by probability functions from the class appropriate to that logic. Classical Bayesianism, which fixes the logic as classical logic, is only one version of this general approach. Another, which we call Intuitionistic Bayesianism, selects intuitionistic logic as the preferred logic and the associated class of probability functions as the right class of candidate representions of epistemic states (rational allocations of degrees of belief). Various objections to classical Bayesianism are, we argue, best met by passing to intuitionistic Bayesianism—in which the probability functions are taken relative to intuitionistic logic—rather than by adopting a radically non-Kolmogorovian, for example, nonadditive, conception of (or substitute for) probability functions, in spite of the popularity of the latter response among those who have raised these objections. The interest of intuitionistic Bayesianism is further enhanced by the availability of a Dutch Book argument justifying the selection of intuitionistic probability functions as guides to rational betting behavior when due consideration is paid to the fact that bets are settled only when/if the outcome bet on becomes known.}, + langid = {english}, + file = {/home/mpwd/Zotero/storage/KGRF39PS/Disseminate.pdf;/home/mpwd/Zotero/storage/YA26X8Y3/Weatherson - 2003 - From Classical to Intuitionistic Probability.pdf} +} + +@incollection{williamsonProbabilityLogic2002, + title = {Probability Logic}, + booktitle = {Studies in {{Logic}} and {{Practical Reasoning}}}, + author = {Williamson, Jon}, + editor = {Gabbay, Dov M. and Johnson, Ralph H. and Ohlbach, Hans Jürgen and Woods, John}, + year = {2002}, + month = jan, + series = {Handbook of the {{Logic}} of {{Argument}} and {{Inference}}}, + volume = {1}, + pages = {397--424}, + publisher = {{Elsevier}}, + doi = {10.1016/S1570-2464(02)80011-8}, + abstract = {This chapter discusses probability logic. It highlights probability as a representation of uncertainty, and see how a logic of practical reasoning might involve probability, in order to help agents. The chapter recalls the standard definition of probability, and the standard interpretations of this formal definition. It also recalls the standard definition of probability, and the standard interpretations of this formal definition. The chapter also discusses attempts to incorporate probability into a logic, and go on to investigate a practical question, namely inference. Probability has a rather technical mathematical characterization. Probability has a number of standard interpretations and it presents a brief review of this. The starting point for most theories that integrate probability and logic is to attach probability to logical statements rather than events. The motivation is that logic operates on statements and so it would be natural if a probabilistic logic for practical reasoning has to do the same. A second motivation is that when looking at the application of the mathematical theory of probability, it shows that probabilities are usually posited of a random variable taking a certain value.}, + langid = {english}, + file = {/home/mpwd/Zotero/storage/G246X5AX/S1570246402800118.html} +} + diff --git a/thys/Suppes_Theorem/document/root.tex b/thys/Suppes_Theorem/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Suppes_Theorem/document/root.tex @@ -0,0 +1,64 @@ +\documentclass[11pt,a4paper]{report} +\usepackage{isabelle, isabellesym} +\usepackage{amsfonts, amsmath, amssymb} +\usepackage{mathpartir} +\usepackage{eurosym} + +\usepackage[only,bigsqcap]{stmaryrd} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{Suppes' Theorem For Probability Logic} +\author{Matthew Doty} + +\maketitle + +\begin{abstract} + We develop finitely additive probability logic and prove a theorem + of Patrick Suppes that asserts that $\Psi \vdash \phi$ in classical + propositional logic if and only if + $(\sum \psi \leftarrow \Psi.\; 1 - \mathcal{P} \psi) \geq 1 - + \mathcal{P} \phi$ holds for all probabilities $\mathcal{P}$. We also + provide a novel \emph{dual} form of Suppes' Theorem, which holds + that + $(\sum \phi \leftarrow \Phi.\; \mathcal{P} \phi) \leq \mathcal{P} + \psi$ for all probabilities $\mathcal{P}$ if and only + $\left(\bigvee \Phi\right) \vdash \psi$ and all of the formulae in + $\Phi$ are logically exclusive from one another. Our proofs use + \emph{Maximally Consistent Sets}, and as a consequence, we obtain + two \emph{collapse} theorems. In particular, we show + $(\sum \phi \leftarrow \Phi.\; \mathcal{P} \phi) \geq \mathcal{P} + \psi$ holds for all probabilities $\mathcal{P}$ if and only if + $(\sum \phi \leftarrow \Phi.\; \delta\; \phi) \geq \delta\; \psi$ + holds for all binary-valued probabilities $\delta$, along with the + dual assertion that + $(\sum \phi \leftarrow \Phi. \;\mathcal{P} \phi) \leq \mathcal{P} + \psi$ holds for all probabilities $\mathcal{P}$ if and only if + $(\sum \phi \leftarrow \Phi.\; \delta\; \phi) \leq \delta\; \psi$ + holds for all binary-valued probabilities $\delta$. +\end{abstract} + +\tableofcontents + +\newpage + +\parindent 0pt\parskip 0.5ex + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: