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

5
votes
1answer
181 views

What is the proof-theoretic ordinal of the first-order theory of real closed fields?

I recently asked a question on MathOverflow, concerning a predicative second-order theory of real numbers. Now the standard way of developing predicativity in the case of second-order arithmetic is ...
4
votes
1answer
185 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 ...
4
votes
1answer
128 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 ...
2
votes
1answer
58 views

What is meant by “constant” in Liouville's Theorem?

Liouville's Theorem states that: Every holomorphic* function for which there exists a positive number M such that $|f(z)| \le M$ for all $z \in \mathbb C$ is constant. I'm using this to prove ...
2
votes
1answer
74 views

Maximal Principle: Why using the new transition matrix $\tilde{P}$?

First some notation: Let $(X,E,P)$ denote a finite, irreducible Markov chain with finite state space $E$ and transition matrix $P$. Choose and fix a subset $E^°$ of $E$, which will be called ...
2
votes
1answer
167 views

What if 'proof by contradiction' is not a valid method of proof?

I've just been reading this question about the existence (or lack thereof) of contradictions in maths. I've been wondering: What if 'proof by contradiction' is not a valid method to (dis)prove a ...
1
vote
1answer
20 views

Clarification when using Mean Value Property to prove Fundamental Theorem of Algebra

We say that $f$ satisfies the Mean Value Property (MVP) on a ball $B(a,R) = \{z; |z-a| <R \}$ if $$ f(a) = \frac{1}{2 \pi} {\int_0}^{2\pi} f(a + te^{i \phi}) d \phi$$ for $0 < t <R.$ It is ...
1
vote
1answer
56 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 ...
1
vote
1answer
35 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
1
vote
1answer
69 views

Infinitely many proofs?

While compiling a list of my favorite proofs of the infinitude of primes, the following came to mind; Proposition: There are infinitely many non-isomorphic proofs of the infinitude of primes. I'm ...
1
vote
1answer
445 views

proof of validity of tautology in first order logic

Every first-order logic formula which has a tautological shape in propositional logic is a valid formula. Will it be possible to give a formal proof for the above ? Thanks and Regards.
0
votes
1answer
38 views

Prove by contradiction that a circle chord is no longer than its diameter

Can anyone help me with this homework question of mine? I'm actually new to discrete mathematics and to be specific, with proofs. Here's the question, "Prove, by contradiction, that no chord of a ...
0
votes
1answer
45 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
24 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
46 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
47 views

Proving Properties in Ordered Fields

Refer to Definition 1.3, which states, an ordered field is a field F that is ordered set with the following additional properties: ...
0
votes
1answer
43 views

Cartesian product proof with counterexample

I was asked to disprove the following statement by counterexample: Let A, B and C be sets. If A x C = B x C then A = B I was under the impression that: (x1, y1) = (x2, y2) if and only if x1 = x2 and ...
0
votes
1answer
25 views

Struggling with proof, by contrapositive?

I am having trouble solving this proof. I tried to do a proof by contrapositive. Q = $(u+z)/(v+w) < z/w$ P = $(u/v < x/y \land x/y < z/w)$ Assuming $\lnot Q$ got me: $u/v \ge z/w$ ...
8
votes
0answers
130 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 ...
3
votes
0answers
63 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 ...
3
votes
0answers
53 views

Using an automatic tool for checking geometric conjectures

I do a lot of research about squares, and I thought of using some automatic tool for proving / disproving some geometric conjectures. As a simple example, consider the following Square coloring ...
2
votes
0answers
34 views

What exactly is wrong with this argument (Lucas-Penrose fallacy)

Argument "For every computer system, there is a sentence which is undecidable for the computer, but the human sees that it is true, therefore proving the sentence via some non-algorithmic method." ...
2
votes
0answers
45 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 ...
2
votes
0answers
74 views

How much arithmetic can Predicative Second-Order EFA do?

As discussed in this MathOverflow question, I'm trying to find what the result would be of applying a Feferman-Scutte-like analysis to the predicativism of Edward Nelson and Charles Parsons, who ...
2
votes
0answers
260 views

Difference between soundness and correctness

Is there any actual semantic difference between soundness and correctness? Can I use these words interchangeably when talking about formal reasoning, proof, logics, etc.? Otherwise, is there a ...
1
vote
0answers
46 views

Show that if A and B are strictly convex, then A + B is strictly convex or provide a counter example.

We have: If A is open: $\exists x,y \in A,$ $x \neq y$ such that $\lambda x+(1-\lambda y)\in \dot A $ (the interior) and $\exists u,v \in B,$ $x \neq y$ such that $\lambda u+(1-\lambda v)\in ...
1
vote
0answers
27 views

Is the full strength of first-order logic needed for dealing with equational theories?

More specifically, if we have an equational theory $T$ (a set of equations understood as being implicitly universally quantified), are the (equational) consequences of $T$ that can be proved with ...
1
vote
0answers
57 views

Disproving $\neg Q$ proves Q in all cases?

Does disproving the negation of a claim prove the claim in all scenarios and sufficient enough to say Q is true? Even if Q is an implication, or an equality, or etc? What about vacuous truths? Can ...
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 ...
1
vote
0answers
59 views

Is a sentence in $\Pi_1$ true given $Q \vdash \lnot\varphi$?

If $Q \vdash \lnot\varphi$ (Q is the Robinson arithmetic), and if I assume that $\varphi \in \Pi_1$; Can I say that $\varphi$ is a true sentence? My thoughts are that, given that Q is $\Sigma_1$- ...
1
vote
0answers
104 views

Do we know that if $\pi$ is normal then there is a proof of it?

We do not know whether $\pi$ is normal or it is not and many other weaker statements, e.g. (*) $\pi$ contains infinitely many $0$s. Inspired by the Godel's incompleteness theorem that there are some ...
1
vote
0answers
42 views

A question about $KP + V = L$ and $KP$ set theory.

In reading Rathjen (Choice principles in constructive set theories) and Jager (On Feferman's OST) I've come across two facts that are taken as obvious/well known, and probably are, but for which I ...
1
vote
0answers
39 views

Girard's System $F$ (also named Polymorphism)

I have been studying Girard's Polymorphism and a question came to my mind: why is it (also) called system $F$? Where does the $F$ come from? (i searched it online but didn't get any luck...)
1
vote
0answers
52 views

Proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in $\lambda\pi $ calculus $\equiv$

What is the right representation of the proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in simple type theory as a term of $\lambda\pi $ calculus $\equiv$? Note on notation: The epsilon ...
1
vote
0answers
62 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 ...
1
vote
0answers
86 views

proof checking machine vs. provability checking machine

Let M be a proof-checking Turing machine which takes two inputs, A and B. : M(A,B) = 0 if A codes a valid proof of the sentence coded by B in ZFC. M(A,B) = 1 if A does not code a valid proof of the ...
1
vote
0answers
76 views

Examining every mathematical result in purely formal, ZFC language.

My main interest is physics. However, being self-taught in mathematics for the most part, my proofs tend to be more intuitive than it is acceptable. Yet, I recognize my inaptitude in rigor, and I ...
0
votes
0answers
58 views

A provability puzzle

This is a problem I came up with on my own, and it has me stumped, so I am going to pose it as a kind of puzzle. Let $F$ be a formal proof system, recursively axiomatizable, with an acceptable ...
0
votes
0answers
15 views

Legendre polynomial related simple proof question

Given the set of orthogonal polynomials {Qi(x)}i=0 to n , a polynomial Pn(x) of degree ≤ n, can be written as: Pn(x) = a0*Q0(x) + a1*Q1(x) + · · · + an*Qn(x) for some a0, a1, . . . , an. Please help ...
0
votes
0answers
42 views

Prove that the following Horn satisfiability problem is P-complete

Show that the following Horn satisfiability problem is P-complete: given a set of Horn clauses, is there a variable assignment which satisfies them? This is P's version of the Boolean satisfiability ...
0
votes
0answers
31 views

Proof the Restricted Case of CVP is P-complete

Show that the following Restricted Case of CVP is P-complete: Like CVP, except the input circuit satisfying the following conditions: All gates are placed int layers; the inputs of a gate come from ...
0
votes
0answers
36 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
0answers
42 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} ...
0
votes
0answers
53 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
0answers
31 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
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 ...
0
votes
0answers
30 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 ...
0
votes
0answers
34 views

How Do I Show that Condensed Derivable Rules of Inference Yield the Same Formula as Using Condendensed Detachment Multiple Times?

If we look at condensed detachment of two formulas $\alpha$ and $\beta$, we can see that D$\alpha$.$\beta$, where $\alpha$ has form C$\alpha$$_a$$\alpha$$_b$ is equivalent to using the rule ...
0
votes
0answers
134 views

Proof of law of reflection using Fermat's principle : are we really proving the law of reflection?

Before you skip reading this, let me tell you that this isn't a "how to derive the law of reflection using Fermat's principle" question. Also, I asked it on MSE instead of the physics site because ...
0
votes
0answers
73 views

Proof by contradiction and order of statements

Order matters, take sequences tending towards a limit: $$\forall\epsilon>0\exists N\in\mathbb{N}:n>N\implies|x_n-L|<\epsilon$$ "For all $\epsilon$ there exists an $N$" is totally different to ...