Questions tagged [provability]
For questions on provability, the capability of being demonstrated or logically proved.
238
questions
5
votes
2
answers
59
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 \...
- 51
-1
votes
1
answer
29
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
votes
0
answers
25
views
Showing the existence of primitive recursive function given a property
So I'm studying computation and there is a section of recursive and primitive recursive functions. I understand the rules of what constitutes a p.r. function (constant functions, closed under bounded ...
1
vote
1
answer
36
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 ...
- 315
0
votes
0
answers
17
views
Applying the axiom of choice on the reals to use transfinite induction
Transfinite induction is the extension of mathematical induction to well-ordered sets, and the axiom of choice, from what I've read (although haven't seen examples or applications of), may be applied ...
- 39
2
votes
1
answer
56
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 \...
- 189
1
vote
0
answers
41
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
22
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(\...
- 46
1
vote
0
answers
36
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
73
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
48
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 ...
- 196
0
votes
3
answers
128
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, ...
- 3,785
1
vote
1
answer
36
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,011
1
vote
2
answers
124
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 ...
- 37.5k
0
votes
1
answer
89
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?
- 309
-1
votes
2
answers
66
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 ...
- 161
3
votes
1
answer
100
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 ...
- 513
0
votes
0
answers
41
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
71
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
211
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?
- 13.2k
3
votes
2
answers
65
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 ...
- 189
1
vote
0
answers
81
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 ...
- 3,766
0
votes
0
answers
42
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 ...
- 157
1
vote
1
answer
59
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
105
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 ...
- 509
0
votes
3
answers
45
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 ...
- 704
1
vote
1
answer
128
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 \}$
- 213
2
votes
2
answers
227
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 ...
- 604
1
vote
0
answers
82
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
43
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 ...
- 186
0
votes
0
answers
45
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
75
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
52
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,354
6
votes
0
answers
130
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 ...
- 864
2
votes
0
answers
68
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 ...
- 61
2
votes
2
answers
67
views
Is there an uncomputable number between any two real numbers?
I know close to nil about uncomputable numbers, so perhaps it doesn't even make sense to ask this question. All the information I can find about them is unaccessible with my level of education, but I ...
- 81
1
vote
1
answer
62
views
Fundamentals of Truth, Provability and Axioms by means of the Continuum Hypothesis
Let S be the structure/language of ZFC (including PL 1). Let CH refer to the well-known continuum hypothesis. My claims are as follows and could u just say if it's true or wrong and why?
In S neither ...
- 342
0
votes
1
answer
56
views
provability and theorem
I am studying first order logic and I have a hard time understanding the link between provable formulas and theorem.
In the book by Shoenfield, the predicate $ Pr_{T}(a,b)$ of is defined as the set of ...
- 35
1
vote
0
answers
401
views
moment generating function an infinite moments
I consider a random variable which has moments $E[X^n]= \infty$.
Does this imply that the moment generating function does not exists?
How could I prove that?
The taylor series of mgf is: $E(e^{tX})= 1+...
- 43
0
votes
1
answer
93
views
A question about undecidable sentences with purely mathematical contents
I'm struggling with the idea that the continuum hypothesis does indeed have a purely mathemathical/set theoretical meaning, but is neither provable nor disprovable in ZFC (according to Gödel and Cohen)...
- 23
3
votes
1
answer
267
views
What does it mean to some logical statement to be provable and decidable?
I am not a mathematician and trying to get deeper insight into modern logic.
It happens all the time, that statements like statement P is unprovable arise, or, more ...
- 1,365
0
votes
2
answers
129
views
How to establish the modus ponens inference rule in the LK sequent calculus for first-order logic? [closed]
How can the modus ponens inference rule
$$
\frac{\Gamma \vdash \varphi\hspace{1cm}\Delta\vdash \varphi\rightarrow\psi}{\Gamma,\Delta \vdash \psi}
$$
be established in the LK sequent calculus for first-...
- 10.5k
1
vote
1
answer
274
views
Finding the logical consequence of a set of formulas $A$
I am trying to solve an exercise that gives me a set $A$ of formulas such that
$A = \{ p, (r → q) → ¬p, (r ∨ p) → q, r\}$
and wants me to compute $Cn(A)$, knowing that in the textbook $Cn$ (...
- 45
5
votes
1
answer
89
views
Judgment-level negation $\nvdash$
I have a basic question about the use of judgment-level negation $\nvdash$. Though I meet it in some of my courses on proof theory, I usually treat it as a metalevel expression and I don't know how to ...
- 612
2
votes
0
answers
58
views
How can I prove that primitive recursion "preserves" representability in Peano Arithmetic?
I'm working on my thesis about Gödel's Incompleteness Theorems, and at some point I need to prove that the $\textsf{PA}$ system is able to represent all the recursive functions.
By recursive function ...
- 23
3
votes
0
answers
52
views
Showing there is an infinity of prime numbers of the form $12k+11$ [duplicate]
I want to prove there is an infinite number of prime of the form $12k+11$. I worked hard to make the first part of my solution but I don't know how to do with the second part.
First : I suppose there ...
- 93
3
votes
5
answers
145
views
If $a^2+b^2-ab=c^2$ for positive $a$, $b$, $c$, then show that $(a-c)(b-c)\leq0$
Let $a$, $b$, $c$ be positive numbers. If $a^2+b^2-ab=c^2$. Show that
$$(a-c)(b-c)\leq0$$
I have managed to get the equation to $(a-b)^2=c^2-ab$, but I haven't been able to make any progress.
Can ...
- 51
10
votes
2
answers
759
views
In what sense is $\sf ZFC$ "stronger" than Peano arithmetic?
I was revisiting the discussion under a previous question of mine, and realized that I don't know how to rigorously formulate the notion of a theory being stronger than another.
If the two theories ...
- 2,751
2
votes
0
answers
46
views
Proof that $\textsf{Prv}(y) \ \& \ y \neq \ulcorner \textbf{0} = \textbf{1} \urcorner$ meets third Hilbert–Bernays provability condition
I have troubles showing the following (it's a slightly abridged version of Exercise 16.1 form Boolos and Jeffrey's Computability and Logic (3rd ed.)}):
$\textsf{Prv}(y)$ is a provability predicate ...
- 302
4
votes
2
answers
339
views
How can you derive a formula without premises? [duplicate]
What is the difference between $\vdash A $ and $\models A$?
I'm not asking about the general difference between syntactic entailment and semantic entailment.
I specifically don't understand the ...
- 808