Tag: OpenLab 8
Logic on Math StackExchange
- .Formalizing the Provability of Unprovability in Lean 4: A Derivation via Löbâs Theorem [closed] April 16, 2026I am investigating the metalogical constraints on a consistent, recursively axiomatized theory T (extending Peano Arithmetic) regarding its ability to prove sentences about its own unprovability. Specifically, I've been looking at whether T can prove ÂŹProvT(âSâ) for some sentence S. and how this relates to the Second Incompleteness Theorem. To explore this rigorously, I formalized […]Sanand
- Can Infinite Time Turing Machines simulate computations of Ordinal Turing Machines for a specified countable time? April 16, 2026From the replies to one of my questions on Mathoverflow, I can conclude that Infinite Time Turing Machines can somehow simulate computations of Ordinal Turing Machines, but the whole situation is not clear to me. In this question, the term ârealâ implies an infinite binary seuence of length $\omega$. My question is the following: given […]lyrically wicked
- Terminology question: why "positive" in "contrapositive"? April 13, 2026The contrapositive of a statement "if $P$ then $Q$" is "if not $Q$ then not $P$". In Chinese "contrapositive" is translated to "conversion-negation" because it first converse the statement (if $Q$ then $P$) and then negates $P$ and $Q$. This makes me confused why in English it is called "contrapositive". Does "contra" correspond to "conversion"? […]Asigan
- Do we say a (deductive) argument is satisfiable? April 12, 2026A formula is satisfiable if it is true under some assignment of values to its variables. (source) A formula is valid if and only if it is true under every possible interpretation. (source) In terms of validity, deductive arguments may be either valid or invalid. An argument is valid, if and only if (iff) it […]Jason Cho
- List of statements in logic [duplicate] April 10, 2026In a book of basic propositional logic I do not expect any naturals. Nevertheless I see quite often "listsâ of statements like $q_1,\cdots,q_n$. Neither âlistâ nor $n$ are defined. The existence of the naturals is derived from set theory and logic. How can these "listsâ of statements be defined in logic without using the naturals?BW M
- Set theoretic definition of pre-image April 9, 2026Let $f : X \to Y$ and let $B \subseteq Y$. Then according to Wikipedia, the preimage of $B$ under $f$ is defined like \begin{align*} f^{-1}\bigl[B\bigr] = \bigl\{ x \in X \;:\, f(x) \in B \bigr\} \,. \end{align*} By definition, we have: \begin{align*} x \in f^{-1}\bigl[B\bigr] \iff x \in X \;\land\; f(x) \in B \,. […]Jacob Lockard
- Formalizing Behavioral Stability: A Proposed Model ($LE = R \cdot (L \oplus Lu) \implies \sigma_{\infty}$) [closed] April 9, 2026I have been working for 45 years on observing empirical human dynamics and collaborative systems. I am seeking to formalize a "Logic of Exploitation" ($LE$) intended for behavioral auto-regulation. My goal is to represent the transition from social chaos to systemic coherence. The proposed model is: $$LE = R \cdot (L \oplus Lu) \implies \sigma_{\infty}$$ […]Yan Clark
- Gödel's incompleteness theorems as a functional program April 8, 2026In the talk "Propositions as Types" given by Phillip Wadler, Wadler gives an overview of Gödel's incompleteness theorems, and then at 3:00, says: "Don't worry about the details about how he did [the theorem], although it is one of the world's first functional programs..." I was not aware of a connection between the incompleteness theorems […]tlonuqbar
- What is the best way to solve for n [closed] April 8, 2026Let n be a three-digit number such that subtracting the sum of the cubes of its digits from n results in the maximum number. Find the sum of all such numbers n.Lukas
- How do I prove that RAA logicaly follows from LEM via Natural Deduction? [closed] April 8, 2026How do I prove that RAA logicaly follows from LEM? I've asked some LLM's and they keep inserting meta language symbols into the proof. My books has not said that's ok, so I do not want to apply rules I do not understandenter image description here I'll give you an example of how it was […]Phlaelo
Recent Comments