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
175 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
183 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
127 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
73 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
165 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 ...
2
votes
1answer
50 views

Are there statments which do not have a constructive proof?

I understand that a lot of statements are just non-nonconstructive in nature (like negative statements), and I understand that a lot of statements are not provable without the axiom of choice. ...
1
vote
1answer
49 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
33 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
436 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
35 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
35 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
44 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
43 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
39 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
26 views

Proving order of magnitude

Generally how much proof must be given to prove a statement of order-of-magnitude? for example: $n^2 + 2 log (n) = O(n^2)$ $2 log (n)$ has a lower order of magnitude than $n^2$ so it can be argued ...
0
votes
1answer
61 views

particular property and completeness?

I was puzzeling with the almost standard definition of completeness: In mathematical logic and metalogic, a formal system is called complete with respect to a particular property if every formula ...
21
votes
0answers
232 views

When are two proofs “the same”?

Often, we find different proofs for certain theorems that, on the surface, seem to be very different but actually use the same fundamental ideas. For example, the topological proof of the infinitude ...
3
votes
0answers
62 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
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
72 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
244 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
26 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
56 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
103 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
37 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
59 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
74 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
57 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
13 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
20 views

proof calculus in math proofs

Proof theory, is in some way associated with the concept of proofs in mathematics, as proofs of geometric topics, topology, and so on?? And if the three best-known proof calculi (the Hilbert-style ...
0
votes
0answers
40 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
27 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
33 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
41 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
30 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
29 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
30 views

prove corollary to the Universal Non-Euclidean Theorem?

For any line l and any point P not on l, there are infinitely many lines through P parallel to l. In the proof of the theorem, the choice of point X on m uniquely determines the line PS. Show that ...
0
votes
0answers
33 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
108 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
71 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 ...
0
votes
0answers
51 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 ...