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
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 ...
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 ...
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$-...
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 (...
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" ...
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}...
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 $...
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])},$$
...
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}$ (...
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 ...
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 ...
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 ...
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 $$\...
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 ...
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 ...
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 ...
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) ...
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 ...
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$ ...
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 ...
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 ...
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....
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 ...
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, ...
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, ...
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 ...
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 ...
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$'...
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 ...
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 ...
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 ...
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{...
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 ...
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 $...
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 ...
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 ...
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, ...
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 ...
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$ ...
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 \...
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 ...
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 ...
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 ...
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 ...
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{...
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, ...
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 ...
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{...
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) \...
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 ...