Tag: OpenLab7
Logic on Math StackExchange
- Irreducibility of multi-level proof-mutation kernels May 16, 2025The recent AlphaEvolve white-paper shows how an evolutionary loop over token-level “diffs’’ can discover novel programs (which translates to novel mathematical solutions/objects based on a quality measure). Inspired by that framework, consider a proof-search analogue inside Lean. A state is a string that serialises the current proof script together with its open goals. Three stochastic […]user1632355
- Separation of types in a complete theory May 13, 2025I encountered the following problem: Let $T$ be a complete theory. Suppose that $p_i(\bar{x})\in S_n(T)\ (iuser1630448
- Why are some propositions in Principia Mathematica written like this? [closed] May 13, 2025While reading Principia Mathematica by Bertrand Russell, I stumbled upon this proposition with a dot I don’t understand: weird dot The dot to left of the second disjunction in this term confuses me. Can anyone please explain what every dot means?Holz
- How the two derived identities help prove that the 2-basis ensures $\mathtt{NAND}$'s functional completeness? May 10, 2025I am proving that $\mathtt{NAND}$ is functionally complete in Boolean algebra using Robert Veroff’s 2-basis for the Sheffer stroke ($\mathtt{NAND}$) from his paper (A Shortest 2-Basis for Boolean Algebra in Terms of the Sheffer Stroke). I need clarification on how two derived identities from the paper’s proof contribute to constructing the standard $\mathtt{NAND}$ expressions for […]Dang Dang
- What is meant by this statement of Lavwere about the arrow category? May 8, 2025I am reading the thesis, Functorial Semantics of Algebraic Theories by Lawvere. Starting on page 26, he describes the category of categories, with functors as morphisms. He describes some special objects in this category, which he names 0, 1 and 2. The first two are what you expect, and 2 is the arrow category, consisting […]Carlyle
- Is there a "true" value of BB(745)? May 7, 2025I was reading this reddit thread and I got confused by one part. I always thought that there is always a "true" value of BB(n), even though it might not be provable or findable. There is a 745-state Turing Machine that halts iff ZFC is inconsistent. By Gödel's second incompleteness theorem, ZFC cannot prove BB(745) […]David Lui
- Is it necessary the existence of a set to prove the existence of empty set? [duplicate] May 6, 2025I know that in a set theory like Z or ZF we can prove the existence of the empty set starting from the existence of any set (guaranteed for example from infinity axiom) using the separation axiom on the first order formula $x\neq x$. However, it seems to me that it is not really necessary […]Manuel Bonanno
- Does cut elimination imply invertability in some cases? May 6, 2025I am currently reading a paper presenting a (Gentzen-style) proof system without a cut rule. In it, cut elimination is proven first, so if $\phi \sqsubseteq \psi$ and $\psi \sqsubseteq \rho$ have proofs, then $\phi \sqsubseteq \rho$ does as well. In Theorem 4.1, he then claims that if $\phi \sqsubseteq \psi_1 \sqcap \psi_2$ has a […]Snek
- Does Godel's incompleteness really means that parsability of language entails ill-self-reference? May 6, 2025I want to make the following claim. Could you please correct me, thanks ? Godel's incompleteness theorem relies on the folding of higher order structure with the arithmetic one, leading to self reference which states impossible "liar sentences". This is due to the parsability of the sentences of FOL and its tree data structure. An […]Ok Ok
- What is the basis for assuming $V \neq L$? May 6, 2025My understanding is that Godel proved if $ZFC$ is consistent, then $ZFC + (V=L)$ is also consistent. But what about the negation, i.e. $V \neq L$? Is it similarly provable that if $ZFC$ is consistent then $ZFC + (V \neq L)$ is also consistent? Or is $V \neq L$ effectively an axiom that has to […]NikS
Recent Comments