Communities

Writing
Writing
Codidact Meta
Codidact Meta
The Great Outdoors
The Great Outdoors
Photography & Video
Photography & Video
Scientific Speculation
Scientific Speculation
Cooking
Cooking
Electrical Engineering
Electrical Engineering
Judaism
Judaism
Languages & Linguistics
Languages & Linguistics
Software Development
Software Development
Mathematics
Mathematics
Christianity
Christianity
Code Golf
Code Golf
Music
Music
Physics
Physics
Linux Systems
Linux Systems
Power Users
Power Users
Tabletop RPGs
Tabletop RPGs
Community Proposals
Community Proposals
tag:snake search within a tag
answers:0 unanswered questions
user:xxxx search by author id
score:0.5 posts with 0.5+ score
"snake oil" exact phrase
votes:4 posts with 4+ votes
created:<1w created < 1 week ago
post_type:xxxx type of post
Search help
Notifications
Mark all as read See all your notifications »
Users Search
Help Dashboard Sign In Sign Up
Q&A Meta
Q&A
Posts Tags Edits
Ask Question

Post History

66%
+2 −0
Q&A Defining Bayes’s theorem from scratch in ZFC

posted 8mo ago by xamidi‭  ·  edited 8mo ago by xamidi‭

Answer
#5: Post edited by user avatar xamidi‭ · 2024-04-07T12:41:16Z (8 months ago)
  • All of this has already been dealt with on Metamath, see [mpeuni/bayesth](https://us.metamath.org/mpeuni/bayesth.html) or [asrt/bayesth](https://expln.github.io/metamath/asrt/bayesth.html).
  • At first, they had to decide on concrete formulations of ZFC axioms, which must be stated in a formal language. All referenced axioms (including definitions of, for example, [the class of probability measures](https://us.metamath.org/mpeuni/df-prob.html) and [conditional probability](https://us.metamath.org/mpeuni/df-cndprob.html)) are linked at the bottom of the site of the first link, and you can explore the whole proof by following the references to subproofs.
  • Note that these proofs are fully formalized and thus can be verified by a machine. This is always the case when deriving everything from axioms, rather than making intuitive statements in natural language, which are rather _social proofs_ in contrast to _formal proofs_, as [noted here](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/handbookI/ChapterI.pdf).
  • It appears to me that you underestimate the complexity of creating formal proofs from nothing, which is indicated by the mere amount of definitions that this theorem relies upon. Even though the theorem contains only one name of the person who completed it, it resulted from a big collaborative effort due being built upon this large framework.
  • Formal proofs work purely on syntax (i.e. structure) and not at all on semantics (i.e. meaning). Outsourcing the thinking process (which is susceptible to errors) to formal methods is precisely what axioms and proofs are meant for. Social proofs (which are most common in mathematics) just do not go all the way.
  • Which is mainly, because that would be too hard for most mathematicians to both create and conceive. After all, mathematics _de facto_ is a social framework for humans to intuitively understand abstract objects.
  • All of this has already been dealt with on Metamath, see [mpeuni/bayesth](https://us.metamath.org/mpeuni/bayesth.html) or [asrt/bayesth](https://expln.github.io/metamath/asrt/bayesth.html).
  • At first, they had to decide on concrete formulations of ZFC axioms, which must be stated in a formal language. All referenced axioms (including definitions of, for example, [the class of probability measures](https://us.metamath.org/mpeuni/df-prob.html) and [conditional probability](https://us.metamath.org/mpeuni/df-cndprob.html)) are linked at the bottom of the site of the first link, and you can explore the whole proof by following the references to subproofs.
  • Note that these proofs are fully formalized and thus can be verified by a machine. This is always the case when deriving everything from axioms, rather than making intuitive statements in natural language, which are rather _social proofs_ in contrast to _formal proofs_, as [noted here](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/handbookI/ChapterI.pdf).
  • It appears to me that you underestimate the complexity of creating formal proofs from scratch, which is indicated by the mere amount of definitions that this theorem relies upon. Even though the theorem contains only one name of the person who completed it, it resulted from a big collaborative effort due being built upon this large framework.
  • Formal proofs work purely on syntax (i.e. structure) and not at all on semantics (i.e. meaning). Outsourcing the thinking process (which is susceptible to errors) to formal methods is precisely what axioms and proofs are meant for. Social proofs (which are most common in mathematics) just do not go all the way.
  • Which is mainly, because that would be too hard for most mathematicians to both create and conceive. After all, mathematics _de facto_ is a social framework for humans to intuitively understand abstract objects.
#4: Post edited by user avatar xamidi‭ · 2024-04-07T12:34:36Z (8 months ago)
  • All of this has already been dealt with on Metamath, see [mpeuni/bayesth](https://us.metamath.org/mpeuni/bayesth.html) or [asrt/bayesth](https://expln.github.io/metamath/asrt/bayesth.html).
  • At first, they had to decide on concrete formulations of ZFC axioms, which must be stated in a formal language. All referenced axioms (including definitions of, for example, [the class of probability measures](https://us.metamath.org/mpeuni/df-prob.html) and [conditional probability](https://us.metamath.org/mpeuni/df-cndprob.html)) are linked at the bottom of the site of the first link, and you can explore the whole proof by following the references to subproofs.
  • Note that these proofs are fully formalized and thus can be verified by a machine. This is always the case when deriving everything from axioms, rather than making intuitive statements in natural language, which are rather _social proofs_ in contrast to _formal proofs_, as [noted here](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/handbookI/ChapterI.pdf).
  • It appears to me that you underestimate the complexity of creating formal proofs from nothing, which is indicated by the mere amount of definitions that this theorem relies upon. Even though the theorem contains only one name of the person who completed it, it resulted from a big collaborative effort due being built upon this large framework.
  • Formal proofs work purely on syntax (i.e. structure) and not at all on semantics (i.e. meaning). Outsourcing the thinking process (which is susceptible to errors) to formal methods is precisely what axioms and proofs are meant for. Social proofs (which are most common in mathematics) just do not go all the way.
  • Which is mainly, because that would be too hard for most mathematicians to both create and conceive. After all, mathematics is a social framework for humans to intuitively understand abstract objects.
  • All of this has already been dealt with on Metamath, see [mpeuni/bayesth](https://us.metamath.org/mpeuni/bayesth.html) or [asrt/bayesth](https://expln.github.io/metamath/asrt/bayesth.html).
  • At first, they had to decide on concrete formulations of ZFC axioms, which must be stated in a formal language. All referenced axioms (including definitions of, for example, [the class of probability measures](https://us.metamath.org/mpeuni/df-prob.html) and [conditional probability](https://us.metamath.org/mpeuni/df-cndprob.html)) are linked at the bottom of the site of the first link, and you can explore the whole proof by following the references to subproofs.
  • Note that these proofs are fully formalized and thus can be verified by a machine. This is always the case when deriving everything from axioms, rather than making intuitive statements in natural language, which are rather _social proofs_ in contrast to _formal proofs_, as [noted here](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/handbookI/ChapterI.pdf).
  • It appears to me that you underestimate the complexity of creating formal proofs from nothing, which is indicated by the mere amount of definitions that this theorem relies upon. Even though the theorem contains only one name of the person who completed it, it resulted from a big collaborative effort due being built upon this large framework.
  • Formal proofs work purely on syntax (i.e. structure) and not at all on semantics (i.e. meaning). Outsourcing the thinking process (which is susceptible to errors) to formal methods is precisely what axioms and proofs are meant for. Social proofs (which are most common in mathematics) just do not go all the way.
  • Which is mainly, because that would be too hard for most mathematicians to both create and conceive. After all, mathematics _de facto_ is a social framework for humans to intuitively understand abstract objects.
#3: Post edited by user avatar xamidi‭ · 2024-04-07T12:33:31Z (8 months ago)
  • All of this has already been dealt with on Metamath, see [mpeuni/bayesth](https://us.metamath.org/mpeuni/bayesth.html) or [asrt/bayesth](https://expln.github.io/metamath/asrt/bayesth.html).
  • At first, they had to decide on concrete formulations of ZFC axioms, which must be stated in a formal language. All referenced axioms (including definitions of, for example, [the class of probability measures](https://us.metamath.org/mpeuni/df-prob.html) and [conditional probability](https://us.metamath.org/mpeuni/df-cndprob.html)) are linked at the bottom of the site of the first link, and you can explore the whole proof by following the references to subproofs.
  • Note that these proofs are fully formalized and thus can be verified by a machine. This is always the case when deriving everything from axioms, rather than making intuitive statements in natural language, which are rather _social proofs_ in contrast to _formal proofs_, as [noted here](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/handbookI/ChapterI.pdf).
  • It appears to me that you underestimate the complexity of creating formal proofs from nothing, which is indicated by the mere amount of definitions that this theorem relies upon. Even though the theorem contains only one name of the person who completed it, it resulted from a big collaborative effort due being built upon this large framework.
  • Formal proofs work purely on syntax (i.e. structure) and not at all on semantics (i.e. meaning). Outsourcing the thinking process (which is subsceptible to errors) to formal methods is precisely what axioms and proofs are meant for. Social proofs (which are most common in mathematics) just do not go all the way.
  • Which is mainly, because that would be too hard for most mathematicians to both create and conceive. After all, mathematics is a social framework for humans to intuitively understand abstract objects.
  • All of this has already been dealt with on Metamath, see [mpeuni/bayesth](https://us.metamath.org/mpeuni/bayesth.html) or [asrt/bayesth](https://expln.github.io/metamath/asrt/bayesth.html).
  • At first, they had to decide on concrete formulations of ZFC axioms, which must be stated in a formal language. All referenced axioms (including definitions of, for example, [the class of probability measures](https://us.metamath.org/mpeuni/df-prob.html) and [conditional probability](https://us.metamath.org/mpeuni/df-cndprob.html)) are linked at the bottom of the site of the first link, and you can explore the whole proof by following the references to subproofs.
  • Note that these proofs are fully formalized and thus can be verified by a machine. This is always the case when deriving everything from axioms, rather than making intuitive statements in natural language, which are rather _social proofs_ in contrast to _formal proofs_, as [noted here](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/handbookI/ChapterI.pdf).
  • It appears to me that you underestimate the complexity of creating formal proofs from nothing, which is indicated by the mere amount of definitions that this theorem relies upon. Even though the theorem contains only one name of the person who completed it, it resulted from a big collaborative effort due being built upon this large framework.
  • Formal proofs work purely on syntax (i.e. structure) and not at all on semantics (i.e. meaning). Outsourcing the thinking process (which is susceptible to errors) to formal methods is precisely what axioms and proofs are meant for. Social proofs (which are most common in mathematics) just do not go all the way.
  • Which is mainly, because that would be too hard for most mathematicians to both create and conceive. After all, mathematics is a social framework for humans to intuitively understand abstract objects.
#2: Post edited by user avatar xamidi‭ · 2024-04-07T12:27:48Z (8 months ago)
  • All of this has already been dealt with on Metamath, see [mpeuni/bayesth](https://us.metamath.org/mpeuni/bayesth.html) or [asrt/bayesth](https://expln.github.io/metamath/asrt/bayesth.html).
  • At first, they had to decide on concrete formulations of ZFC axioms, which must be stated in a formal language. All referenced axioms (including definitions of, for example, [the class of probability measures](https://us.metamath.org/mpeuni/df-prob.html)) are linked at the bottom of the site of the first link, and you can explore the whole proof by following the references to subproofs.
  • Note that these proofs are fully formalized and thus can be verified by a machine. This is always the case when deriving everything from axioms, rather than making intuitive statements in natural language, which are rather _social proofs_ in contrast to _formal proofs_, as [noted here](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/handbookI/ChapterI.pdf).
  • It appears to me that you underestimate the complexity of creating formal proofs from nothing, which is indicated by the mere amount of definitions that this theorem relies upon. Even though the theorem contains only one name of the person who completed it, it resulted from a big collaborative effort due being built upon this large framework.
  • Formal proofs work purely on syntax (i.e. structure) and not at all on semantics (i.e. meaning). Outsourcing the thinking process (which is subsceptible to errors) to formal methods is precisely what axioms and proofs are meant for. Social proofs (which are most common in mathematics) just do not go all the way.
  • Which is mainly, because that would be too hard for most mathematicians to both create and conceive. After all, mathematics is a social framework for humans to intuitively understand abstract objects.
  • All of this has already been dealt with on Metamath, see [mpeuni/bayesth](https://us.metamath.org/mpeuni/bayesth.html) or [asrt/bayesth](https://expln.github.io/metamath/asrt/bayesth.html).
  • At first, they had to decide on concrete formulations of ZFC axioms, which must be stated in a formal language. All referenced axioms (including definitions of, for example, [the class of probability measures](https://us.metamath.org/mpeuni/df-prob.html) and [conditional probability](https://us.metamath.org/mpeuni/df-cndprob.html)) are linked at the bottom of the site of the first link, and you can explore the whole proof by following the references to subproofs.
  • Note that these proofs are fully formalized and thus can be verified by a machine. This is always the case when deriving everything from axioms, rather than making intuitive statements in natural language, which are rather _social proofs_ in contrast to _formal proofs_, as [noted here](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/handbookI/ChapterI.pdf).
  • It appears to me that you underestimate the complexity of creating formal proofs from nothing, which is indicated by the mere amount of definitions that this theorem relies upon. Even though the theorem contains only one name of the person who completed it, it resulted from a big collaborative effort due being built upon this large framework.
  • Formal proofs work purely on syntax (i.e. structure) and not at all on semantics (i.e. meaning). Outsourcing the thinking process (which is subsceptible to errors) to formal methods is precisely what axioms and proofs are meant for. Social proofs (which are most common in mathematics) just do not go all the way.
  • Which is mainly, because that would be too hard for most mathematicians to both create and conceive. After all, mathematics is a social framework for humans to intuitively understand abstract objects.
#1: Initial revision by user avatar xamidi‭ · 2024-04-07T12:09:28Z (8 months ago) 
All of this has already been dealt with on Metamath, see [mpeuni/bayesth](https://us.metamath.org/mpeuni/bayesth.html) or [asrt/bayesth](https://expln.github.io/metamath/asrt/bayesth.html).

At first, they had to decide on concrete formulations of ZFC axioms, which must be stated in a formal language. All referenced axioms (including definitions of, for example, [the class of probability measures](https://us.metamath.org/mpeuni/df-prob.html)) are linked at the bottom of the site of the first link, and you can explore the whole proof by following the references to subproofs.

Note that these proofs are fully formalized and thus can be verified by a machine. This is always the case when deriving everything from axioms, rather than making intuitive statements in natural language, which are rather _social proofs_ in contrast to _formal proofs_, as [noted here](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/handbookI/ChapterI.pdf).

It appears to me that you underestimate the complexity of creating formal proofs from nothing, which is indicated by the mere amount of definitions that this theorem relies upon. Even though the theorem contains only one name of the person who completed it, it resulted from a big collaborative effort due being built upon this large framework.

Formal proofs work purely on syntax (i.e. structure) and not at all on semantics (i.e. meaning). Outsourcing the thinking process (which is subsceptible to errors) to formal methods is precisely what axioms and proofs are meant for. Social proofs (which are most common in mathematics) just do not go all the way.  
Which is mainly, because that would be too hard for most mathematicians to both create and conceive. After all, mathematics is a social framework for humans to intuitively understand abstract objects.