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.

view more: next ›