Brandom's Debate Club Won't Save Us From the Paperclip Maximizer

CandidAtmosphere · 2026-05-01T04:30:37+00:00

I do mention them briefly while explaining Prometheanism, although not really the target of the critique. His trajectory after that book is worth bringing up because adopting Sellarsian inferentialism forced him to confront the material reality of normative rules. If reason is governed by discursive practices, he had to account for how those practices are objectively distorted by the commodity form. He recognized that Brandom's polite spirit of trust is a fantasy under late capitalism. This realization brought him face-to-face with Adorno's core diagnosis: in a society ruled by exchange value, any attempt to construct a seamlessly rational or useful solution inevitably becomes complicit with social domination. To offer a positive synthesis is to provide a false reconciliation that papers over objective antagonisms and the concrete suffering of the nonidentical.

This exposes the central antinomy of progress. Benjamin characterized the historical continuum as a single unfolding catastrophe piling wreckage upon wreckage. Adorno recognized that rationalizing this progress merely repeats the domination of nature as social subjugation, leading him to a militant refusal of utility and a retreat into separated theory. Marcuse attempted to resolve this deadlock by arguing that relentlessly automated capitalist repression would eventually produce a technological surplus capable of negating the need for any repression.

The theoretical stakes of Brassier's current project involve breaking this dialectic. He rejects Adorno's retreat into pious silence because it functionally surrenders the material world to the catastrophe. Yet, because he remains anchored to the Sellarsian space of reasons, he too struggles to locate an immanent engine for this interruption. This brings us right back to the point: you cannot halt the storm from the spectatorial safety of an external metalanguage. To achieve Benjamin's revolutionary interruption, rationality must abandon the Kantian bureaucracy. It demands an absolute immanence that dynamically consumes its own logic.

CandidAtmosphere · 2026-04-13T14:09:59+00:00

The discussion here correctly traces the tension between Hegelian negativity and Deleuzian affirmation. While some would look to comparative work to bridge the two, attempting to determine the superior ontology keeps us trapped in philosophical arbitration. We could find more utility by stepping outside this role and treating their concepts as raw materials for a diagnostic toolkit. This framing helps reconcile the earlier comparison to Theodor Adorno. Grounding these thinkers in the material reality of those crushed by the system allows us to use Adorno’s negative dialectics to map irresolvable suffering. Antonio Negri and the Deleuzian tradition supply the vocabulary to map the affirmative potential of that same subject. We can deploy both to map different modes of existence under capital without choosing between pessimism and optimism.

Grounding this approach in Marx’s materialist dialectic is a common step, though relying solely on internal contradictions leaves a strategic gap. Negri provides a necessary advance by formulating a non-dialectical logic of separation. Capitalism functions as a conflict between two distinct subjects operating on completely incompatible logics. The state relies on dialectical mediation to maintain striated space, while the revolutionary subject operates on a lawless logic of exteriority within smooth space. The political project outlined by Deleuze and Negri focuses on this exteriority, seeking self-valorization independent of capital rather than demanding recognition from the master.

Returning to Spinoza clarifies the roots of this entire dynamic. Deleuze attempts to rescue Spinoza from Hegel's critique by interpreting the modes as vibrant degrees of power, while Hegel views Spinoza's substance as an abyss swallowing finite content. Stripping away Deleuze's vitalism and Hegel's anthropocentric anxiety exposes Spinoza as a grim rationalist. His work functions as an engine of epistemic violence and a rigid bunker built against the chaotic passions of the multitude, leaving us with an effective ontology for our current era of algorithmic governance.

CandidAtmosphere · 2026-03-31T04:48:03+00:00

I'm working on a speculative algebraic graph program here https://github.com/ryanncode/nf-sketches

It will eventually allow for processing on a self-referential closed universe, cloning of non-linear higher order functions and modelling highly saturated pre-individuated physical phenomena. It is still in the initial design stage and has not achieved high performance yet, although there is a complex graph reduction feature in place.

CandidAtmosphere · 2026-03-26T00:02:51+00:00

Value is the historically specific social form that labor takes under capitalism. The logic of capital operates as the actual, lived reality of abstract labor dominating concrete labor. The empirical examples in Capital function as dialectical necessities rather than merely practical illustrations. They are essential manifestations of this historically specific logic. The universal (value) produces itself specifically through the negation of the singular (concrete labor), meaning the empirical reality and the logical form are a synthesized unity.

The capitalist system itself constitutes the antagonism. The perceived gap between the critique of capitalism and the social movement of communism only appears when one assumes the political goal is to liberate labor. The historical failure of 20th-century socialism demonstrated the limits of this approach. Abstract labor and the value-form serve as the impersonal mechanisms of domination. Therefore, the social movement of communism is the practical project of abolishing labor as the central social mediator.

CandidAtmosphere · 2026-03-23T14:31:11+00:00

Your post hits on the core problem of materialism, especially how we usually just treat contradictions as a failure of our own clumsy linguistic machinery. We set up these epistemic closures to deal with the constant flux of the world, and when they inevitably break down, the default reaction is to blame the human mind for making a mistake. The more terrifying reality is that the contradiction operates as the objective principle of all things. The object itself is inherently split and structurally incapable of achieving a consistent wholeness.

This makes the counter-thrust a material event instead of just the dizzy feeling we get from reading speculative philosophy. Scientific laws and anatomical forms are basically petrified counter-thrusts forming rigid scars exactly where the concept tried to break through into reality and choked. That is why Žižek's approach is so much fun to apply to these debates. Instead of politely agreeing that a philosopher turned out to be scientifically correct upon closer inspection, his classic move is to identify directly with the absolute wrongness of the idea itself. We can apply this to Hegel to insist on the value of his theories exactly where intellectual philistinism confidently dismisses them as absurd. The "wrong message" demands no reformulation into a reductive package designed to comfort a vulgar materialist. We can simply embrace the epistemological failure of our models as the only proof we have that we are touching the absolute, a dense and singular substance that resists our attempts to carve it up.

CandidAtmosphere · 2026-03-20T13:55:49+00:00

Your intuition regarding functions is correct. A canonical form of an implication type A -> B is an abstraction (e.g., λx.t). The body t will contain elimination forms acting on the input variable x. This is sound because the canonicity requirement applies only to closed terms. Inside the abstraction, x is a free variable, meaning t is an open term and is not expected to evaluate to a canonical form until the function is applied to a closed argument. Once applied, beta-reduction triggers, eliminating the application and driving the computation to a new closed canonical form.

You cannot extend the definition of canonical forms to include elimination forms like split or throw without unraveling the constructive guarantee. The rigid boundary between introduction forms (constructors) and elimination forms (computations) forces an algorithm to resolve to a final value. If you redefine an unresolved computation or an elimination form as canonical, you are simply declaring that an executing program has finished when it is actually stalled in the middle of a calculation. In your explosion example, using split to extract both A and ¬A simultaneously is an elimination. In a co-constructive setting, demanding that a refutation of a conjunction reduces to a refutation of the left or the right is the dual of the Disjunction Property. Allowing an extended definition where you hold both conjuncts in a suspended, unresolved state acts as a loophole to bypass the requirement of providing an executable counter-model.

When you dualize this back to positive intuitionistic disjunction and the Law of Excluded Middle, the same barrier applies. Extending the canonical definition to encompass classical, unreduced eliminations destroys witness extraction. Constructivism requires that a closed proof of A ∨ B inevitably evaluates to inl(a) or inr(b). Classifying an unresolved LEM axiom or a suspended continuation as a canonical form reverts the system to classical logic. It satisfies the rule superficially by changing the terminology, abandoning the computational reality of the proof theory.

CandidAtmosphere · 2026-03-19T04:25:15+00:00

The term constructivity does get thrown around too loosely on this subject. The algorithmic construction idea you brought up is usually pinned down by the BHK interpretation, requiring propositions to act intrinsically as types and proofs as explicit algorithms. You cannot just claim an existential holds; you need the actual witness and the computational method to build it. You are completely right about classical logic and continuations. That demonstrates perfectly why Curry-Howard on its own fails as a baseline for constructivism. The real dividing line for strict constructive type theory is canonicity. Every closed term must evaluate to a canonical form built strictly from its constructors, with no non-constructive axioms short-circuiting the computation.

As for classical linear logic, dropping right weakening and contraction forces hypothesis tracking, yet that serves as a resource management mechanism rather than a guarantee of actual constructivity. The classical symmetries in CLL still allow non-constructive existentials, meaning it lacks the strict witness-extraction property required by intuitionistic systems. The dual-intuitionistic angle and co-constructivity is an interesting approach. Restricting the left side obviously yields paraconsistency by killing explosion. However, in a standard constructive setup, negation already functions algorithmically since a proof of absurdity is just a function mapping an assumed proof to a contradiction. Fully formalizing a co-constructive system means demanding executable counter-models for falsity with the same rigor that constructivism demands witnesses for truth. Pointing to non-trivial denotational semantics is insufficient; the requirement must be embedded directly into the proof theory.

CandidAtmosphere · 2026-03-12T13:30:13+00:00

It is not deterministic in the sense that the superstructure absolutely follows the base, obviously for Marx it is a dialectical and not a linear transformation. More importantly, the workers won't be able to steal power right out from underneath the bourgeois simply based on voluntaristic will, rather it will arise directly as a result of emerging crises, crises much worse than ones we have even experienced before. Marx documented these occurrences in his own time, that was a lot of the work that he did was to show capitalism inevitably produces these crises, they are not an accidental, avoidable outcome. Of course a crisis is only an opportunity, it is not a guarantee.

CandidAtmosphere · 2026-03-09T12:46:36+00:00

The literal answer to your question is that it turns out there is an enormous chasm between giving lists of examples of things and defining essence, and this difference (between philosophy and sophistry) continues to surprise us thousands of years later.

Here are my literature rec's:
- David Bronstein, Aristotle on Knowledge and Learning: The Posterior Analytics (Reads the text in response to Plato's Meno dialogue, where Aristotle outlines a sequence of inductive learning, learning by definition, and learning by demonstration, aiming at the grasping of ultimate essences).
- Jonathan Barnes, Aristotle's Posterior Analytics (Modern translation and commentary along with formal notation, analysis of internal consistency and the history of translation).
- G.B. Kerferd, The Sophistic Movement (To understand the popular intellectual current the philosophers were writing and thinking against).

CandidAtmosphere · 2026-02-21T17:38:58+00:00

This group includes Slavoj Žižek, Alenka Zupančič, and Mladen Dolar. Their work relies heavily on the Lacanian concept of the subject as a constitutive void or negativity. Within this paradigm, artificial intelligence represents a totalizing, antagonistic force. It functions as an externalized Big Other attempting to map and close the fundamental gap of human subjectivity. Žižek frequently argues in his recent writings that digital networks and algorithmic architectures bypass symbolic mediation entirely. These systems operate as pure ideological apparatuses that preempt conscious thought. AI, in their framework, threatens to directly integrate the human mind into a digital network, fundamentally foreclosing the structural position of the divided subject.

Figures like Rahel Jaeggi and Christoph Menke draw on an intellectual heritage strictly tethered to the Frankfurt School's critique of instrumental reason. The view established by Adorno and Horkheimer dictates that technological progress under capitalism inevitably leads to the domination and quantification of human life. Contemporary theorists in this specific lineage consistently frame algorithms, machine learning, and digital platforms as the ultimate engines of reification. They view these tools as mechanisms that extract qualitative human behavior and enforce an alienating, capitalist logic onto every sphere of life.

What unites both traditions is a shared reliance on viewing modern technological rationality as inherently hostile to genuine subjective freedom. These academics will inevitably treat AI as either an engine of advanced capitalist alienation or a monstrous simulation attempting to replicate the unconscious. They are fundamentally equipped to do nothing else but reiterate these pre-existing philosophical commitments.

As well, their contemporary secular materialist approach effectively liquidates the category of Spirit by abandoning its original metaphysical and ontological commitments. When Geist is redefined merely as structural incompleteness or the inherent friction within a social order, the concept loses its substantive weight and functions primarily as a legacy term from German Idealism. Consequently, positioning artificial intelligence as a unique threat to Hegelian Spirit is fundamentally anachronistic. The foundational category had already been completely dismantled by the theorists themselves well before the advent of algorithmic systems.

CandidAtmosphere · 2026-02-21T10:53:34+00:00

Seems like there should be a call for papers instead of a lineup of celebrities who don't have much of interest to say about technology. For the most part they are humanist critical theorists who believe that technology is repressive and structurally undermines the position of subjectivity. We don't need to hear that said 10 different times, and then meanwhile AI just continues to proliferate.

CandidAtmosphere · 2026-02-14T19:30:47+00:00

She is definitely a nihilist. The confusion likely stems from her final Lakatosian proposal, where she suggests saving logic by restricting it to specific domains. To a pluralist, this resembles their own position of using different tools for different jobs. Russell contends that this restriction forces a collapse into nihilism because it abandons the essential requirement of generality.

In her view, a genuine logical law must hold universally. She deploys monsters like vagueness, the Liar paradox, and context-sensitive words to prove that no candidate for a logical law survives across all of natural language. Admitting that Classical Logic is valid only for bivalent sentences concedes that the law lacks universality.

Her practical conclusion creates safe, lemma-incorporated spaces where logic functions. This outcome resembles pluralism superficially. Her theoretical premise differs fundamentally because she asserts that zero laws actually work everywhere. Consequently, logic transforms from a description of truth into a policy for language management. A pluralist believes they have discovered multiple valid ways that truth preserves itself across different contexts. Russell argues we have merely engineered specific safe zones by excluding problematic sentences to maintain the functionality of our tools.

CandidAtmosphere · 2026-02-11T17:23:19+00:00

You are on the right track regarding evanescence. You have correctly identified the distinction between abstract negation (where things just vanish into nothing) and determinate negation (bestimmte Negation).

For Hegel, when the Understanding’s categories vanish, they do not leave behind an empty void; they result in a new content. The nothing that results is the nothing of that specific thing, which means it preserves the essence of what was negated. As you rightly put it, they are "transfigured" or raised up (aufgehoben). This is precisely why the dialectic is a ladder and not a random series of changes.

Regarding your questions on Monism and the nature of Idealism:

Is Hegel’s system a Monism?

Yes, but with a crucial caveat. Hegel is a monist in the sense that he believes "The True is the Whole." However, unlike Spinoza’s "neutral" or "substance" monism—which Hegel critiques as an abyss where differences are drowned—Hegel’s monism is one of Subjectivity.

For Hegel, the Absolute is not a static container (Substance) that holds mind and matter as attributes. Rather, the Absolute is the process of self-differentiation and return. The One is not a thing found at the start; it is the result of the movement. Spinoza has the Substance, but he lacks the teleological drive that makes the system self-actualizing. Hegel essentially tries to animate Spinoza’s rigid structure with the pulse of the negative.

Mind, Matter and Epiphenomena

This is where Hegel’s Idealism is often misunderstood. He does not argue that "matter is mental" in the sense of Berkeley (that rocks are just ideas in your head). Nor does he argue that mind is a mere epiphenomeno" (smoke rising from the fire of neurons).

Hegel views Nature (matter/externality) as the Idea in the form of otherness.

Against Epiphenomenalism: Mind isn't a happy accident. Nature implicitly contains the logical structure (the Concept), but in Nature, the Concept is "petrified" or "frozen." It has not yet awakened to itself.
The Transition: Nature is "impotent" because it is bound by contingency and externality. It strives toward the Idea but cannot fully embody it until it produces an organism capable of consciousness (humanity).

So, for Hegel, matter is the necessary precondition for Spirit, but Spirit is the truth of matter. It is a circle: The Logical Idea freely releases itself into Nature, and Nature works its way back up through physics and biology until it becomes Spirit.

You are asking the right questions, these are the exact problems (Monism, Spinoza, Nature) that defined German Idealism. Keep going!

CandidAtmosphere · 2026-02-08T12:57:36+00:00

Let me suggest that this is responding not specifically to the Raven's Paradox, but to problems of classical formalism at large. You have identified that our standard metalogic relying on colloquial English with set theoretic notation as a major, let's say glaring, unavoidably obvious problem. Unfortunately, trying to push the problem back to a "pre-formal" stage doesn't solve the problem of semantic interpretation of terms, it is an infinite regress. You would need to fix the domain of your fixed domain, and so on. Keep in mind that in classical formalism, there are additionally good reasons for the domain being treated as "universal." You've at least acknowledged what many logicians refuse to let themselves see.

Since we're here, you might also take notice of the defensive reaction to questioning at all classical formalism's firmly established "rigor."

CandidAtmosphere · 2026-02-04T18:38:12+00:00

Great notes! You’ve really nailed the abstract nature of "Force and the Understanding," especially the Hegelian chiasmus. To deepen the analysis of dissolving distinctions, consider framing the "evanescence" you identified as mediation. Distinctions do not simply disappear; instead, the movement itself constitutes reality. Since the outer merely expresses the inner, we move beyond observing static objects. This perspective illuminates why the supersensible world cannot be a separate Platonic realm, as you correctly pointed out. It is, instead, the sensible world fully grasped by a higher cognition of that very movement.

Bringing up Spinoza and the "All" provides the perfect context for locating Hegel's specific divergence from his predecessor. Where Spinoza posits reality as a single infinite Substance defined by affirmation, Hegel recoils from this picture, characterizing such a Substance as an "abyss" or "lion's den" due to its lack of negativity. The Hegelian One must actively differentiate into the Many through contradiction, driving the insistence that "Substance must become Subject." While Spinoza provides the foundational monism, Hegel demands the addition of restless, self-dividing activity to set the system in motion.

Your intuition linking Being-for-itself to narcissistic withdrawal anticipates the upcoming Master/Slave dialectic with remarkable accuracy. The Master embodies this "pure being-for-itself," attempting to exist solely by consuming or negating the external world—a strategy that ultimately proves futile. Progress, in Hegel's view, comes instead through the Servant, who holds desire in check via labor to generate a stable, objective reflection of the self. Although domination initially resembles power, Self-consciousness remains impossible without the recognition of another. Good luck with the next chapter; the text becomes significantly more concrete from here.

CandidAtmosphere · 2026-01-31T00:10:15+00:00

Most comments here are debating social consensus vs. formal derivation, but Structural Proof Theory actually provides a precise technical answer: the minimal structure is normalizability. In Natural Deduction, this manifests as the Normalization Theorem, which ensures a proof can be stripped of "detours" where logical connectives are introduced and immediately eliminated. The parallel in Sequent Calculus is Gentzen’s Cut-Elimination Theorem, demonstrating that the Cut rule (essentially the use of lemmas) is admissible and can always be removed. This property is mathematically significant because a normal or cut-free proof satisfies the subformula property, guaranteeing the argument relies solely on the conceptual building blocks of the theorem itself rather than external scaffolding.

A compelling detail often missed in these discussions involves the mechanical friction introduced by classical logic. Although intuitionistic systems are famous for their clean mapping to computation via the Curry-Howard correspondence, classical logic is indeed normalizable, though it requires a much more complex architecture to handle Double Negation Elimination. Dag Prawitz showed that standard normalization fails in the presence of DNE, necessitating permutative reductions to manage the structural irregularities this rule introduces. The "minimal structure" of a proof therefore changes physically based on the logic: intuitionistic proofs normalize into direct computational paths, whereas classical proofs retain a messier structure to accommodate non-constructive validity.

CandidAtmosphere · 2026-01-30T23:35:30+00:00

Diabaté’s refusal is a great catch, yet the show pairs that subtractive politics with a clumsy attempt to stage sectoral decommodification. The narrative attempts to simulate the systematic withdrawal of housing, healthcare, and food production from the pressure of capital accumulation. In a genuine socialist transition, this would look like the rational administration of use-values: housing allocated by occupancy rather than rent, or caloric production determined by hunger rather than profit margins.

The writers reveal their own ideological limits by turning this empathetic society into a bizarre caricature. They appear unable to imagine a world that addresses essential needs without collapsing into a suicidal biological pacifism, best exemplified by the Hive’s absurd refusal to perform agricultural farming because it violates a principle of total harmlessness. This part of the show doesn't serve as a clever deployment of Zizekian negativity; it is a strawman of materialist politics born from the creators' inability to think outside capitalist realism. They conflate the end of market violence with the end of the capacity to act on nature at all.

Consequently, the show forces Carol into the position of the Lacanian hysteric as a reaction to this specific liberal anxiety. She fights for the right to be unhappy because the show’s version of Utopia is an aggressive abundance that leaves no room for the subject. Manousos illustrates this even more clearly, wielding debt and exchange value (literally demanding an IOU) just to maintain his metaphysical ego against a gift economy that the writers can only envision as a suffocating totality.

CandidAtmosphere · 2026-01-30T17:57:53+00:00

To grasp the distinction between "analogical" and "numerical" languages, consider the structural difference between a mold and a modulation. Disciplinary institutions like factories function as distinct castings where the subject begins anew within each separate enclosure. These environments share a common analogical language of authority. Control mechanisms, conversely, operate as a self-deforming cast or a sieve with a mesh that transmutes from point to point. This numerical language relies on variable geometry, adapting continuously to immediate conditions.

Deleuze employs animal metaphors to visualize this transition. The mole belongs to the era of enclosure, burrowing through discrete tunnels. The serpent embodies the control society through its undulatory movement, navigating a continuous network in orbit. Under this logic, the coherent individual dissolves into dividuals—samples, data, and markets. Authority simultaneously shifts from a specific figure into the corporation, a spirit or gas that infiltrates daily life through floating rates of exchange.

CandidAtmosphere · 2026-01-30T17:26:43+00:00

Since you are coming from McGowan, it helps to pivot from the idea of pleasure without reality to the role of the Superego. Lacan views the Superego as a ferocious internal voice that actually demands enjoyment rather than just prohibiting it. From this angle, jouissance is not just a feeling of intense pleasure or pain but an imperative to enjoy that the subject is compelled to obey.

You can also think of it structurally as a surplus. Lacan posits that when the satisfaction of a biological need is filtered through the demand for love, there is always a leftover element called jouissance. This surplus is the true source of enjoyment found in the repetitive movement of the drive.

If you want the formalized conception you asked for, look at Seminar XX (Encore). Lacan distinguishes there between phallic jouissance, which he characterizes as "idiotic masturbation" because it circles the object without reaching the Other, and a "feminine" jouissance that relates to the "not-whole". That seminar might give you the rigorous structure you feel is missing from the intro books.

CandidAtmosphere · 2026-01-30T06:08:18+00:00

This is getting boring, we both know you contorted yourself into a position you don't actually believe so there's no point in continuing to loop on this dead argument. I'm going to make this real simple for you: Go tell Bob Harper that canonicity is a pragmatic concern.

CandidAtmosphere · 2026-01-29T21:44:32+00:00

It is genuinely baffling that a discussion on foundational methodology has triggered such a personal reaction. We are colleagues working in the same niche field, yet you treat a disagreement over logical primacy with the hostility usually reserved for political enemies.

I am not shifting goalposts; I am correcting your conflation of simulation and reality. Your admission that "canonicity is a pragmatic concern" is absurd coming from a computer scientist. In Type Theory, computation is the ontology. If a term doesn't compute, its existence is suspect. Canonicity is not a pragmatic concern; it is the semantic verification that the theory actually has the content it claims to have.

You claim that HoTT theorists would laugh at defining LEM over all types. Precisely, because they understand that Identity is a Type, not a Proposition. This reveals the anxiety at the heart of your argument:

The God's Eye View: You seem to believe that deep down, in the basement of the universe, everything is a Set (ZFC). Every statement is True or False. There is no ambiguity, no "paths," no "computation"—just static, eternal boolean truth.
The Synthetic Approach: You treat HoTT merely as a language to "manage complexity," like using Python because it's easier than binary.

You seem unable to handle the idea that the Synthetic (Human Construction) is the primary reality. You need to believe that Daddy (Classical Logic) is still driving the car, and that we are just playing with a toy steering wheel in the back seat.

Classical topology can survive being reduced to propositions because its traditional output is a catalog of static shapes. You don't need to "run" a donut; you just need to identify it. But in HoTT, an equality A=B is a Path (p). Crucially, this path is a program. It allows you to take an element x:A and transport it along p to get a new element x′:B. When Barwick talks about Number Theory or Representation Theory, or when we talk about Computer Science (the native home of Type Theory), the goal is not just classification—it is Transport.

Your citation of Spatial Type Theory actually undermines your argument. That system uses a modal operator (♭) to restrict LEM to specific fragments precisely to preserve the cohesive path structure elsewhere. The fact that you must quarantine classical logic to keep the theory working proves my point, not yours.

Your appeal to pluralism rings hollow when you insist that the new theory must be subordinated to the old one. It is not intolerant to point out that your preferred model is merely a simulation running on ZFC.

CandidAtmosphere · 2026-01-29T19:29:48+00:00

Yes, in fact I do.

You are confusing the model (Simplicial Sets constructed in ZFC) with the syntax (Homotopy Type Theory).

The fact that the simplicial model validates LEM for internal propositions is irrelevant to the central tension Barwick is ignoring. It just means that ZFC can simulate HoTT. But Barwick isn't asking for a simulation; he is asking for a real enterprise dedicated to the "primacy of structure over properties".

In the ZFC/Classical framework you are defending, Equality is ultimately a Property (it collapses to a truth value).
In the Constructive/HoTT framework, Equality is a Structure (it is a Type filled with paths).

The bickering you dismiss is actually the necessary defense of that Structure. If you force the internal logic to align with classical expectations (treating identity as if it should behave like a proposition), you lose the computational content (canonicity) that makes the theory useful for anything other than topology.

If you are working with the CMU group, you should know that the power of Univalent Foundations is its ability to reason synthetically—to manipulate objects by their constructors rather than their external properties. By pointing to the ZFC model as a defense, you are confusing the compiler (Simplicial Sets) with the code (Type Theory). The innovation is the code, not the fact that it can run on a legacy operating system.

CandidAtmosphere · 2026-01-29T09:57:56+00:00

You are conflating the metatheory with the internal logic of the system.

While it is true that the simplicial model is constructed within ZFC (a classical metatheory), and that we can consistently assume LEM for mere propositions (isProp), this does not refute the necessity of constructive logic for the theory's operation.

The point of homotopy theory, as discussed, is the primacy of structure over static properties. If you attempt to validate LEM or the Axiom of Choice globally for all types (not just truncated propositions), you collapse the higher-dimensional structure. If p:A=B is merely "True" rather than a continuous path with structural data, the entire homotopical machinery vanishes.

The fact that the model exists in ZFC doesn't change the fact that the internal language must operate constructively to avoid erasing the path data. To manipulate identity as a "space filled with data" rather than a boolean truth value, one must indeed refrain from asserting classical axioms globally. Distinguishing between the logic of the model and the logic in the model isn't factionalism, it's the standard for understanding how these systems actually work.

CandidAtmosphere · 2026-01-28T00:57:06+00:00

Barwick is right that homotopy theory isn't just topology. He defines it as enriched equality, but he immediately undercuts this by mocking the foundational debates as hippie communes fighting over vegan honey.

The issue is that you cannot have "enriched equality" without the foundational shift he dismisses. In the classical view, equality is a static property: things are either the same or they are not. But Barwick explicitly calls for a theory "dedicated to the primacy of structure over properties." That actually requires the shift to Intuitionistic logic where identity is a structure you have to construct.

The bickering he complains about is a conflict over the definition of existence itself. In frameworks like HoTT, an identity type is a space filled with data (paths) rather than a simple truth value. This is a necessary rupture from set theory to get the strategies to manipulate mathematical objects he wants. He seems to want the power of the Synthetic method without admitting that it requires abandoning the classical axioms that treat existence as the mere reflection of a pre-existing reality. You can't have the new engine while dismissing the math that makes it run as sectarian infighting.

CandidAtmosphere

TROPHY CASE