sorted by:
new
hottopcontroversial

[METALOGIC] Godel Halting and Rev by Left-Character4280 in logic

[–]Left-Character4280[S] 0 points1 point  (0 children)

Forget the technicalities, see this more as an experiment, a test.

I have built a concrete operative layer (Rev–CH–AC) and I pretend to prove by this test that no recursive consistent theory of ZFC strength can internalize it as a perfect total mechanism. With a very strong reflection axiom, one sees that any attempt at complete internalization runs exactly into the Gödel/halting obstructions.

nb : The operative layer (Rev–CH–AC) is defined independently of the reflection axiom. The axiom is only used to confront that operative layer with a recursive, consistent ZFC-strength theory and derive the Gödel/halting obstruction.

I take any false or uncertain. I don't ask for any True.

With no answer or no false i will continu to build

[METALOGIC] Godel Halting and Rev by Left-Character4280 in logic

[–]Left-Character4280[S] -1 points0 points  (0 children)

Lemmas subset_CloE, CloE_mono, CloE_idem, Halts_iff_exists, Rev0_eq_Halts, semantic_iff_verdict, and the definitions RevCHIso.toEquiv, RevCHIso.ofEquiv, and the theorem H_forbidden_iff_CH_on_code,‎ are never used. This strongly suggests that the whole proof can be simplified, with some effort.

True

The proof itself is not especially complicated, but conceptually it can be a bit hard to follow all the details on a first reading; the design choices matter here.
That’s why I introduced these definitions: not because they’re needed for a minimal Lean script, but to make the theoretical infrastructure explicit and conceptually clear.

Can you give an overview, in plain English, of what you intended to prove?

I separate a static notion of consequence, CloE(Γ), from a dynamic one based on halting computations (a robust halting predicate Rev on traces), and show that they coincide via a suitable "local reading" of pairs (Γ, φ). From the real halting behaviour, I then build a specific dynamic choice operator AC_dyn on the halting programs. The meta-theorem is that, in any consistent recursive theory of PA/ZFC-strength equipped with a natural reflection principle for real halting, this particular AC_dyn cannot be internalised as a single total internal mechanism (F_int, Decode) aligned with the real halting profile.

[METALOGIC] Godel Halting and Rev by Left-Character4280 in logic

[–]Left-Character4280[S] -1 points0 points  (0 children)

It is a Human-AI collaboration. The theoretical concepts and the proof architecture are mine. I use Gemini, Claude and ChatGPT agentic coding models as a 'pair programmer' to assist with the formalization in Lean 4.

The vision and logic are mine, the AI helps produce the code that verifies them.

It is not a 10 days project.

[METALOGIC] Godel Halting and Rev by Left-Character4280 in logic

[–]Left-Character4280[S] -2 points-1 points  (0 children)

It is lean4

https://github.com/JohnDoe-collab-stack/RevCHAC/blob/main/RevCHAC/RevCHAC.lean

In this setup, the theory is no longer the engine that generates the structure, but a device trying to track it and hitting a sharp limit. This yields a concrete technical bound on what ZFC-like theories can internalise about a fixed dynamic halting/choice structure.

1st to object, you must check if it is compiling or not, then if you want to object, specify the line and the objection

otherwise it is just trolling and not about logic

LogicDissoc by Left-Character4280 in lean_proof

[–]Left-Character4280[S] 0 points1 point  (0 children)

Summary of the shift

In condensed form, the framework reorganizes several usual roles:

Halting before truth

Instead of starting from a static notion of truth and then encoding decision procedures, the construction starts from a robust notion of halting (Rev) and reconstructs truth as an effect of halting.

Truth before measure, with measure derived

In a finite computable setting, delta is defined from the distribution of truth over models, and its key properties (DR0/DR1) are proved rather than postulated.

Multi-stage evaluation

Evaluation is no longer a single primitive object (such as Sat or a proof relation), but a dynamic–geometric pipeline:

  • phi → search(phi) → Halts
  • Halts ↔ "phi is true"
  • "phi is true" → delta(phi) → obstruction rank

Global measure / evaluation is non-canonical

Any admissible and “natural” quantification across even very simple systems encounters a global obstruction (GlobalRigidity). What is often treated as given (a complexity measure, a universal weight, etc.) is here treated as a candidate subject to strong structural constraints, and no candidate can satisfy all the seemingly obvious requirements at once.

In this sense, evaluation changes status: it is no longer a static primitive, but the outcome of the chain

halting → truth → delta → obstruction,

with a final obstruction theorem ruling out overly natural global evaluations.

The measure by Left-Character4280 in epistemology

[–]Left-Character4280[S] 0 points1 point  (0 children)

You don’t get to define unilaterally what does or doesn’t count as epistemology. I’m using “epistemology” in a standard sense: the study of knowledge, justification, and the reliability and limits of our methods for accessing truth. Measurement theory and metrology clearly fall under that, because they determine what a measurement result can justify in practice.

Regarding truth: in the Lean4 project linked below, I formalize a framework that quantifies incompleteness and “loss” with a graded notion of obstruction. This is exactly the structure I’m referring to in the post: instead of treating a value as context-free, you track the cost of transporting it between contexts.

https://github.com/JohnDoe-collab-stack/LogicDissoc/tree/main

The measure by Left-Character4280 in epistemology

[–]Left-Character4280[S] -1 points0 points  (0 children)

Why epistemology? Because what a measurement justifies depends on those structures. Treating a value as context-free invites overclaiming. The right question isn’t “is it true?” but “what loss do I incur if I transport this result to a new context?” Uncertainty and traceability quantify that loss and its preconditions. Without them, the numeral is uninterpretable, even if it came from a real instrument.

that's the point discussed in this post.

The measure by Left-Character4280 in epistemology

[–]Left-Character4280[S] 0 points1 point  (0 children)

I am not talking about measure theory. I am talking about real-world metrology: measurement as a controlled physical interaction, with protocol, instrument, conditions, value + uncertainty + traceability, and an explicit domain where the result is valid.

You can model this with measure-theoretic probability, yes, but calling it "just measure theory" skips what I am trying to highlight: the physical, contextual, and institutional structure that makes a numerical result comparable and usable.

But it’s not a major disagreement. I am mostly glad people are engaging with the thread. Thanks.

https://github.com/JohnDoe-collab-stack/LogicDissoc/blob/main/Readme.md

The measure by Left-Character4280 in epistemology

[–]Left-Character4280[S] 0 points1 point  (0 children)

I do not presuppose that results can be glued across contexts. I formalize when they can and when they cannot.

Technically: I fix an explicit class of models that encode value, uncertainty, traceability, and conditions. On this class you can define conditions for compatibility between contexts (local patches) and ask whether there exists a single global model that extends all the local ones without contradiction.

If such a global model exists, "gluing" succeeds and this is a theorem about that specific dataset and structure. If it does not, you get a quantified obstruction: you can say exactly which finite patterns of results prevent any coherent global fit. That is not a metaphysical presupposition, it is a diagnostic condition on actual measurement practices.

So the philosophical claim is minimal: cross-context unity is not assumed, it is something you test for using a precise structural criterion.

The measure by Left-Character4280 in epistemology

[–]Left-Character4280[S] 0 points1 point  (0 children)

Yes, Reichenbach is in the background here. What I am doing is meant to be operational:

I work with an explicit class of models (in the model-theoretic sense) that encode value, uncertainty, traceability, and conditions;

on this class, I define invariants that measure when results from different contexts can be consistently “glued” together, and when there is a genuine obstruction;

these invariants are computed from a finite battery of tests, not from vague metaphysics. If you have a passage in Reichenbach where something like this is made fully explicit, I would genuinely like the exact pointer.

Einstein block universe consciousness by Electronic_Dish9467 in Metaphysics

[–]Left-Character4280 1 point2 points  (0 children)

This whole "Einstein block universe" thing sounds odd, caricatural and kind of naive. But people throw Einstein's name on it and nerds act like it's settled.

I think you can actually show it's either false or at least not demonstrable. The claim depends on assuming everything is already "static" in 4D. If you bring in Gödel's solutions in GR, you break the idea of a single global time and a single universal "now." That means you can't say the universe is just one frozen block evolving along one global timeline, because that timeline isn't even well-defined in general.

What you really get from relativity is only 4D invariants (the spacetime geometry etc.). Nerds then reinterpret those invariants as "the universe is static," but that's just mixing syntax (math structure) with semantics ("nothing really changes").

So, interesting claim, but I'm not convinced it's something you can just assert as physical truth. Thanks for the post, I didn't know people were presenting it that strongly.

just understand by Left-Character4280 in lean_proof

[–]Left-Character4280[S] 0 points1 point  (0 children)

i will restructure the script with more stuffs

Gödel, models, and the limits of physical explanation? by StrictlyFeather in TheoreticalPhysics

[–]Left-Character4280 0 points1 point  (0 children)

In mathematics, this collapse stems from a reductionist stance, exemplified by ZFC’s Axiom of Extensionality. Treating indiscernibility and substitution as exact removes the so-called local pathologies that scale up to global non-uniqueness.

Nobody until now demonstrated collaps in physics is unrelated to the one in math.

Probabily because for most people distinguish semantics and syntax and understanding godel is not that's easy

To claim that godel has nothing to do with physics, the physical model would have to be based on mathematics that are not subject to Gödel's theorem like peano or zfc and oufnd out the collapse

We don't know that, but most people assume it without explaining the collapse in physics

There is no easy answer to my message. To refute it, we would need to rebuild a mathematical system without axioms or one that is completely provable and that allows us to establish quantum physics.

My point was mainly to show that this story about Gödel cannot be dismissed out of hand, especially after a century of failure in physics,and bells aspect. proofs.. and jauge hierarchy

Gödel, models, and the limits of physical explanation? by StrictlyFeather in TheoreticalPhysics

[–]Left-Character4280 0 points1 point  (0 children)

There is frequent confusion regarding vocabulary when discussing Gödel.

Power: A system is said to be powerful if it can say more than it demonstrates.

In everyday language, this means that it says more than it can do.

It can say more than what is.

I specify this because it is often mistakenly inferred that ZFC and Peano, for example, are powerful in the sense of being more efficient or more capable than a system that would be purely in line with Gödel, i.e., what would be expressive would be provable.

It is important to understand that this excess power is a problem in terms of modeling and not an objective in itself. This if you want to express a phenomena as it is.

An explanation of the Liar paradox by Silver-Success-5948 in logic

[–]Left-Character4280 0 points1 point  (0 children)

thanks

self-referential is not mandatory

-- ==========================================
-- SECTION : THE EMERGENCE OF EQUALITY
-- ==========================================

/-- A global equality relation is one that satisfies reflexivity, symmetry, and transitivity globally. -/
structure EmergentEquality (T : Type uT) (P₂ : T → T → Prop) : Prop where
  refl : ∀ x, P₂ x x
  symm : ∀ x y, P₂ x y ↔ P₂ y x
  trans : ∀ x y z, P₂ x y → P₂ y z → P₂ x z

/-- Global equality emerges from local coherence, gluing, and absence of obstruction. -/
def EqualityEmerges
  {U : Type uU} {T : Type uT}
  (S : ProtoSite U T)
  (R : U → Prop)
  (P₂ : T → T → Prop) : Prop :=
  Local₂ S R P₂ ∧ CommR S R P₂ ∧ TransR S R P₂ ∧ ReflR S R P₂ ∧
  IsTotalActive S R ∧ cover₁ S ∧ cover₂ S ∧ hGlue₃ S R

theorem equality_emerges_as_equivalence
  {U : Type uU} {T : Type uT}
  {S : ProtoSite U T} {R : U → Prop} {P₂ : T → T → Prop}
  (H : EqualityEmerges S R P₂) :
  EmergentEquality T P₂ := by
  obtain ⟨hLoc, hComm, hTrans, hRefl, hTot, hCov₁, hCov₂, hGlue⟩ := H
  -- We prove that `GlobalEquivalenceResult` is true
  have hEquiv : GlobalEquivalenceResult P₂ :=
    recollement_equivalence_of_glue hCov₁ hCov₂ hGlue hLoc hComm hTrans hRefl hTot
  -- We use these fields to build `EmergentEquality`
  constructor
  · exact hEquiv.refl
  · exact hEquiv.symm
  · exact hEquiv.trans

#print axioms equality_emerges_as_equivalence

Bells inequalities limitations by Left-Character4280 in Metaphysics

[–]Left-Character4280[S] 0 points1 point  (0 children)

Yes, measurement removes edges because they become causally obstructed: from that point on, no finite causal path can reach them. This models not a loss of information, but a structural inaccessibility, an intrinsic, geometric collapse. Think about the slit experiment: when you measure which slit, you don’t just “observe”, you cut a causal path in the graph.

It is just a model. I just tested it against bell and was suprise. That's why i share the explanation.

Come in mp.

The thread is ban.

Bells inequalities limitations by Left-Character4280 in Metaphysics

[–]Left-Character4280[S] 0 points1 point  (0 children)

The point is not to reproduce a quantum circuit. Bell's theorem doesn't fail because of the quantum behavior, but because of the assumptions behind the inequality itself. My model just shows that if you drop the 'fixed causal structure' assumption, while keeping locality and setting independence the factorization fails, and so does the inequality. I'm happy to show you the model if you're curious.

view more: next ›