Questions tagged [provability]

For questions on provability, the capability of being demonstrated or logically proved.

Filter by
Sorted by
Tagged with
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 \...
user avatar
-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 ...
user avatar
-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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 \...
user avatar
  • 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 ...
user avatar
  • 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(\...
user avatar
  • 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?
user avatar
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&...
user avatar
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 ...
user avatar
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, ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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?
user avatar
-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 ...
user avatar
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 ...
user avatar
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.
user avatar
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 ...
user avatar
  • 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?
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 \}$
user avatar
  • 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 ...
user avatar
  • 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:...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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. ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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+...
user avatar
  • 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)...
user avatar
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 ...
user avatar
  • 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-...
user avatar
  • 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$ (...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar

1
2 3 4 5