Questions tagged [provability]
For questions on provability, the capability of being demonstrated or logically proved.
253
questions
1
vote
3
answers
99
views
Does a Turing machine exist with output 1 if an unprovable statement is true and 0 otherwise?
Suppose there is some statement $X$ that is unprovable in some system, e.g. ZFC. Let $L = \{x : x \in \Sigma^* \land X \text{ is true}\}$. Is there a Turing machine that decides $L$? I have had an ...
- 527
0
votes
0
answers
23
views
Proving minimum steps solution for a math quiz [duplicate]
I have the following math quiz:
You have 4 Red Balls & 4 Green Balls. You cannot see the color of the balls but you have a machine (or function) which takes 2 balls as input and returns true, when ...
- 19
-2
votes
1
answer
105
views
Prove $\sqrt{-3+44a} \in N$ can't be a square root of a square of a natural number [closed]
Prove $\sqrt{-3+44a} \in N$ can't be a square root of a square of a natural number.
$$
\begin{equation*}
\begin{cases}
a \in N
\\
d \in N
\\
-3+44a = d^2
\end{cases}
\end{equation*}
$$
- 11
1
vote
0
answers
67
views
Is someone trying to solve problems by building all possible proofs using all possible rules of inference?
We obviously can construct a program that, starting with ZFC (or any other theory) axioms, would use all possible rules of inference to get all possible proofs constructible in ZFC. (There would be ...
5
votes
1
answer
143
views
Is there a proposition that cannot be proven to be provable(or not)? [duplicate]
I have been studying mathematical logic and the foundations of formal systems, and I came across the concept of "provability" and "unprovability" of propositions within such ...
- 151
0
votes
0
answers
39
views
Estimating Set Size from Sample Data
I encountered a sampling problem and managed to approximate programmatically. However, I'm interested in determining the analytical solution.
There are two sets $A$ and $B$. $|A|$ is known, $|B|$ is ...
- 143
1
vote
0
answers
57
views
Reflection principle for finite subsystems of PA.
I would like to clarify the reasoning behind the proof of reflection schema for finite subsystems of PA that I found in "The Blind Spot" book.
To be wore precise, we have a finite subsystem $...
- 328
0
votes
0
answers
19
views
Arrangement of element such that no two share the same position nor the same order [duplicate]
My friend asked me an interesting question yesterday:
Say you have six names, which you have to sort in six groups. The order of the names must always be different between the groups, such that:
...
0
votes
0
answers
48
views
Set of consequences of $\Gamma$.
Let $\text{Con}(\Gamma):=\{\varphi:\Gamma\vdash\varphi\}$. Prove that $\text{Con}(\text{Con}(\Gamma))=\text{Con}(\Gamma)$.
I think I have the first inclusion. Let $\varphi\in\text{Con}(\text{Con}(\...
- 503
1
vote
1
answer
93
views
Prove that every Isosceles triangle with two equal sides third side is equal to $c = \pm(a+b)$
Let $\triangle ABC$ be an isosceles triangle with two equal sides that $AB = AC$ than $\angle AB = \angle AC$ so with law of cosines we can calculate:
$$\cos\theta_{1} = \frac{b^2+c^2-a^2}{2bc}$$
$$\...
- 103
0
votes
1
answer
31
views
Is $V$ a subspace of $M_{2,2}$?
Consider the subset
$$
V = \{A \in M_{2,2} | v^TA = (Av)^T\}
$$
of vector space $M_{2,2}$ fo 2x2 matrices. $v^T$ inidcates the transpose of v. Is V a subspace of $M_{2,2}$?
Assuming the set is non-...
- 3
0
votes
1
answer
98
views
Lob's theorem paradox resolution
The following puzzle is given in A Cartoon Guide to Lob's Theorem:
The Deduction Theorem states that whenever assuming a hypothesis H enables us to prove a formula F in classical logic, then (H->F)...
- 1,410
3
votes
2
answers
94
views
If in some theory it is impossible to prove $X$, is it impossible to disprove $X$ too?
In mathematical logic, if we can prove that it is impossible to prove a statement $X$ with some theory $T$, do we necessarily have a proof that it is impossible to disprove the statement $X$ in theory ...
- 1,667
1
vote
0
answers
42
views
What excatly are the "worlds" in provability logic?
What is the interpretation of the set $W$ in a Kripke model $\mathcal{K}=\langle W,R,\phi\rangle$ of provability logic, where the $\Box$-operator stands for provability in a given arithmetic theory. ...
- 11
1
vote
1
answer
70
views
Invertibility of the first Hilbert-Bernays condition in $\omega$-consistent theories
I am reading the Wikipedia article about the Hilbert–Bernays provability conditions and I don't understand the following place there:
The condition that $T$ is $\omega$-consistent is generalized by ...
- 2,415
-1
votes
1
answer
178
views
What are proofs in constructivist logic?
The difference in syntax between classical and constructivist mathematics is, as far as I've understood, not because constructivists think a well-formed proposition may be untrue and unfalse at the ...
- 1,057
-2
votes
1
answer
92
views
Difficulty understanding the Diagonalization Lemma
The diagonal lemma states that:
∀Φ∃Ψ (Ψ<—>Φ(⌜Ψ⌝))
A classic use of this lemma/theorem is to prove Löb’s theorem in provability logic. In that case, the theorem is instantiated to Q<—>(Prv(...
- 993
5
votes
3
answers
126
views
If $S5 \vdash \alpha$ then $S4 \vdash \diamond \alpha$
I would like to prove that if S5 proves $\alpha$ then S4 proves $\diamond \alpha$. Here S4 is K plus axioms for reflexivity ($\square \alpha \to \alpha$) and transitivity ($\square \alpha \to \square \...
- 91
0
votes
1
answer
56
views
Does Z₂ Prove the iteration theorem?
iteration theorem:
Let (ℕ,0,S) be the structure of natural numbers. And let W be an arbitrary set and c be an arbitrary member of W and g be a function from W into W. Then, there is a unique function ...
1
vote
1
answer
100
views
Provability of sequents in LK
In his answer to my question Andreas Blass writes: "$A\lor(B\land C)$ doesn't classically imply $(A\lor B)\land C$". I read this as: The sequent $A\lor(B\land C) \vdash (A\lor B)\land C$ is ...
- 1,585
2
votes
1
answer
70
views
How to prove $\forall x\; (\phi (x)\land \psi (x) ) \rightarrow \forall x\; \psi (x)$ without using the completeness theorem?
The statement $\forall x\; (\phi (x)\land \psi (x) ) \rightarrow \forall x\; \psi (x)$ is valid, that is it is true in any structure. Hence, for any $\sum \subseteq Form_{\mathcal{L}}\; \sum \models \...
- 259
1
vote
0
answers
44
views
Is it True: The average distance of points from the diagonals is less than the average distance from circumference of the circle in a rectangular area
My problem is related to proving that the average distance of random distributed points from the diagonals is less than the average distance from the circumference of the circle.
The problem is ...
- 23
1
vote
0
answers
40
views
Formulas that can be proved from the uniform reflection schema
Let $T$ be a sound, r.e. theory containing elementary arithmetic. By the uniform reflection schema of $T$ ($\mathrm{RFN}(T)$) I mean the schema that expresses the soundness of $T$:
$\forall x(\...
- 138
1
vote
0
answers
51
views
Defining a rule of inference using infinitely many premises
I tried to look up for a rule of inference using infinitely many premises but couldn’t find one. Why there is no such a rule? Will such a rule make any sense?
- 71
2
votes
0
answers
81
views
What are the inference rules of Peano Arithmetic? [duplicate]
There are many examples in the literature (for example, in this question)
where the author says that something "is provable in Peano arithmetic" or "is not provable in Peano arithmetic&...
- 21
0
votes
1
answer
83
views
Demonstration of proving a statement is unprovable
Similar questions have been asked, but this is not a duplicate.
I'm looking for a proof itself, not a description of methods.
Related:
How do we prove that something is unprovable?
is possible to ...
- 226
0
votes
3
answers
320
views
Does this proof of Godel's incompleteness theorem rely on soundness?
The proof of Godel's first incompleteness theorem is often paraphrased like this. First, find a sentence $\phi$ which is true exactly if it is not provable. If $\phi$ is false, it must be provable, ...
- 4,564
2
votes
1
answer
53
views
Are there bounds given for the strengthened Ramsey theorem?
The Paris-Harrington theorem says that a variant of the finite Ramsey theorem is not provable in Peano arithmetic, but it is provable in stronger systems.
The proof of the strengthened finite Ramsey ...
- 2,427
1
vote
2
answers
193
views
Type Theory: we cannot prove double negation, but can we prove it is unprovable?
I'm currently trying to learn type theory from the first chapter of HoTT. It is remarked that we cannot prove $\neg\neg A \rightarrow A$, when $A$ is interpreted as a proposition, or, equivalently, we ...
- 39.4k
0
votes
1
answer
259
views
Number of k-tuples of non-negative integers whose sum equals a given integer
Does the sum over the non-negative integers,
$$
\sum\limits_{ {i_1, \ldots i_k \geq 0:\\\ i_1+\ldots i_k=L }} 1
$$
have a closed expression, where $L$ and $k$ are some integers?
- 172
-1
votes
2
answers
71
views
Questions about logic and proof systems
I encountered two similar expressions when prooving two sets A and B are equivalent.
For $A \subseteq B$, we have two ways to prove?
$\forall x \in A$, then $x \in B$
$\forall(x \in A \longrightarrow ...
- 171
3
votes
0
answers
121
views
Ultra-finite math [closed]
Assume our universe is finite in any sense (the information amount was some $10^{120}$ bits, if I remember correct) and deal with the following, slightly (and intendedly) preposterous, scenario:
The ...
- 705
0
votes
0
answers
72
views
How can I encode a proof in PA as a godel number?
It seems straightforward to encode a wff in PA as a number. I can't see how to encode a proof. Could someone please tell me how this is usally done? Thanks.
0
votes
2
answers
165
views
Prove or disprove: if Γ ⊢ α and Γ ⊆ ∆ then ∆ ⊢ α
I am trying to solve this question but I am doubting about the answer. Namely:
Γ ⊢ α means that there is a derivation with conclusion α and with all hypothesis in Γ. Since Γ ⊆ ∆, we can use the same ...
- 57
0
votes
3
answers
253
views
What is the truth value if any for $f(x)=y$ when $x$ is outside of the domain of $f$?
What is the truth value if any for $f(x)=y$ when $x$ is outside of the domain of $f$? Could it be false or undefined?
- 14.3k
3
votes
2
answers
79
views
Can we have another set of inference rule which is simplier and equivalent (in the sense that they prove the same formulas)?
I have some questions on inference rules in model theory.
Question 1) In (some books of) model theory, $(\psi \rightarrow \phi, \psi \rightarrow \forall x \phi)$ where $x$ is not free in $\psi$ is ...
- 259
1
vote
0
answers
82
views
Is the set of all provable theorems countable? [duplicate]
I suppose this is not an easy question unless we formally define what counts as a theorem. For the purpose of this question, let us conservatively suppose that we are taking ZFC as our foundation, and ...
- 4,448
0
votes
0
answers
64
views
For every $n \in \mathbb {N} $, assume $p_{n}$ is the $n^{th}$ prime number. if $n \gt 1$, prove that $p_{n}\lt 2^{n}$. [duplicate]
I tried to solve this problem using mathematical induction. First, we say that $ 3 \lt 4$ for $n =2$, which is correct.
Then by assuming that it's accurate for $k$, we need to prove it's accurate as ...
- 161
1
vote
1
answer
102
views
Independent events in Probability theory
Events A, B and C are independent, $\mathbb P (A) = 0.1$; $\mathbb P (B) = 0.4$ and $\mathbb P (C) = 0.9.$
Find the probability of an event $D = (A + B) (A + C) (B + C).$
Find the probability of ...
- 93
1
vote
2
answers
196
views
Are provable statements true?
I recently started reading an introductory logic textbook, and I haven't got yet to the chapter that talks about completeness theorem, but I just couldn't wait to read about it using shortcuts. I just ...
- 762
0
votes
3
answers
62
views
Is it possible to obtain a contradiction from provability logic GL + inference rule ($\square P$ ==> $P$)
Is it possible to obtain a contradiction from provability logic GL + inference rule ($\square P$ ==> $P$) ?
I suspect that answer is "No".
If I am right, then there is a model of such ...
- 790
3
votes
1
answer
175
views
Does $\mathbf{Z}$ prove existence of transitive closure of every set?
Is Zermelo set theory sufficient to prove the existence of the transitive closure of any set $X$?
$TC(X)=\{X, \bigcup X, \bigcup\bigcup X, \ldots \}$
- 233
3
votes
2
answers
688
views
Incompleteness theorem: Peano arithmetic vs. standard model of arithmetic
Context (from
https://en.wikipedia.org/wiki/Non-standard_model_of_arithmetic#From_the_incompleteness_theorems):
The incompleteness theorems show that a particular sentence G, the
Gödel sentence of ...
- 726
1
vote
0
answers
94
views
Characterization for unprovable formulas for first-order logic
Is there any existing work on characterizations of the unprovable formulas in (general) first-order logic? i.e. Gödel's incompletness result constructs an explicit formula that is valid but unprovable:...
user375735
0
votes
0
answers
49
views
If a statement implies an undecidable statement, does that make it undecidable itself?
Wikipedia writes that in every consistent formal system that satisfies Gödel's first incompleteness theorem there exist statements about natural numbers that are true, but that are unprovable within ...
- 260
0
votes
0
answers
48
views
Can PA prove Cons(PA) under standard model?
We know that PA cannot prove Cons(PA) without being inconsistent. But can PA prove Cons(PA') where PA' is a restricted PA that allows only the standard model (for example by defining PA' to be the ...
- 11
0
votes
1
answer
131
views
Is there a chess example of True but Not Provable statement?
I am trying to explain to someone (and also to understand better) Godel's Theorems through a chess example.
Indeed I found some examples of True but Not Provable math statements, but they are honestly ...
1
vote
1
answer
91
views
Computability and Logic by Boolos et all Problem 17.1
Show that the existence of a semirecursive set that is not recursive implies that any consistent, axiomatizable extension of $\mathbf{Q}$ fails to prove some correct $\forall$-rudimentary sentence.
...
- 2,639
6
votes
0
answers
136
views
"Barely-unprovable" functions
Fix a $\Sigma_1$-sound theory $\mathcal{T}$ containing basic (Robinson) arithmetic.
On the one hand, by diagonalizing over the provably total computable functions in $\mathcal{T}$, we can construct a ...
- 894
2
votes
0
answers
76
views
Is there a conjecture or result such that if it's proven to be true would automatically prove (the Strong) Goldbach's conjecture? [duplicate]
I'm just wondering if there's any existing conjectures or results such that if they're proven to be true, Goldbach's conjecture would also be proven to be true.
Additional Information:
I've looked at ...
- 93