1. If you are aiming at some fundamental physics, such as QFT, that still leaves out every non-fundamental theory that is not reducible to fundamental physics - which means pretty much everything, from solid state physics to derivative trading. Now, it is plausible, though still controversial, that, to the extent that they are accurate, those "special sciences" supervene on fundamental physics. — SophistiCat
What's the end game - something like Quantum Field Theory? — SophistiCat
If you are aiming at some fundamental physics, such as QFT, that still leaves out every non-fundamental theory that is not reducible to fundamental physics — SophistiCat
there isn't a unique construction — SophistiCat
If you read the OP you’d see that that’s just the midpoint. We build up to something like QFT, and then build from there to something like a human. I’m not specifying the exact route we must take or how far we can go but that’s the rough idea. — Pfhorrest
And the joint negation or complement operation is the sole sufficient operation, which returns the set of everything that is not any of the arguments fed into i — Pfhorrest
The game is to start with the most elementary of mathematical structures, and build from there up to the structure that is (on our best current understanding of physics) identical to (or if you really prefer, the perfect model of) our physical universe — Pfhorrest
To begin with, there is the empty set, and the empty set is without contents and void. — Pfhorrest
as I understand it the logical operations are all equivalent to set operations — Pfhorrest
I always forget that even among physicalists the reducibility of everything to fundamental physics in contentious. So I suppose that’s another presumption of this thread, and the thread itself can serve as the debate on that, as players put forward constructions of higher levels from lower ones and others challenge the accuracy of those. — Pfhorrest
↪fishfry I think you meant to quote the part where I wrote "And the complement of the empty set, all that is not nothing, is everything. The end." That part was a joke, and I immediately backtracked to get back to the actual point of that first post. — Pfhorrest
I could use a little clarification though, because as I understand it the logical operations are all equivalent to set operations, and as I understand it complement is the set-theoretic equivalent of negation, but negation isn't quite the same as joint negation though it can trivially be made to function as such (just feed an operand into both arguments of NOR instead of the single argument of NOT), so I'm not entirely sure if complement can be treated as the set-theoretic equivalent of joint negation too, or just plain unary negation, and in the latter case, what actually is the set-theoretic equivalent of joint negation? — Pfhorrest
Of course, we'd better load the propositional-logic language-extension pack, along with first-order extensions (universal quantifiers). Language must of course be "pluggable". Still, if we load the propositional-logic language extension pack, we must also load its axiom pack with the 14 basic rules of propositional logic. Language packs and axiomatic packs are not entirely independent. — alcontali
Yeah no this thread is not supposed to be demonstrating mathematicism, it's just assuming it, and as I said in the OP you can instead assume we're building a simulation of the universe instead, if that makes you more comfortable.expecting to show how the entire universe works mathematically (what some people seem to be reading the thread as) — fdrake
The "derive cells from sets" goal is very silly, the "show what math goes into some simple physical laws from the ground up" goal is not — fdrake
I'm not sure why NOR is important to you — fishfry
anything you can say in propositional logic you can say in predicate logic — Pfhorrest
anything you can say in propositional logic you can say in predicate logic — Pfhorrest
so if you start with sets you don't need to "manually" include propositional logic, it's one of the things you can build along the way. — Pfhorrest
Someone else please check this because I don't trust alcontali's word on this for various reasons, and my understanding is that from set theory you can build predicate logic, which serves as an extension of propositional logic (anything you can say in propositional logic you can say in predicate logic), so if you start with sets you don't need to "manually" include propositional logic, it's one of the things you can build along the way. — Pfhorrest
It would be fantastic if it were possible to derive the 14 axioms of propositional logic as theorems in ZFC, but I have not run into any documentation that confirms this or clarifies how to do that. I am absolutely not sure that it can be built along the way on top of ZFC. All documentation that I have seen up till now suggests that it is simply another, additional axiom pack. — alcontali
It's kinda redundant to start from sets then derive quantifiers (like for some being arbitrary disjunction over set elements, or for all being infinite conjunction over set elements). — fdrake
The syntax of type theory is more complicated than that of set theory. In set theory, there is only one kind of object; officially, everything is a set. In contrast, in type theory, every well-formed expression in Lean has a type, and there is a rich vocabulary of defining types.
In fact, Lean is based on a version of an axiomatic framework known as the Calculus of Inductive Constructions, which provides all of the following ...
Given this last fact, why not just use set theory instead of type theory for interactive theorem proving? Some interactive theorem provers do just that. But type theory has some advantages ... — LEAN on Dependent Type Theory
anything you can say in predicate logic you can say in first-order logic, which is what you need for PA or ZFC. Predicate logic is not sufficient. You need the universal quantifiers too — alcontali
I think you may be confusing propositional logic with predicate logic. — Pfhorrest
The set of axiom schemata of first-order predicate calculus is comprised of the axiom schemata of propositional calculus together with the two following axiom schemata:
∀ x F(x) ⇒ F(r)
F(r) ⇒ ∃ x F(x)
— Wolfram on first-order logic
I thought it was supposed to build a play-dough universe of solid, unerring, unassailable, elementary numbers. Such as 1, or 2, or... or 3, for instance. Not any of those newfangled numbers like, i, e, or pi. — god must be atheist
Do you know why this is needed? — alcontali
They do not see zeroth-order predicate logic as something that needs to be mentioned separately — alcontali
I don't, and if I'm reading them correctly, they together contradict my understanding of predicate logic, wherein "for all x, F(x)" does not entail "there exists some x such that F(x)", but only "there does not exist any x such that not-F(x)". Which makes me think I'm not reading that passage correctly. — Pfhorrest
No, we'll get to those eventually... if anybody actually plays the game instead of arguing about the premise of it. I mean, I can build you the integers, rationals, reals, and complex numbers in my next post if you like, though I'm not up to building arithmetic out of set operations alongside it, so I was hoping someone else would do that. — Pfhorrest
so if you start with sets you don't need to "manually" include propositional logic, it's one of the things you can build along the way. — Pfhorrest
Difference from set theory. There are many different set theories and many different systems of type theory, so what follows are generalizations. Set theory is built on top of logic. It requires a separate system like predicate logic underneath it. In type theory, concepts like "and" and "or" can be encoded as types in the type theory itself. — Wikipedia on type theory
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.