Questions tagged [provability]

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

151 questions
262 views

Where is my Collatz conjecture proof wrong?

I am amateur and don't have very good understanding of mathematical proving. My proof is so simple i don't believe noone thought of this before. But I am so blinded by the hope it is correct, that I ...
42 views

Variation on Lob's Theorem

Lob's theorem is, of course, if $P(y)$ is a provability predicate for $S$, $S$ diagonalisable, then if $(P(A) \rightarrow A)$ is provable in $S$ then $A$ is provable in $S$. I understand the proof of ...
50 views

When is $X \rightarrow P(X)$ provable?

My question is: within a system $S$ where $S$ is any extension of $Q$ (Robinson's Arithmetic), and when $P(y)$ is a provability predicate for $S$, when is $(X \rightarrow P(X))$ provable? By ...
65 views

How to deduce $\square p\to p$ from other modal axioms?

I'm trying to deduce the T axiom $\square p\to p$ from the B,D,5 (and also K) axioms. B: $q\to\square\diamond q$ D: $\square q\to\diamond q$ 5: $\diamond q\to \square \diamond q$ I tried to assume ...
50 views

Proving that a sentence is inconsistent [duplicate]

I'm trying to understand if the sentence $\square\bot\land \phi$ is consistent in KD. I don't think it is true because it looks like no serial model where this sentence is satisfiable exists. As I ...
90 views

What does it mean for a number to be independent of ZFC?

Since the definition of the Busy Beaver function by Radó in 1962, an interesting open question has been what [is] the smallest value of $n$ for which $BB(n)$ is independent of ZFC set theory. Source: ...
32 views

Maximum cycle length of tiles in rubik cube

I tried to write a program to count the number of repeated sequence(s) to make NxNxN (for N=2 to 20) rubik cube back to it's initial state/placement. I solved it by counting the length of cycle of ...
85 views

Formal proof of one of De Morgan's laws

How to give a formal proof of $\vdash \neg (p\land q)\to\neg p\lor \neg q$ in the natural deduction proof system? Here is what I have: ...
52 views

Is this proof in natural deduction proof system correct?

Consider a natural deduction proof system. Suppose I know that $\vdash \phi$ (the sentence $\phi$ is provable from no premises). If I'm proving something like $\vdash \psi$, can I just use that $\phi$ ...
79 views

Godel's theorem incompleteness, truth vs.provability

I know this question has been investigated in other threads, but I would like to pose yet another question on Gödel's theorem incompleteness, and truth in 'the standard model' compared with ...
90 views

Partition of positive reals with each part closed under addition without choice

It is an easy exercise using transfinite recursion to prove the following (in ZFC): There exists sets $S,T$ that partition $\mathbb{R}_{>0}$ such that each of $S$ and $T$ is closed under ...
118 views

n-consistency - provability/truth of $\Sigma^0_n$ and $\Pi^0_{n+1}$ -formulas; n-consistent extensions, etc.

I am facing difficulties with the following exercise. (It is 1.5.9. from 'proof theory and logical complexity', Girard, '87) (i) T is $\textbf{n-consistent} \ (n>0)$ if any $\Sigma^0_n$ - theorem ...
62 views

Are the HBL derivability conditions necessary for Gödel's incompleteness theorems? (For Löb's theorem?)

I am currently working with 'proof theory and logical complexity', a monograph on proof theory. In the exercises of the first chapter one was asked to prove Löb's theorem (https://en.wikipedia.org/...
124 views

An alternative formulation (or corollary) of Tarski's theorem? [Or just a typo?]

In my proof theory monograph (proof theory and logical complexity, Girard from '87) there is an exercise 1.5.4. on page 78 called 'Tarski's theorem'. It says: "Show that there is no truth predicate ...
111 views

Why the 'natural' consistency proof of PA cannot be carried out $\textbf{in}$ PA

In my proof theory monograph there is this exercise: "The natural proof of PA cannot be carried out in PA. Why? (This proof consists in showing that all theorems of PA are ture.)" Apparently, by '...
63 views

On independency of ZFC of statements in math problem solving

To be honest, this is a question that has been bothering me (provided that I understand this correctly), which probably means I'm not quite sure about what I ask, but I'm looking for some ...
55 views

Questions in proof theory (PRA-provability of EA-theorems, Girards book from '87)

I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there. I would be glad if someone can help me with some of the exercises, ...
66 views

Questions in proof theory (PRA-provability of an EA-axiom, Girards Book from '87)

I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there. I would be glad if someone can help me with some of the exercises, ...
55 views

Is it possible to prove the following inequalities to be true?

I'm trying to prove the following inequalities are true, but they're a little too complex, is it even possible to prove that they are true? I suspect they are, but unless there is some simple method ...
55 views

Godelian problems with logic puzzles

It occurs to me that the sort of reasoning common in many logic puzzles (e.g. https://en.wikipedia.org/wiki/Hat_puzzle or https://xkcd.com/blue_eyes.html), the persons involved all trust one another ...
46 views

60 views

If $f:\mathbb R\to\mathbb R$ is a polynomial of odd degree, then for every real $y$ there is a real $x$ such that $f(x)=y$

Prove that if the function $f: \mathbb R \to \mathbb R$ is an odd degree polynomial, for every number $y ∈ \mathbb R$ there exists such a number $x ∈ \mathbb R$ that $f(x) = y$. Prove that this is ...
13k views

Is there any conjecture that has been proved to be solvable/provable but whose direct solution/proof is not yet known?

In mathematics, is there any conjecture about the existence of an object that was proven to exist but that has not been explicitly constructed to this day? Here object could be any mathematical object,...
36 views

Would a proof predicate change if a stronger system used despite sharing language?

This is a follow-up question from Proof predicate in PA and stronger system Suppose that two theories $T_1$ and $T_2$ share the same language - thus only axioms differ such that $T_2$ is a stronger ...
94 views

Proof predicate in PA and stronger system

It is said that proof predicate of PA is primitive recursive, but I cannot find explicit form of the proof predicate, or how it is defined. What is this proof predicate? What about defining for other ...
165 views

46 views

171 views

Computable extension to $Σ_1$-sound system that is $Σ_2$-unsound?

Recently, I wrote this post showing (if I did not make a mistake) essentially that: For any nice formal system $S$ that is $Σ_1$-sound there exists some extension $S'$ that is $Σ_1$-sound but $Σ_2$-...
Brutal gaussian integral of death $\int_{\mathbb{R}} x \Phi(x) \phi(Bx-b)$
Ciao, I was making some computation and I've been stucked in this one. Let $B$ and $b$ be positive contant. We call $\phi(x)$ standard gaussian distribution and $\Phi(x)$ its cumulative function, i....
Take any formal system $S$ that has a proof verifier program and interprets TC or PA$^-$. $\def\imp{\Rightarrow} \def\con{\text{Con}}$ Then the incompleteness theorems show that $S$ does not prove \$...