Proof theory is an area of logic that studies proof as formal mathematical objects. For questions asking how to write proofs or for checking an informal proof, please use the proof-writing or proof-strategy tags instead.

learn more… | top users | synonyms

0
votes
0answers
59 views

How do I create this geometry proof? [duplicate]

I understand that a similar question like this has been asked before however, I did not understand the answers given. Thus, I would really appreciate it if you were to attempt to give an ...
0
votes
1answer
54 views

Prove every angle has a bisector.

Prove every angle has a bisector. I have successfully constructed a bisector and justified by construction. Now I need to put it in proof form. However, I technically do not know midpoints and ...
0
votes
1answer
47 views

What is the logic behind Jacobi iterative method?

The book I follow and on net also, all that I can find is the algorithm to find the solution, but I don't quite understand the physical significance or logic behind the algorithm. Can someone please ...
5
votes
6answers
147 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 ...
0
votes
0answers
47 views

Law of one price theorem proof

There are two subparts to Fundamental Asset Pricing theorem. The LOOP (Law of one price) holds if and only if there exists a state price vector. In a market in which the LOOP (law of one price) ...
0
votes
1answer
30 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 ...
0
votes
1answer
35 views

Set and Logic, Proving two quantifier the same

$(∃x∈A:P(x))∨(∃x∈B:P(x)) = ∃x∈(A∪B):P(x)$ I spent hours approaching this problem many different way By Definition: $(∃x∈A:P(x))∨(∃x∈B:P(x)) \\ ∃x:[(x∈A \to P(x) \vee (x∈B \to P(x)] \\ ∃x:[(¬x∈A ∨ ...
0
votes
1answer
134 views

Proof of subspaces of odd and even functions

$F^+(\mathbb{R})$, the set of even functions in $F(\mathbb{R}, \mathbb{R})=\{ f: \mathbb{R} \to \mathbb{R} \}$ and $F^−(\mathbb{R})$, the set of odd functions in $F(\mathbb{R}, \mathbb{R})$ are both ...
2
votes
1answer
87 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 ...
0
votes
1answer
79 views

Mathematical Induction with Fermat's last theorem?

Question on Fermat's Last theorem: $\nexists a,b,c\in \mathbb N:a^n+b^n = c^n$ for all $n \in \mathbb N, n\ge 2$. Assume that we have shown a proof for the cases $n = 3$ and $n = 4$. Can we say ...
0
votes
0answers
45 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} ...
1
vote
1answer
73 views

Proof of existence of “peaks” in The Sequential Compactness Theorem

According to Bolzano–Weierstrass theorem: How do we guarantee that EVERY sequence of real numbers has either infinitely or finitely many "peaks"? (Note that a subsequent is ordered in a way of ...
2
votes
1answer
67 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 ...
0
votes
0answers
56 views

Theorem of Lefschetz

If anyone has the book of James D. Lewis entitled: A survey of Hodge conjecture on page $58$, There are the famous theorem of Lefschetz $(1,1)$ "without proof it seems to me." Is that so? Could you ...
0
votes
1answer
92 views

Prove that the sequence {an} does not converge by showing it is not Cauchy

Let an = {7 + 4/n if n is even, 8 - 1/n if n is odd}. Prove that the sequence {an} does not converge by showing that it's not a Cauchy sequence. This is what I have so far. Let $\epsilon$ > 0. For ...
0
votes
1answer
30 views

Left “ and” inference rule G3cp

If you are at the stage of $$((P\supset Q) \wedge (Q\supset \bot)) \Longrightarrow (P \supset \bot)$$ And then you apply an $L\wedge$ rule, Why do you get $$(P \supset Q),(Q\supset\bot)),P ...
0
votes
1answer
28 views

Example of an axioms in G3Cp

Would $$A,B,C \Longrightarrow C,A$$ be an axiom in G3Cp? I ask because B is not on both sides and I am not sure if that makes a difference or not?
1
vote
1answer
40 views

Proofs from the book: in Praise of inequality's

I am reading a book with nice proofs, but i struggle at a few points. 1) why is $\sum_{i=1}^{k} p_i \int_{a_i}^{G} (\frac{1}{t} - \frac{1}{G}) dt + \sum_{i=k+1}^{n} p_i \int_{G}^{a_i} (\frac{1}{G} - ...
0
votes
0answers
37 views

Proofs for PCA, LDA, ICA, HMM learning algorithms and other stuff

I was wondering if there is some kind of encyclopedia of website for all known math proofs. I'm more interested in statistics (PCA, ICA, LDA, Factor analysis, HMM learning, GMM learning) and algebra ...
0
votes
3answers
232 views

Proof of the Dirichlet–Dini Criterion for Pointwise convergence of Fourier series

I have tried and failed to prove the Dirichlet–Dini Criterion for Pointwise convergence of Fourier series which is as follows (and is described here: ...
1
vote
1answer
41 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
0
votes
2answers
50 views

How would one prove this flavour of the triangle inequality?

I have to prove $|z_1 - z_2| \leq |z_1|+|z_2|$ where $z_1,z_2$ are in $\mathbb{C}$. What I wrote down is: $$|z_1| = |z_1+z_2-z_2| \geq |z_1-z_2|-|z_2|\implies |z_1|+|z_2|\geq |z_1-z_2|,$$as desired. ...
1
vote
0answers
21 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 ...
0
votes
0answers
20 views

Is it decidable whether there are finitely or infinitely many positive integers n such that the (2^n)+1th last digit of 3^(2^n) in base 2 is 1.

It seems so obvious that there are infinitely many such n because using a probabilistic arguement, it seems like there's no chance of there only being finitely many of them. Yet, it seems impossible ...
2
votes
1answer
50 views

Next step to reach the contradiction?

This is a problem from Discrete Mathematics and its Applications Here are my notes and my current work so far for this problem. I started with an assumption that what i am trying to prove is ...
0
votes
2answers
60 views

What to use for r in proof by contradiction?

This is a problem from Discrete Mathematics and its applications To this proof, I am trying to use proof by contradiction. Here is how the book described the process of proof by contradiction. I ...
0
votes
0answers
41 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 ...
3
votes
2answers
86 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 ...
0
votes
1answer
62 views

What is the slowest growing function that cannot be proven to be total by PA?

I asked the question if PA can prove any function growing faster than $f_{\epsilon_0}(n)$ to be total. The answer was no. What about the converse : Can prove PA every function growing slower than ...
0
votes
2answers
54 views

Inference rule for Non-Empty Domains

I am currently experimenting with logic frameworks. I am basically using something along dependent types as in "Proof-assistants using Dependent Type Systems" by Henk Barendregt and Herman Geuvers. ...
4
votes
2answers
84 views

Is there any unreachable result?

I hope that this question is reasonable and make sense because I am not sure. Every theorem's proof is consisting of finite logical steps. Can a proof of the theorem require infinitely many ...
3
votes
0answers
71 views

Is the following derivation of Gödel's Paradox generalizable to an intuitionistic one using provability?

I will follow Goedel's original proof of Goedel's paradox located on pg. 264 of Hao Wang's A Logical Journey: From Gödel to Philosophy. With this in sight, and to also avoid confusion, I will also ...
7
votes
1answer
56 views

Can PA prove very fast growing functions to be total?

The Goodstein-sequence is a total function, but PA cannot prove this. Is this true for any other function with growth rate at least $f_{\epsilon_0}$ or are there functions growing at least as fast ...
1
vote
1answer
69 views

Proof in sequent calculus without cut

I met an exercise in Gaisi Takeuti, Proof Theory [Exercise 2.7, page 14]. How to construct a cut-free proof of$\ \forall xA(x)\rightarrow B\vdash \exists x(A(x)\rightarrow B)$, where A(a) and B are ...
1
vote
1answer
138 views

2 Questions regarding Relative Consistency Proofs

First Question: Let IC be the statement "There is an inaccessible cardinal." I have read that one cannot prove (in ZFC) the relative consistency of ZFC + IC w.r.t. ZFC. i.e. $ Con(ZFC) \rightarrow ...
-3
votes
1answer
66 views

fake proof of $\forall a. \forall b. a = b \to 1 = 0$

I saw a less formal version of this fake proof that claimed to prove $2=1$ but because it assumed $a=b$ from the start I knew why it was wrong. It does seem however that the proof can be used to prove ...
0
votes
1answer
74 views

Beginning Haskell - cannot understand proof

I've just started reading "Thinking Functionally with Haskell" by Richard Bird In the preface he states : And after stating the proof he also states the proof will be used throughout the book. ...
1
vote
2answers
31 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 ...
1
vote
1answer
114 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 ...
1
vote
2answers
85 views

Help with understanding this proof in discrete mathematics?

This is the question and solution: Q: Prove that for any integer $a$, $2a + 1$ and $4a^2$ + 1 are relatively prime. A: Since $4a^2 + 1 = (2a − 1)(2a + 1) + 2$, any common divisor of $2a + 1$ and ...
-2
votes
1answer
54 views

Proof by induction of this formula? [duplicate]

$2^0+2^1+2^2+...+2^n$ for $n ∈ \mathbb{N}$ U ${0}$. I made a conjecture that this is $2^{n+1} - 1$. Now I have to prove it by induction. I tested the base case where it's equal to zero, and it ...
-2
votes
1answer
35 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 ...
0
votes
1answer
47 views

Did I do this big-Omega proof correctly?

Prove or disprove: 6n^3 – 4n^2 + 3n +2 is in Ω (5n^3 – n^2 + n +1). So I'm not sure if I did this right or not, any pointers or the correct steps would be helpful Ǝc ∈ ℝ+, ƎB ∈ ℕ, ∀n ∈ ℕ, n ≥ B ⇒ ...
0
votes
1answer
30 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$ ...
0
votes
1answer
26 views

Define $f:\mathbb{Z}/4\mathbb{Z}\to \mathbb{Z}/4\mathbb{Z}$ by $f([a])=[3a+1]$.

Define $f:\mathbb{Z}/4\mathbb{Z}\to \mathbb{Z}/4\mathbb{Z}$ by $f([a])=[3a+1]$. Prove that $f$ is well-defined, surjective and injective I don't really have a problem with figuring out if it's ...
1
vote
5answers
83 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 ...
1
vote
1answer
95 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 ...
2
votes
0answers
52 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 ...
0
votes
1answer
57 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 ...
1
vote
1answer
63 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 ...