Questions tagged [proof-theory]

Proof theory is an area of logic that studies proof as formal mathematical objects. If you'd like advice on the presentation of a proof you have in draft, use proof-writing instead. If you'd like feedback on its validity, use proof-verification. If none of the above apply, you do not need a proof-* tag.

214 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
15 votes
0 answers
371 views

What are some arguments/counterarguments for Zeilberger's "proof certificates"?

Here is the quote I wish to ask about: "I speculate that similar developments will occur elsewhere in mathematics, and will 'trivialize' large parts of mathematics, by reducing mathematical ...
GPerez's user avatar
  • 6,766
13 votes
0 answers
1k views

Is there a Sokoban level with such conditions

First of all, let me explain what Sokoban is. It is a logic game created in Japan and it literally means "warehouse keeper". It is a type of transport puzzle, in which the player pushes boxes or ...
user avatar
13 votes
1 answer
598 views

The ethics of Borel determinacy

I was speaking with a friend the other day, and I happened to say "morally, Borel determinacy is as strong as ZF." I was riffing on the well-known result of Harvey Friedman, that we need $\omega_1$-...
Noah Schweber's user avatar
12 votes
0 answers
682 views

Why don't the quantifiers split in linear logic?

Every presentation of linear logic I've seen seems to either omit or treat quantifiers as an after-thought. Even Girard says that there is "little to say" about them. However, if we view universal (...
user181407's user avatar
8 votes
0 answers
551 views

Proof by reflection and Homotopy Type Theory

I have been looking into various proof assistants, and came across the method of proof by reflection in Coq, which (from what I understand) allows one to verify a program provides the correct "answer" ...
John Colanduoni's user avatar
7 votes
0 answers
168 views

Can all $\mathsf{Q}$-provably recursive functions be "frequently termlike"?

Now asked at MO. Motivated by this question, I'd like to ask whether in a precise sense there are no "interesting" functions which are provably recursive in Robinson's arithmetic $\mathsf{Q}...
Noah Schweber's user avatar
7 votes
0 answers
100 views

What is the "validity logic(s)" of moderate theories?

This question is motivated by this old answer of mine. Below, by "appropriate theory" I mean any consistent finitely axiomatizable theory in the language $L_2$ of second-order arithmetic containing $...
Noah Schweber's user avatar
7 votes
0 answers
242 views

What is this property exhibited by some logical systems?

The following property exhibited by some logical systems has captured my attention: $$\forall X\; ( {\vdash x_1[X]} \implies {\vdash x_2[X]} ) \implies \forall X\; {\vdash (x_1[X]\to x_2[X])},$$ ...
Hans Brende's user avatar
6 votes
0 answers
101 views

Who is the "$\Pi_2$-soundness" version of the first incompleteness theorem due to?

I'm trying to remember who is responsible for the following well-known weak version of the first incompleteness theorem: Suppose $T$ is a c.e. consistent $\Pi_2$ extension of Robinson's $\mathsf{Q}$ (...
Noah Schweber's user avatar
6 votes
0 answers
137 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 ...
Robin Saunders's user avatar
6 votes
0 answers
517 views

Metamathematics and the foundations of mathematics

I have some really big doubts about what is the real starting point of all (formal) mathematics. For example: when I search on internet or study texts about the foundations of mathematics such as ...
luis_orion's user avatar
6 votes
0 answers
81 views

Axiomatizing a "bounded" companion to PA

There's nothing special about PA here, I'm just focusing on it since it's strong enough to ignore lots of minor technical issues around foundations. If switching to some other theory would yield a ...
Noah Schweber's user avatar
5 votes
0 answers
169 views

Proving $\exists x[P(x)] \to \exists y[\exists x[P(x)]\to P(y)]$ in for intuitionistic $\varepsilon$-calculus.

I am researching Mint's paper: Intuitionistic Existential Instantiation and Epsilon Symbol (this is as far as I know unfinished work) In intuitionistic logic, it is not difficult to prove that $$\...
Tungsten's user avatar
  • 130
5 votes
0 answers
84 views

When should one use transfinite induction?

I've come across it multiple times now in proof theory papers that authors use (sometimes quite elaborate) inductions in order to prove easy results. The most striking example is the following, where ...
10012511's user avatar
  • 682
5 votes
0 answers
124 views

Are soundness and completeness a part of proof theory, model theory or something else?

I have a question that I hope can clarify the scopes of model theory and proof theory. I have the following naïve understanding of the two areas (please correct me if I'm wrong): Model theory is ...
dumbo's user avatar
  • 71
5 votes
0 answers
145 views

Can ZFC decide more values of the Busy Beaver function than PA?

This is related to a previous question. In that question, I asked whether ZFC can define the Busy Beaver function. I was told even Peano Arithmetic(PA) can define it, and also that PA can't decide ...
user107952's user avatar
  • 20.4k
5 votes
0 answers
126 views

Calculi for the category theory?

Some branches of mathematics admit calculi with whom one can do syntactical (language-like, grammatical) or geometric operations to arrive at certaing conclusions. The syntactical part (proof theory) ...
TomR's user avatar
  • 1,313
5 votes
0 answers
161 views

How much arithmetic is required to formalize quantifier elimination in Presburger arithmetic?

As we know, Presburger arithmetic can be proved decidable by demonstrating that it admits quantifier elimination, i.e. that there is an algorithm that reduces any sentence in the language to some ...
Morgan Sinclaire's user avatar
4 votes
0 answers
193 views

Examples of statements which, if true, have unreasonably long proofs

In $\mathbf{Q}$ (or any theory strong enough to encode $\mathbf{Q}$), there exist true statements whose proofs cannot be written in under $N$ symbols for a fixed $N$. For example, if $N = 1000000$ ...
mattematician 's user avatar
4 votes
0 answers
57 views

Gaps between intutionistic and classical arithmetic

Let $\mathrm{I}\Sigma_n$ stand for the classical theory of Robinson arithmetic + bounded induction + induction on $\Sigma_n$ formulas. Let $\mathrm{CI}\Sigma_n$ stand for the intuitionistic theory of ...
univalence's user avatar
4 votes
0 answers
466 views

Open problems in Proof theory and Logic

There are numerous questions in the same form: "What are some open problems in mathematical logic". So for this we know: Shelahs "Logical Dreams" Logical Dreams Friedmans "102 ...
LogicTheorist's user avatar
4 votes
0 answers
91 views

Has something like the Turing Machine that halts if ZFC is inconsistent been done for other axiom systems?

The current best result (as far as I could find) is that there exists a $748$-state Turing Machine that halts iff ZFC contains a contradiction. Are there any similar results for other axiom systems, e....
Kotlopou's user avatar
  • 375
4 votes
0 answers
101 views

Every provably recursive function in PA is bounded by a Hardy function

The following lemma and proof are from Takeuti's Proof Theory (2nd edition, pp. 126-127), I've highlighted the problematic part in blue: How does Takeuti get this inequality? If the proof $x$ is not ...
Jori's user avatar
  • 1,698
4 votes
0 answers
100 views

Characterization of provably recursive functions in PA

This concerns Takeuti's Proof Theory: the book contains a lot of wonderful material, but the presentation is sometimes lacking (and so many typos!). At least that has been my experience so far, ...
Jori's user avatar
  • 1,698
4 votes
0 answers
139 views

self-contained vs. non-self-contained notions of realizability

There seem to be two notions of realizability in literature, where in one case the realization of a formula is fully self-contained with respect to providing a proof object for the given formula, ...
ternary's user avatar
  • 371
4 votes
0 answers
138 views

Strongest tools to detect unsoundness

I am curious about the strongest computable methods we currently know of that can allow us to possibly discover (arithmetical) unsoundness or nonstandardness in a foundational system $S$ that ...
user21820's user avatar
  • 57.3k
4 votes
0 answers
146 views

Can we prove consistency of Euclidean geometry in Peano arithmetic?

It is obvious that the statement that asserts consistency of euclidean geometry (in fact its formalized versions due to Hilbert and Tarski) is a $\Pi_1$ sentence in the language of $PA$ (Peano ...
Payam Seraji's user avatar
4 votes
0 answers
232 views

A complicated, curious tableaux proof rule for Intuitionistic S4

In Amati and Pirri, A uniform tableau method for intuitionistic modal logics I (1993) a tableau method for a variety of intuitionistic modal logics is presented with signed formulas ('$\textbf{T}A$'...
user65526's user avatar
  • 1,373
4 votes
0 answers
84 views

Transforming intuitionistic propositional validities into validities of linear logic

A tableaux method for linear logic is briefly discussed in https://www.academia.edu/6591354/TABLEAU_METHODS_FOR_SUBSTRUCTURAL_LOGICS?auto=download D'Agostino writes (p.418-9): ''It is ...
user65526's user avatar
  • 1,373
4 votes
1 answer
434 views

Learning to do proofs: Examples or theory

So I have a couple of weeks to study what I want before heading back to college. I am debating whether to study multivariable calculus or to study how to write proofs in general. For context, I have ...
Striker's user avatar
  • 803
4 votes
0 answers
319 views

What is the relationship between Realizability and the Curry-Howard isomorphism?

I have recently been studying the Curry-Howard isomorphism/correspondence. My sources have primarly been Sørensen [1] and Girard [2]. Realizability is introduced here in the form of Kleene's ...
Matteo's user avatar
  • 146
4 votes
0 answers
98 views

Is it always possible to go from one identity to another?

This question was inspired by this Quora question. I'm sure lots of you are familiar with the fact that we have many different representations of $\pi$, things like $$ \begin{align} \pi & = \sqrt{...
user3002473's user avatar
  • 8,943
4 votes
3 answers
366 views

What are those "things that cannot be proved using only ordinary rules of inference"?

The online edition of the book Introduction to Logic by Michael Genesereth and Eric Kao, has a detail that left me confused. CHAPTER 4 [...] 4.2 Linear Proofs [...] The interesting thing about the ...
nlognfan's user avatar
4 votes
0 answers
209 views

What is the proof-theoretic strength of the predicative second-order theory of real numbers?

The first-order theory of real numbers, AKA the theory of real closed fields, is obtained by added to the axioms for ordered fields an axiom schema of completeness, which states that for each formula $...
Keshav Srinivasan's user avatar
4 votes
1 answer
338 views

Curry-Howard Correspondence (Proof Theory)

As you all know, the Curry-Howard correspondance provides a link between type theory and predicate logic. Concepts featured in the former, such as $\Pi$-type and $\Sigma$-type can, by the ...
user107804's user avatar
3 votes
1 answer
81 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,015
3 votes
1 answer
59 views

Michell FPL 2.3.5 (observable types)

(a) Show that the relation of observational equivalence remains the same when changing the observable types of pcf from nat, bool to nat. (b) Further show that changing from nat,bool to nat, bool, ...
emesupap's user avatar
  • 643
3 votes
0 answers
118 views

Proofs and Types: Girard's remarks on Theoretical Computing

In the first chapter of Girard's Proofs and Types (1989) one finds the following remarks: Theoretical Computing is not yet a science. Many basic concepts have not been clarified, and current work in ...
Max Demirdilek's user avatar
3 votes
0 answers
217 views

Which sentences are irreducibly self-referential?

Below, all sentences/formulas are in the language of arithmetic, and for simplicity we conflate numbers with numerals and sentences with Godel numbers. Now asked at MO. Say that a sentence $\varphi$ ...
Noah Schweber's user avatar
3 votes
0 answers
56 views

Comparing two semantics, equivalent in the global sense, not in the local sense?

I am working on a project that involves a deductive system $\vdash$, with two model-theoretic semantics $\models_A$ and $\models_B$, for which $\vdash$ is sound and complete. That is, $\Gamma \vdash \...
Eoin's user avatar
  • 369
3 votes
0 answers
102 views

Concrete examples of statements not provable in PRA + $\epsilon_0$-induction that are provable in PA?

It is well-known that $\mathbf{PRA}$ plus $\epsilon_0$-induction on bounded formulas cannot prove all $\mathbf{PA}$ theorems (essentially because $I\Sigma_1$ plus $\epsilon_0$-induction on bounded ...
Jori's user avatar
  • 1,698
3 votes
0 answers
89 views

Reducing the strength of a category theoretic proof

The motivation for this question is the following: Say we have a formula $\phi$ in peano arithmetic, and we have proof $\pi$ of $\phi$ using possibly higher order arithmetic or category theory (that ...
Couchy's user avatar
  • 2,722
3 votes
0 answers
106 views

Optimal bound for cost of cut elimination in infinitary logic with transfinite cut-rank in terms of Veblen's $\varphi$ function

The theorem I am referring to is Tait's sharpening of Gentzen's Cut Elimination Theorem in [1], which Schütte [2, p. 204, Theorem 22.8] also calls the ``second cut elimination theorem'' (here written ...
10012511's user avatar
  • 682
3 votes
0 answers
143 views

Hilbert calculi for First-Order Logic

I'm a bit confused about the Hilbert-style axiomatization of first-order logic. More precisely, I am a bit confused about completeness w.r.t. to Hilbert-calculi. A complete Hilbert-style calculus I am ...
blub's user avatar
  • 4,784
3 votes
0 answers
174 views

What does it mean for a type system to be "inconsistent"?

This paper on the calculus of inductive constructions states: The need for an infinite hierarchy of universes comes from the fact that the more naive system where we have only one sort $\mathsf{...
user83014's user avatar
3 votes
0 answers
181 views

Cut elimination proofs of the consistency of arithmetic

It is well known that one can use cut elimination to establish the consistency of arithmetic (though this involves assuming transfinite induction up to a particular countable ordinal.) Most proofs, ...
provocateur's user avatar
3 votes
0 answers
166 views

Why can't the sequent calculus for First-Order Classical Logic be used for proving decidability via Proof-search?

I understand that Turing reduced the halting problem to the satisfiability problem of first-order logic thus proving first-order logic undecidable. However, when thinking about the sequent calculus ...
Joe Smith's user avatar
3 votes
0 answers
61 views

What will be the notion of a "valid deduction" in the following system?

Consider the Propositional Calculus whose axiom schemes and rule of inference are given below (here $P,Q$ and $S$ are formula schemes, $\color{crimson}{\text{Axiom 1.}}\ P\to (Q\to P)$ $\color{...
user avatar
3 votes
0 answers
362 views

Formal proof of $\exists x (\exists y P(y) \rightarrow P(x))$ and $(\forall x \exists y R(x,y))\rightarrow (\forall y \exists x R(y,x))$

within the following axiomatic system I've beeb trying to proof the formulas (1) $\forall x \exists y R(x,y) \rightarrow \forall y \exists x R(y,x) \\$ and (2) $\\ \exists x (\exists y P(y) \...
Studentu's user avatar
  • 599
3 votes
0 answers
220 views

Model for the type-theoretic axiom of choice in Coq.

This is the request for references. It is a known fact that there is a model of ZFC in ZF, so ZFC is consistent if ZF is consistent. It is also know that there is a double-negation Godel-Gentzen ...
georgy_dunaev's user avatar

1
2 3 4 5