Questions tagged [provability]
For questions on provability, the capability of being demonstrated or logically proved.
6
votes
3answers
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 ...
1
vote
2answers
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 ...
2
votes
1answer
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 ...
2
votes
1answer
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 ...
0
votes
1answer
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 ...
3
votes
1answer
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: ...
0
votes
1answer
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 ...
3
votes
3answers
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:
...
2
votes
2answers
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$ ...
3
votes
0answers
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 ...
1
vote
1answer
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 ...
2
votes
0answers
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 ...
1
vote
0answers
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/...
1
vote
1answer
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 ...
1
vote
0answers
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 '...
0
votes
1answer
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 ...
0
votes
0answers
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, ...
1
vote
0answers
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, ...
0
votes
0answers
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 ...
1
vote
0answers
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 ...
0
votes
0answers
46 views
$\neg (\neg A) \rightarrow A$ part of the axioms of propositional logic? [duplicate]
When talking with a mathematics teacher the other day, we discussed these axioms in the context of proving tautologies with semantic tableaux:
$(p\to(q\to p))$
$((p\to(q\to r))\to((p\to q)\to(p\to r))...
0
votes
0answers
18 views
how to prove [(a mod n) * (b mod n)] mod n = a * b mod n [duplicate]
How to prove this modular multiplication
[(a mod n) * (b mod n)] mod n = a * b mod n
6
votes
1answer
80 views
Can the negation of an unprovable true statement be added as an axiom?
Let $S$ be some statement which is unprovable but true in an axiomatic system $T$. If $T$ is consistent, then adding $S$ as an axiom of $T$ keeps the system consistent. But what about adding $\neg S$ ...
-2
votes
1answer
29 views
Prove of Greedy Algorithm
Can anyone prove the following?
given n numbers [integer and not necessary distinct] and lets denote the sum of all those number by Sum(n) then we have one of the following facts:
1- Sum(n) is ...
2
votes
1answer
147 views
Higher-order Busy Beaver functions and the language of first-order set theory
I have a question, but before asking this question, it is required to ask the preliminary question: is it possible to define a particular higher-order Busy Beaver function by a formula (of finite ...
28
votes
11answers
5k views
BIG LIST: Statements that look obviously false but cannot be disproved
I'm looking for statements that look obviously false but have no disproof (yet).
For example The base-10 digits of $\pi$ eventually only include 0s and 1s.
To make this question a little objective, ...
1
vote
3answers
138 views
Is there a maximal universe of sets?
In asking a question on this site about the unprovability on the Continuum Hypothesis, many people explained to me that for a given set of axioms, there are many different models that satisfy that set ...
0
votes
0answers
83 views
Why Presburger arithmetic cannot prove pigeonhole principle
The pigeonhole principle is the scheme
$\forall \bar{a},s \{\forall x\!<\!s\!+\!1 \exists y\!<\!s\psi(x,y,\bar{a}) \to \exists x_1,x_2\!<\!s\!+\!1\exists y\!<\!s[x_1\neq x_2 \wedge \psi(...
1
vote
1answer
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 ...
89
votes
11answers
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,...
1
vote
1answer
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 ...
1
vote
1answer
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 ...
3
votes
0answers
165 views
Prove that $\left(\sum_{k=1}^n\,\left(\frac{k}{n}\right)^n\right)^{\frac{1}{n}}$ decreases as $n$ increases.
Please help me to prove the following problem with inductive argument
$$\left(\left(\frac{1}{n+1}\right)^{n+1}+\dots+\left(\frac{n+1}{n+1}\right)^{n+1}\right)^{\frac{1}{n+1}}<\left(\left(\frac{1}{n}...
1
vote
2answers
92 views
Löb's Theorem for proofs of constant size
Löb's Theorem roughly states that for any formal system $T$ with Peano Arithmetic and all formulas $P$
If $T$ proves (if $T$ proves $P$ then $P$) then $T$ proves $P$
What happens if we change the ...
1
vote
2answers
72 views
expression that cannot be “written down” re: incompleteness, logic
I apologize for the poor title.
We are given a computer that writes down only expressions that are true. Let $\omega$ be an expression. Define the composition C of $\omega$ as $\omega(\omega)$. We ...
0
votes
0answers
100 views
What's the difference between fixed point lemma and diagonalization lemma
By knowing Solovay's proof for the arithmetical completeness of provability logic, isn't the celebrated fixed point lemma of provability logic just equivalent to the Gödel's diagonal lemma? Or does ...
0
votes
1answer
27 views
Find $a$ given a function
Given $f(x)=xe^{a \over x}, x>0$, for which it applies $f(x)\ge e^a, \forall x>0
$ (1)
• Show that $a=1.$
Personal work:
Even by getting $e^a$ to the other side of the equation it still,...
1
vote
2answers
29 views
Is there such a function $f(a,b)=k$ where each value of $k$ appears only once for all integer values of $a$ and $b$?
Suppose we have $f(a,b)=k$ such that $k$ is an integer when $a$ and $b$ are integers. Is there such a function where each value of $k$ appears only once for all integer values of $a$ and $b$?
e.g ...
1
vote
6answers
107 views
Inverse Functions and their intersection points
Say you have $f(x) $ and $g(x)$ and $g(x) = f^{-1}(x) $.
I observed that these two curves need not intersect, for example with $f(x) = e^x$ and $g(x) = \ln x $ never intersecting each other.
I also ...
1
vote
2answers
231 views
Example of the property of rational numbers that must be proved using the axioms of real numbers?
According to Godel's incompleteness theorem, some statements about rational numbers are independent from the axioms of the rational numbers given in Wikipedia--an ordered field generated by 1. So can ...
1
vote
1answer
64 views
Is the sign of a real number decidable?
I'm working on the following problem in a class on provability.
Consider how $\mathbb{R}$ might be presented. Is the property of being positive decidable?
How could the reals possibly be presented ...
0
votes
1answer
38 views
How do I prove that the following function is increasing in $t\geq 1$ for any $1\leq y \leq t$?
I am sorry if I am asking something too specific and not useful to the general public, but I am stuck at proving that the following function is increasing for all $t\geq 1$ at any given $y$ such that $...
7
votes
1answer
446 views
Semantics for minimal logic
Minimal logic is a fragment of intuitionistic logic that rejects not only the classical law of excluded middle (as intuitionistic logic does), but also the principle of explosion (ex falso quodlibet). ...
1
vote
1answer
207 views
How to justify: Proof by contradiction ? (First Order Logic)
How to justify this rule?
Proof by contradiction:
If a proof of $\Gamma,\lnot B\vdash C\land\lnot C$ involves no application of Gen using a variable free in $B$, then $\Gamma\vdash B.$
I did one ...
6
votes
1answer
108 views
Being not “close” to ZFC and not “far away” from it at the same time
For each formula $\varphi$ we can have a look at the following two properties:
$$1) ZFC \not \vdash Con (ZFC) \rightarrow Con (ZFC + \varphi)$$
$$2) ZFC + \varphi \not \vdash Con (ZFC)$$
Intuitively, ...
0
votes
1answer
46 views
Deduction from negation of uniqueness quantifier
The problem is this:
By defintion $ \neg(\exists ! y F(x,y))\quad \leftrightarrow \quad \forall y\neg((F(x,y) \wedge \forall z (F(x,z) \rightarrow y=z))) $
I don't see how $\neg F(x,y)\quad \...
0
votes
3answers
70 views
Provability vs. implication?
For any logic we have an is provable from relation denoted by $S \vdash \phi$ where $S$ is a (for the sake of the argument lets say) finite set of sentences and $\...
2
votes
2answers
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$-...
8
votes
2answers
190 views
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....
5
votes
1answer
63 views
Equivalence of different consistency sentences
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 $...
