Tag: Open Lab 8
Logic on Math StackExchange
- Proof of the General Deduction Theorem December 6, 2024Theorem: For all axiom systems $\Sigma$ and all formulas $\varphi, \psi_1, \ldots, \psi_n$, it holds that: $ \Sigma, \psi_1, \ldots, \psi_n \vdash \varphi \iff \Sigma \vdash \psi_1 \to \ldots \to \psi_n \to \varphi$ Proof: $\Rightarrow$: We prove by complete induction. Initially, that is, for $n = 1$, it holds: Let $\Sigma, \psi_1 \vdash \varphi$, and […]God
- Existence of a model of $\mathsf{ZFC}$ which has the internal standard model of arithmetic coincide with the real standard model of arithmetic December 6, 2024$\mathsf{ZFC} + \operatorname{Con}(\mathsf{ZFC})$ can prove that there is a model $M$ of $\mathsf{ZFC}$ which has the natural numbers structure $\mathbb{N}^M$ as the standard model of arithmetic inside $M$ but $\mathbb{N}^M \ncong \mathbb{N}$ holds outside, where $\mathbb{N}$ means the real standard model of arithmetic in the meta-theory $\mathsf{ZFC} + \operatorname{Con}(\mathsf{ZFC})$. Then, can we take a model […]Pointwise
- Do "truly" infinite proofs exist? December 6, 2024An assumption underlying this earlier question was the existence (and greater expressive strength) of infinite proofs in logics like $\mathcal{L}_{\omega_{1}^{CK}, \omega}$ (based on, for example, the discussion in §2 chap. IX of Mathematical Logic by Ebbinghaus et. al., and answers like this and this) However the comments in response to the question have led me […]NikS
- How do you define universal and existential quantification rigorously and non-circularly? December 5, 2024Universal and existential quantification are necessary to build math from set theory. But I can't think of any way to define them besides the traditional intuition: that is, $(\forall x\in S)[p(x)]$ means "for all $x$ in $S, p(x)$" and $(\exists x\in S)[p(x)]$ means "there is some $x$ in $S$ such that $p(x)$". I know that […]Mathemagician314
- Do quantified statements without domains mean anything? What is one to do when it seems impossible for there to be any domain? [duplicate] December 5, 2024I used to find quantified statements without domains perfectly sensible, but now I can hardly grasp them. Such statements are in introductory texts, proof assistants, and many other places. When a statement concerns numbers, it almost always has a domain, and there is no ambiguity. In many other statements, however, there is less clarity. How […]interested
- Define if the statement: ∀x(A(x) ≡ B(x)) ~ (∀x A(x) ≡ ∀x B(x)) is always true December 5, 2024There is a statement: $$∀x(A(x) \equiv B(x)) \sim (∀x A(x) \equiv ∀x B(x))$$ that seems to be true in all models, but unfortunately I can't think of an idea to proove that, except this, but I am not sure whether it makes sense... $$∀x(A(x) \equiv B(x)) \sim (∀x A(x) \equiv ∀x B(x))$$ is the same […]Artkol
- Demonstrating that an Induction Hypothesis is too weak. December 5, 2024My background is in Computer Science. Proofs by induction are ubiquitous here, especially in programming languages. As a running example, let us take proving things about the natural numbers. To prove that a predicate P holds for all natural numbers (∀n:Nat, P(n)), you prove P(0) (base case) and ∀n:Nat, P(n) => P(n+1) (inductive step). In […]Suraaj K S
- The Hanf number of higher-order logic December 5, 2024The reduction of second-order logic (SOL) to a $\Pi_1^1$-fragment on the Stanford Page of Higher-Order Logic (Section 4) is as follows: From this we get that the Hanf and Löwenheim number of SOL is the same as a $\Pi_1^1$-fragment of SOL (the Hanf number of SOL is also the supremum of $\Sigma_2$-definable ordinals). The intuition […]SJe967
- Unsure about a logic question by Brilliant.org December 5, 2024For context: I wanted to try out brilliant.org for a while after seeing it on numerous sponsored videos by educational YouTubers. I decided to try its level 1 logic course and everything seems to make sense until this question came along. I am posting this because I feel that something is slightly off about this […]Singaporean Hermit
- Reference Request: A general approach to forcing, and some clarification December 4, 2024I've wanted to understand forcing for quite some time now, but I wish to understand it in the general sense of formal logic, rather than just the specific case of set theory, which I find quite confusing anyways. However, I'm struggling to find sources which take this approach, making me doubt it exists. I recall […]Joseph_Kopp
Recent Comments