# Tagged Questions

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-* ...

53 views

### Proof of cut elimination

I am reading Proofs and types and am blocked at the proof of cut elimination in sequent calculus (chap 13). I don't see either how the cuts are being pushed up above the preceding steps to the top of ...
63 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" ...
768 views

### What does “rigorous proof” mean?

I have heard several times that some mathematician has given another and more rigorous for an established theorem, but I don't know what does it really mean and what differences makes it to be more '...
35 views

### Problem with a step in a proof in predictive control

I'm trying to follow a demontration written in an optimal control paper. In one of the steps, it states What I'm having troubles with is the last step, it states that because of the convexity of ...
97 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 ...
78 views

### Encyclopedia of Mathematical Proofs with no English

I was wondering if anyone is aware of a modern book that builds a subset of elementary number theory from Peano axioms preferably in a Principia Mathematica fashion? Or similarly an encyclopedia of ...
114 views

### Consistent, complete axiom system that proves its own consistency

Is there a consistent, complete axiom system that proves its own consistency? I know that this question isn't exact and I haven't defined when an axiom system proves its own consistency because that'...
88 views

### What kind of trivial statement still needs to be proven?

There are many statements that seem to be needless of a proof since they are ‘evident’ mainly because of our intuition. But some of them have proofs. For example, in C. Adams’ Introduction to topology,...
238 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$-...
55 views

65 views

### More details of the “Standard View og Proof” with three points are needed.

I have a Danish book about the theory of knowledge for mathematicians which I have tried my best to translate some parts into English. According to the lecturer, we can with "certain reasonability" ...
2k views

### Why is Gödel's Second Incompleteness Theorem important?

Given that the consistency of a system can be proven outside of the given formal system, Gödel says, It must be noted that proposition XI... represents no contradiction to the formalities ...
172 views

### Notable examples of “impossible” results ruled out by earlier barrier or no-go theorems or widespread beliefs

there is a certain style of type of proof in mathematics something like a "barrier theorem" but which also relates to widespread mathematical beliefs/ "conventional wisdom". an example would be the ...
49 views

### Inversion lemma for G3ip

I'm following the book Structural Proof Theory by Negri and others. In it, they claim on page 32 about G3ip that if $⊢ _ n A \& B, Γ ⇒ C$, then $⊢ _ n A, B, Γ ⇒ C$. But, given that the only ...
142 views

### What are 2-morphisms in the category of proofs?

After reading through "Categories for the practicing physicist" I came to learn there is a category whose objects are propositions $A,B,...$ and whose morphisms are proofs $f:A\rightarrow{B}$ that ...
64 views

### Is the length of the proof of propositional tautology a PA-total function?

Suppose we have fix some interpretation of propositional (not first-order!) logic inside PA, and say $f(n) =$ {the maximum length of a proof of a tautology with $n$ propositional primitives} ...
88 views

### Couple of questions from Takeuti's Proof Theory book

I am reading Gaisi Takeuti's Proof Theory (Second Edition, Dover), and I have a couple of questions: I) Right after the first (1.1.) definition, the author says that "In any case it is essential that ...
33 views

50 views

### What is the proof-theoretic ordinal of $PA+TI(\epsilon_0)$?

what is the proof-theoretic ordinal for $PA+TI(\epsilon_0)$, where $PA+TI(\epsilon_0)$ is Peano arithmetic where transfinite induction up to $\epsilon_0$ was added? Is it known? Thank you
24 views

### Independence of FLT over weak systems

It is known that Fermat's last theorem can be proven in finite-order arithmetic (e.g. accoridng to this site). This is still an extremely high upper bound on proof complexity (for example, compared to ...
77 views

### Are proofs for many-sorted first order logic shorter than single sorted first order logic?

I understand that the expressive power of first order logic with one sort is the same as any many sorted first order logic, and that higher order logic with general semantics is the same as a many ...
115 views

### What is the fastest growing primitive-recursive-function?

Fast growing functions tend to be not primitive-recursive. So I wonder if there is a limit how fast a function can grow, if it is known that it is primitive recursive. What is the fastest growing ...
117 views

32 views

### What does this proposition mean?

$∀x ∈ P(\Bbb{N}), x \notin \{\} \Rightarrow ∃y ∈ x, ∀z ∈ x \ | \ y < z$ Where $P(x)$ is the power set. I'm interpreting it as "in all subsets of the natural numbers, there exists a value smaller ...
180 views

### How to check homeomorphic embedding relation programmatically?

This is a follow up to this question and Deedlit's answer. I'm looking for a precise definition of the "hem?" (tree A homeomorphically embeddable in tree B?) relation, preferably in terms of a ...
50 views

### Z / 6Z being a set of well dedfined equivalence classes, and a congruent to b(mod 6)

why is this = [0],[1],[2],[3],[4],[5],[6] and how would I define f Z/6Z - Z/6Z by f([a]) = ([2a]). I have the proof but I don't understand it. Proof: Assume [a1] = [a2] in Z/6Z. then a1 congruent to ...
77 views

### Proving Theorem: subspace of polynomials of degree two or less?

How can I prove that the set $S$ of polynomials of degree $2$ or less, whose coefficients sum to zero, is a subspace of all polynomials with degree $2$ or less? I know I need to show that $a+b+c=0$ ...
117 views

### Proof by Induction Divisibility.

$6^n-5n+4$ is divisible by 5 for all positive integers $n$. $n >=1$ Prove By Induction My attempt is as follows: $n=1$ $6^1-5(1) +4$ $=5$, Therefore 5 is divisible by 5 so $n=1$ is true ...
101 views

### Uncountable reals in the theory

The Question I'm looking for a possibility to somehow proof the "essence" of Cantor's diagonal argument within a recursive first-order theory which is satisfied by the reals (better: within a theory ...
64 views

### How far can-I rewrite in lambda functions?

I am quite new with the lambda calculus. I am experimenting lambda-calculus proofs through the coq proof assistant, but the question I have is not related to coq (I guess). However, I'm going to use ...
99 views

### Euclid's proof for infinitely many prime numbers

Prove that there are infinitely many primes congruent to 3mod4 using euclid's proof for infinitely many prime number. I guess I don't really know where to start because I don't understand euclid's ...
76 views

### Comparing Statements and predicates using Truth Tables

Consider the four statements: $∃x$ $∀y$ $p(x, y)$ $∃y$ $∀x$ $p(x, y)$ $∀x$ $∃y$ $p(x, y)$ $∀y$ $∃x$ $p(x, y)$ which we call S1, S2, S3 and S4 respectively. Does there exist a predicate p such ...
62 views

### Model-theoretic question about language of field theory.

Let $\mathscr{L}=\{+,·\}$ be the language of the theory of fields. Let $\phi$ be a sentence in this language. Show, using the compactness theorem of first-order logic, that if $\phi$ holds in finite ...