Questions tagged [proof-theory]

For question in Proof Theory, where "proofs" themselves are the object of mathematical investigation. It is not to be used to request a proof of some result.

Filter by
Sorted by
Tagged with
11 votes
1 answer
592 views

Cut-free proofs in ZFC

If a statement $P$ has a ZFC proof of length $n$, must it also have a cut-free ZFC proof of length polynomial in $n$? By a cut-free ZFC proof, I mean a proof in sequent calculus without cut rule of ...
Dmytro Taranovsky's user avatar
7 votes
3 answers
907 views

Notable examples of syntactic proofs whose existence is guaranteed by completeness, but having been found later than a semantic proof?

Question. What are examples (preferably documented and explicitly commented on from this perspective in the literature, preferably in an article dedicated to this aspect alone) of the following well-...
12 votes
5 answers
718 views

Asymmetric $A \iff B$ proofs

When proving that conditions $A$ and $B$ are equivalent, it is often an arbitrary choice whether to first prove $A\implies B$ or $B\implies A$. Are there examples where the second implication uses the ...
Aryeh Kontorovich's user avatar
7 votes
1 answer
329 views

Axiomatizations of arithmetical parts of theories

For common theories that talk about something more general than first-order arithmetic (e.g. set theories and subsystems of second-order arithmetic), are there nice axiomatizations of their arithmetic ...
Alex Mennen's user avatar
  • 2,090
5 votes
4 answers
692 views

Mathematical induction vis-a-vis primes

One of the most used proof-techniques is mathematical induction, and one of the oldest subjects is the study of prime numbers. Thanks to Euclid, we can consider the primes as a infinite monotone ...
7 votes
1 answer
251 views

Weird analogy between quadratic forms and formal systems

A fundamental connection between provability and consistency for formal systems is that, if $Q$ is a formal system and $A$ is a sentence in the language of $S$, then $Q$ proves $A$ if and only if $...
PseudoNeo's user avatar
  • 477
4 votes
0 answers
283 views

the strength of saying "each sentence of true arithmetic has a recursive proof"

Let $PA_{\omega}$ be just like $PA$ except that $PA_{\omega}$-proofs can use any number of applications of the recursive $\omega$-rule. The recursive $\omega$-rule allows the following: For each ...
Haidar's user avatar
  • 449
1 vote
0 answers
175 views

Is there a Carnap-Gödel style account of the undecidability of the Halting Problem?

The proof of Gödel's incompleteness theorem can be streamlined by means of the Carnap-Gödel diagonal lemma and the ensuing fixed point theorem $\vdash_S G\leftrightarrow\lnot\Pi\ulcorner G\urcorner$ ...
Frode Alfson Bjørdal's user avatar
4 votes
1 answer
421 views

$f_{\epsilon_0}$ and provably total functions in $PA$

A total recursive function $f(x)$ is provably total in $PA$ if there's some formula $\phi(x,y)$ such that $f(x)=y \iff PA\vdash \phi(x,y)$ and $PA\vdash \forall x \exists y \phi(x,y)$ I know (not in ...
Eric's user avatar
  • 2,601
2 votes
0 answers
191 views

$P=NP$ and provability of family of propositional formulas

Let $\mathcal{L}'=\{+,\cdot,0,S,=,<,||,\#,R\}$ be the lanugage of bounded arithmetic with a $k$-ary relation $R$. For every bounded sentence $\phi({\bf\bar{n}})$ in $\mathcal{L}'$ define ...
Erfan Khaniki's user avatar
15 votes
1 answer
357 views

How much can "(recursively) large ordinal axioms" prove?

In "Collapsing functions based on recursively large ordinals: A well–ordering proof for KPM", Michael Rathjen shows that certain notations for the proof-theoretic ordinals of theories, which ...
Robin Saunders's user avatar
5 votes
1 answer
360 views

The difference between KP+Inf+Pow and Z

I'd like to clarify some details about the theories Z (= Zermelo set theory) and KP+=KP+Infinity+Powerset (KP is Kripke-Platek set theory). In this paper (M1), Mathias claims that Z+KP is consistent ...
Noah Schweber's user avatar
3 votes
0 answers
538 views

When must one strengthen one's induction hypothesis?

My questions are about the phenomenon that in order to prove a fact $\forall x \phi(x)$ by induction, sometimes straightforward induction "does not work" and instead one "must" use a "stronger" ...
Anders Lundstedt's user avatar
17 votes
2 answers
1k views

Who first proved that we can prove that we prove things we prove?

Sorry about the title, I couldn't resist. It's a classic fact that, not only does $PA$ prove every true $\Sigma_1$ sentence, but $PA$ proves that $PA$ proves every true $\Sigma_1$ sentence! In ...
Noah Schweber's user avatar
9 votes
3 answers
572 views

Admissibility of Harrop's rule, computationally

It is obvious that the following formula is not a theorem of intuitionistic propositional calculus (IPC). $$ (\neg A \; \to \; B \vee C) \;\; \to \;\; ((\neg A \; \to \; B) \vee (\neg A \; \to \; ...
Bob's user avatar
  • 476
7 votes
1 answer
387 views

Pure first order logic formulations of Markov's principle

Markov's principle is a statement of constructive arithmetic that allows classical reasoning on formulas of the shape $\exists x P$ when $P$ is a recursive predicate: $\neg \neg \exists x P \to \...
Matteo's user avatar
  • 71
10 votes
2 answers
2k views

What exactly is a judgement?

Before formulating my question, let me briefly sum up what I know about the topic (feel free to correct me if something I claimed is false!). This is for you good to see what my state of knowledge is, ...
user avatar
9 votes
3 answers
701 views

What is the definition of computational content?

I am interested in type theory and proof theory. I have read a lot of papers and books that use the term "computational content" (For example: https://scholar.google.com/scholar?hl=en&q=%...
user2377's user avatar
  • 439
3 votes
0 answers
62 views

Equational theory for resolution proof system

Is there any equational theory $T$ like $PV$ with following properties: If $T\vdash f=g$ for terms $f$ and $g$, translation of $f=g$ to propositional formulas has polynomial resolution proof.(like $...
Erfan Khaniki's user avatar
1 vote
0 answers
140 views

eliminating contraction

I'd like to better understand the role of the contraction rule in Gentzen's $\mathsf{LK}$. I would like to have an example of a derivable sequent that is no longer derivable if the contraction rule is ...
Andre Kornell's user avatar
8 votes
4 answers
3k views

The Halting Problem and Church's Thesis

In the opening chapters of Hartley Rogers, Jr.'s book Theory of Recursive Functions and Effective Computability, the proofs of the unsolvability of the halting problem and related unsolvability ...
Frode Alfson Bjørdal's user avatar
5 votes
0 answers
101 views

Medium Growing Hierarchy

I want to bound some functions using the fast-growing hierarchy, but for accounting reasons it looks like it's going to be easier to deal with a modified hierarchy that grows at "$1/\omega$-th" the ...
Henry Towsner's user avatar
8 votes
1 answer
719 views

Why relative consistency results by forcing arguments are provable in finitistic metatheory

It is claimed in many textbooks that relative consistency results, such as $\text{Con}(\text{ZFC})\rightarrow\text{Con}(\text{ZFC}+2^{\aleph_0}\geq\aleph_2)$, are provable in the finitistic metatheory....
Ruizhi Yang's user avatar
40 votes
4 answers
7k views

Did Euler prove theorems by example?

In his 2014 book, Giovanni Ferraro writes at beginning of chapter 1, section 1 on page 7: Capitolo I Esempi e metodi dimostrativi Introduzione In The Calculus as Algebraic Analysis, Craig Fraser, ...
12 votes
4 answers
876 views

Let's keep adding once undecidable statements

This present thread is inpired by the previous thread the true reason of the incompleteness of formal systems. I have the following intuitive idea: Gödel's second incompleteness theorem states that a ...
asdfusername's user avatar
1 vote
1 answer
182 views

What is difference between length of proof and length of its presentation in Peano Arithmetic?

In this paper http://www.sciencedirect.com/science/article/pii/0304397584901117 page $19$ or $29$ it seems to imply there is a difference between length of proof and length of its presentation in ...
Turbo's user avatar
  • 13.7k
3 votes
0 answers
186 views

What is the known weakest axiom system has Löb's derivability conditions?

We know that Peano Arithmetic satisfies Löb's derivability conditions, which is required in the proof of Gödel's 2nd incompleteness theorem. Is this the best result? If not, is there any known weaker ...
Ruizhi Yang's user avatar
3 votes
0 answers
471 views

A question about the Chaitin constant of a theory

Chaitin's famous incompleteness theorem states that for every r.e. theory $T\supseteq Q$ in the language of arithmetic, there is a constant $d_T$ such that for any $m\geq d_T$ and any $x$, $T$ can ...
Payam Seraji's user avatar
1 vote
1 answer
497 views

A question on the provability predicate of Q

I am not familiar with Robinson's construction as I do not have access to his text or to precise accounts of this, but I have come to understand that the proof predicate of Robinson arithmetic is non-...
Frode Alfson Bjørdal's user avatar
10 votes
2 answers
596 views

Bounded Arithmetic vs Complexity Theory

In this post, when I talk about bounded arithmetic theories, I mean the theories of arithmetic according to "Logical Foundations of Proof Complexity", which capture the complexity classes between $AC^...
John's user avatar
  • 103
16 votes
2 answers
1k views

Is there a consistent arithmetically definable extension of PA that proves its own consistency?

I asked this on stackexchange with no answer. The negation would be the obvious generalization of Gödel's second incompleteness from r.e. extensions of PA to any arithmetically definable extension of ...
vhspdfg's user avatar
  • 435
6 votes
1 answer
335 views

Adding a truth-like predicate to PA

It is well known that adding a truth predicate to arithmetic in the most natural way leads to a contradiction. Suppose as usual that we add a one place relation T to the language of arithmetic, and ...
Cecilia Burrow's user avatar
4 votes
0 answers
205 views

Set theory and forcing from the point of view of a formal system $G^+$ of Gentzen type

There are four papers by Vladimir Alfeevich Kuznetsov, which discuss the above titled topic: (1) Some problems in set theory from the standpoint of a formal system G+ of Gentzen type. (Russian) Akad. ...
Mohammad Golshani's user avatar
3 votes
0 answers
183 views

Reducing Consistency of $PA$ [closed]

By godel translation consistency of $PA$ is equivalent to consistency of $HA$. I want to know any similar theorems for $PA$. 1.What is the minimal theory $T\subsetneq PA$ such that the proof of $PA\...
Erfan Khaniki's user avatar
13 votes
1 answer
661 views

Intutionistic Robinson Arithmetic

By Friedman translation $HA$ and $PA$ prove the same $\Pi_2$ formulas. Is it true for Intutionistic Robinson arithmetic(Robinson axioms with intutionistic logic) and classic Robinson arithmetic? ...
Erfan Khaniki's user avatar
3 votes
1 answer
673 views

Why is a cut-free system consistent?

Assume that the cut-elimination theorem holds for a system $T$. Then, for any proof that makes use of the cut-rule in $T$, there is a proof that does not make use of the cut-rule. An immediate ...
StudentType's user avatar
4 votes
1 answer
321 views

How do I evaluate this sum for $s$ is a complex variable :$\sum_{n=1}^{\infty} \frac{(-1)^{n+1}}{n^{2s}n!}$?

This question related to this question in SE ,I would like to know how do I evaluate this sum for $s$ is a complex variable :$$\sum_{n=1}^{\infty} \frac{(-1)^{n+1}}{n^{2s}n!}$$ . Edit01:And I think ...
zeraoulia rafik's user avatar
15 votes
3 answers
1k views

Algorithmic complexity of formal proof verification?

In this question, suppose $S$ is some popular real-world automated proof system that is stronger than or equivalent to Peano Arithmetic. I would be happy with a positive answer to the following for ...
Andrew Critch's user avatar
6 votes
3 answers
2k views

Euler's constant: irrationality and proof theory

Let $\gamma$ represent Euler's constant. Is there a real number $x$ such that there is a proof within Zermelo-Fraenkel set theory (ZF) that $x$ is irrational and there is also a proof within ZF that $\...
user36012's user avatar
2 votes
0 answers
118 views

A Question on Provability Logic and Co-Necessitation

The provability logic $GL$ has the characteristic axioms: $K\hspace{15pt}\Box(\alpha\rightarrow \beta)\rightarrow(\Box\alpha\rightarrow\Box\beta)$ $L\hspace{15pt}\Box(\Box \alpha\rightarrow \alpha)\...
Frode Alfson Bjørdal's user avatar
5 votes
2 answers
533 views

Does the notion of provably total function depend on the chosen representation?

A typical definition of "provably total function in a theory $T$" goes like this (paraphrased from Odifreddi, Classical Recursion Theory II): A function $f : \mathbb{N}^n \to \mathbb{N}$ is ...
Andrei Sipoș's user avatar
10 votes
0 answers
443 views

(A little bit) Beyond the E-recursive

The E-recursive functions are a particular generalization of classical recursion theory to the entire set-theoretic universe, $V$. They are defined via a schemes: see Sacks' $E$-recursive intuitions. ...
Noah Schweber's user avatar
41 votes
6 answers
4k views

Hilbert's (cancelled) 24th problem

Hilbert's 23 problems, ten of which were presented at the 1900 ICM in Paris, are too famous for any mathematician to not know. If one reads the descriptions of the problems in Hilbert's paper, one ...
Burak's user avatar
  • 4,115
13 votes
0 answers
519 views

Large cardinals arising from alternate set theories

My question is whether there are model-theoretic large cardinal axioms associated with $NFU$ - or more generally, with set theories other than $ZFC$. Large cardinal properties generally come in one ...
Noah Schweber's user avatar
9 votes
1 answer
375 views

Proof-theoretic ordinals after liberalizing induction to $RCA_0$

This is kind of a follow-up to this question. For a class $\Gamma$ of second-order formulas (here either $\Sigma_n^0$ or $\Sigma_n^1$), let $X\Gamma$ be a formal theory consisting of $RCA_0$ together ...
Wojowu's user avatar
  • 27.4k
5 votes
0 answers
236 views

What useful admissible rules does ZFC have beyond the deduction theorem?

I'm interested in formal proof verification, and one of the surprisingly difficult parts of this is dealing with proofs by contradiction. The issue is that the final step of such proofs is typically "...
Alexander Smith's user avatar
4 votes
0 answers
154 views

Undecidability of the existential theory

Do you know if I can find the proof that the existential theory of $\mathbb{Z}$ with the structure of addition , divisibility and the relation $(\exists s \in \mathbb{Z})m=np^s$ is undecidable, ...
Mary Star's user avatar
  • 299
0 votes
2 answers
279 views

Undecidable set of problems [closed]

Is there some set of problems, for which determining if given problem is decidable or not is itself undecidable?
M.Martin's user avatar
8 votes
1 answer
664 views

Which ordinals are proof-theoretic ordinals?

Few months ago I have posted this question on MO, but I must admit that at the time, admittedly, I had no idea on how technical proof-theoretic considerations can be. I have decided to revise this ...
Wojowu's user avatar
  • 27.4k
0 votes
1 answer
299 views

Provability of unprovability

I have three questions (without any real background, this is just something I've been wondering about recently) Can PA prove that PA can't prove nor disprove, say, Goodstein theorem (or any natural ...
Wojowu's user avatar
  • 27.4k

1 2 3
4
5
8