Skip to main content

Questions tagged [provability]

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

Filter by
Sorted by
Tagged with
0 votes
1 answer
133 views

Interpretation of Godel's incompleteness theorem [closed]

Godel's incompleteness theorem states "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e. there are statements of the ...
MathTrain's user avatar
  • 2,280
0 votes
0 answers
42 views

Induction on two variables, confused about the induction step

Suppose I want to show For any $n>1$, any $r$, such that whenever $r+1 \leq n$, we have $P(n,r)$. (Geometrically, we have a 'infinite' triangle in the plane) My induction goes as $\forall n >1$ (...
Andrew_Ren's user avatar
3 votes
1 answer
139 views

Is Gödels second incompleteness theorem provable within peano arithmetic?

All following notation and assumptions follow Gödel's Theorems and Zermelo's Axioms by Halbeisen and Krapf. Exercise 11.4 c) states "Conclude that the Second Incompleteness Theorem is provable ...
Lassadar's user avatar
  • 171
3 votes
1 answer
97 views

Are there examples of statements not provable in PA that do not require fast growing (not prf) functions?

Goodstein's theorem is an example of a statement that is not provable in PA. The Goodstein function, $\mathcal {G}:\mathbb {N} \to \mathbb {N}$, defined such that $\mathcal {G}(n)$ is the length of ...
Burnsba's user avatar
  • 1,027
0 votes
0 answers
65 views

Does any computable $T\supset PA^-$ have a provability predicate satisfying Hilbert-Berneys conditions?

In the language of arithmetic, fix a computable theory $T\supset PA^-$. Let $P_T(x)$ be the usual $\Sigma_1$ formula: for any sentence $\varphi$, $\mathbb{N}\models P_T(\ulcorner\varphi\urcorner)$ iff ...
mathlearner98's user avatar
3 votes
1 answer
221 views

Consistent theories $T$ such that $T+\mathrm{Con}(T+\mathrm{Con}(T))$ is inconsistent

In this question, it is asked whether there is a theory $T$ such that $T$ is consistent but $T+\mathrm{Con}(T)$ is inconsistent. The answer is yes: for instance, $T=\mathsf{PA}+\neg\mathrm{Con}(\...
Joe's user avatar
  • 20.7k
0 votes
1 answer
66 views

Proving the existence of an element $x$ in a set $X$ so that $\text{F}(X) \geq \text{f}(x)$ becomes an equality given some rules for f and F

Let $X$ be an arbitrary set. I've defined some functions and rules as follows: $\text{F}()$ is a function from $\mathcal{P}(X)$ to $\mathbf{Ord}$. $\text{f}()$ is a function from $X$ to $\mathbf{Ord}...
Nikita M. Grimm's user avatar
0 votes
1 answer
103 views

Is $(\phi\implies\psi) \iff ((\phi\land\psi)\lor \neg\phi) $ provable in the following hilbert calculus without contraposition or reductio?

Is $(\phi\implies \psi) \iff ((\phi\land \psi)\lor \neg \phi) $ in the following hilbert calculus without contraposition or reductio ad absurdum? If so, how would I go about proving it, and if not, ...
The Sea's user avatar
1 vote
3 answers
124 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 ...
schuelermine's user avatar
0 votes
0 answers
25 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 ...
Toboxos's user avatar
  • 19
-2 votes
1 answer
113 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*} $$
gelerum's user avatar
  • 11
1 vote
2 answers
112 views

Is someone trying to solve problems by building all possible proofs using all possible rules of inference? [closed]

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 ...
ThePhilosopher's user avatar
5 votes
1 answer
214 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 ...
suhdonghwi's user avatar
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 ...
Shimon S's user avatar
  • 143
1 vote
0 answers
59 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 $...
A. G's user avatar
  • 338
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: ...
Jonas Broe Bendtsen's user avatar
1 vote
1 answer
104 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}$$ $$\...
Daniel Wright's user avatar
0 votes
1 answer
37 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-...
bomo's user avatar
  • 103
0 votes
1 answer
125 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)...
Hank Igoe's user avatar
  • 1,416
3 votes
2 answers
103 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 ...
donaastor's user avatar
  • 1,697
1 vote
0 answers
52 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. ...
Cyklotophop's user avatar
1 vote
1 answer
72 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 ...
Sergei Akbarov's user avatar
-1 votes
1 answer
223 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 ...
user110391's user avatar
  • 1,129
-2 votes
1 answer
103 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(...
PW_246's user avatar
  • 1,338
5 votes
3 answers
134 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 \...
Mathplendid's user avatar
0 votes
1 answer
62 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 ...
Mohammad tahmasbi zade's user avatar
1 vote
1 answer
118 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 ...
Margaret's user avatar
  • 1,769
2 votes
1 answer
75 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 \...
boyler's user avatar
  • 375
1 vote
0 answers
49 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 ...
Shanks's user avatar
  • 23
1 vote
0 answers
53 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(\...
sobach'e_pole's user avatar
1 vote
0 answers
55 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?
Thuc Hoang's user avatar
1 vote
0 answers
90 views

What inference rules do people refer to when they talk about "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&...
niilogunay's user avatar
0 votes
1 answer
101 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 ...
Jeff Hykin's user avatar
1 vote
3 answers
403 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, ...
subrosar's user avatar
  • 4,784
2 votes
1 answer
62 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 ...
Maximal Ideal's user avatar
1 vote
2 answers
207 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 ...
Franklin Pezzuti Dyer's user avatar
0 votes
1 answer
352 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?
QuantumLogarithm's user avatar
-1 votes
2 answers
72 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 ...
Andrew Ren's user avatar
3 votes
0 answers
123 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 ...
Hauke Reddmann's user avatar
0 votes
0 answers
83 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.
Rando McRandom's user avatar
0 votes
2 answers
188 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 ...
Julie's user avatar
  • 67
0 votes
3 answers
278 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?
Dan Christensen's user avatar
3 votes
2 answers
87 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 ...
boyler's user avatar
  • 375
1 vote
0 answers
83 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 ...
Graviton's user avatar
  • 4,472
0 votes
0 answers
75 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 ...
ArithEgo's user avatar
  • 161
1 vote
1 answer
123 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 ...
Ben's user avatar
  • 93
1 vote
2 answers
268 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 ...
mathlearner98's user avatar
0 votes
3 answers
66 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 ...
georgy_dunaev's user avatar
3 votes
1 answer
243 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 \}$
Sapiens's user avatar
  • 253
4 votes
2 answers
938 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 ...
Loic's user avatar
  • 781

1
2 3 4 5 6