particularuniversalbeing
46
10
particularuniversalbeing has not written any posts yet.
particularuniversalbeing has not written any posts yet.
... (read more)So the theory purporting to actually solve the Hard Problem of Consciousness needs to shed some light onto the nature and the structure of the space of qualia, in order to be a viable contender from my personal viewpoint.
Unfortunately, I am not aware of any such viable contenders, i.e. of any theories shedding much light onto the nature and the structure of the space of qualia. Essentially, I suspect we are still mostly at square zero in terms of our progress towards solving the Hard Problem of Qualia (I should be able to talk about this particular shade of red, and this particular smell of coffee, and this particular psychedelic sound and
Yes, terms in Prop are routinely defined nonconstructively, but this is all happening within the context of a constructive (or at least very much not set-theoretic) metatheory. So for instance LEM gets derived from choice by Diaconescu's theorem, types are conventionally supposed to be constructive, you sometimes have to care about definitional vs. propositional equality, etc.
Should ZFCbot get trained on random ZFC; random ZFC + library of theorems and conjectures and random combinations of high level maths concepts; or random ZFC plus whatever ChatMathsGPT keeps asking.
None of the above. The "foundations of mathematics" is called that because the field emerged in the context of the "foundational crisis" in the philosophy of mathematics; it does not serve as a practical foundation for math as practiced by mathematicians. The overwhelming majority of mathematicians work informally (which is still very formal by the standards of any other field), and my impression is that those who are interested in formal methods are mostly pursuing constructive/type-theoretic approaches. Lean, for instance, is based on the calculus of inductive constructions: "importing" mathlib into ZFC (without just building a model of CIC within it) would be incredibly difficult.
Although at individual level there is a trade-off between our personal preferences and the general interest, when we talk about “political philosophy”, we have to abstract (in the Rawlsian way) from our particular interests: the legislator is expected to impartially represent the demos. The formal translation of that demand requires building a social utility function that describes the collective preferences for each possible "state of the world". This function must be individualistic and impartial.
You're engaging in political philosophy right now! Or you would be, if you were attempting to defend this brand of technocratic liberalism instead of simply taking it as given.
I do mention that one should probably work with a LISP variant at some point, at a bare minimum. Being able to think in functional programming ways is definitely important
There's functional programming, and then there's functional programming. The term is overloaded almost to the point of uselessness: it mostly just means not-imperative. But beyond that, lisps have little in common with MLs.
Lisp is python done right, and is best suited for the same sorts of domains: those where inputs are messy and everyone is ok with that, runtime errors are easy to surface and cheap to fix, and mostly-right means mostly-as-good.
MLs are theorem provers done wrong done right, and lend themselves to a pretty much orthogonal set of problems: inputs are either well-structured or dangerous enough that they need to have a structure imposed on them, runtime errors can be subtle and/or extremely bad, and mostly-right means wrong.
if you're a logic freak it trains you to be comfortable with the insufficiency of symbols, memes and jokes of mathematicians and physicists disagreeing about notation reveals an underlying controversy about the question "what are symbols actually for?"
I don't think this is an accurate description of the cultural difference between physicists and mathematicians. Tiny respective minorities of die-hard instrumentalists and formalists aside, both fields agree that the symbols are just tools for talking about the relevant objects of study more clearly and concisely than natural language permits. Plenty of published math research is formally incorrect in an extremely strong sense, but no one cares as long as all the errors can be... (read more)
I expect to take several more late-undergraduate- to early-graduate-level math courses. Presumably some will turn out to be much more valuable to me than others, and presumably this is possible to predict better-than-randomly in advance.
Yes, but not in a uniform way. The mathematical frontier is so large, and semesters so short, that Professor A's version of, for instance, a grad level "Dynamical Systems" course can have literally no overlap with Professor B's version. Useful advice here is going to have to come from Professors A and B (though not necessarily directly).
what the math of agency ... is like
Underdeveloped. There's some interesting work coming out of the programming language theory / applied category theory region these days (Neil Ghani and David Spivak come to mind), but "the math of agency" is not even an identifiable field yet, let alone one mature enough to show up in curricula.
This might be useful in relatively young fields (e.g. information theory) , or ones where the topic itself thwarts any serious tower-building (e.g. archaeology), but in general I think this is likely to be misleading. Important problems often require substantial background to recognize as important, or even as problems.
A list of applications of sophisticated math to physics which is aimed at laymen is going to end up looking a lot like a list of applications of sophisticated math to astrophysics, even though condensed matter is an order of magnitude larger, and larger for sensible reasons. Understanding topological insulators (which could plausibly lead to, among other things, practical quantum computers) is more important... (read more)
Here's another approach, using tools that might be more familiar to the modal reader here:
This sort of "forwards on space, backwards on stuff" structure shows up pretty much anywhere you have bundles, but I often find it helpful to focus on the case of polynomial functors - otherwise known as rooted trees, or algebraic data types. These are "polynomials" because they're generated from "constants" and "monomials" by "addition" and "multiplication".
Viewed as trees:
A * x^0 is an A-labelled tree (all our trees have labelled nodes and are furthermore possibly labelled as trees, and the same is true of all their subtrees) with no nodes.A * x is an A-labelled
As someone who definitely has qualia (and believes that you do too), no, that's not what's going on. There's some confusing extra thing on top of behavior - namely, sensations. There would be no confusion if the world were coupled differential equations all the way down (and not just because there would be no one home to be confused), but instead we're something that acts like a collection of coupled differential equations but also, unlike abstract mathematical structures, is like something to be.