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

learn more… | top users | synonyms

5
votes
1answer
206 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
237 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
156 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
71 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
81 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
531 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.
1
vote
1answer
25 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
143 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
44 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
72 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 ...
10
votes
0answers
213 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 ...
5
votes
0answers
72 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 ...
3
votes
0answers
18 views

Looking for references for learning the words and sentences used in proofs

I'm familiar with textbooks on logic, proof techniques, and sets. But I have yet to encounter a textbook that dives into the language used w/ definitions and sentence structure used in proofs, for ...
3
votes
0answers
50 views

Can every mathematical proof be seen as the verification of some algorithm's action?

Put another way: Can every mathematical proof be reformulated to be about some class of Turing Machines? Example Any proof of the existence of infinite prime numbers is equivalent to the statement: ...
3
votes
0answers
73 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
82 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 ...
3
votes
0answers
385 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 ...
2
votes
0answers
49 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" ...
2
votes
0answers
44 views

Clever proofs that prove one identity is equal to another, without going through the original identity?

In a previous question I attempted to formalize the argument of going from one proof of an identity to another, which turned out to be harder than I thought. The thing is, while it may be impossible ...
2
votes
0answers
35 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 & = ...
2
votes
0answers
58 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
90 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 ...
1
vote
0answers
22 views

Is there a consistent arithmetically definable extension of PA that proves its own consistency?

Gödel's second incompleteness applies, for instance, to r.e. extensions of PA. I am wondering if it applies more generally to arithmetically definable extensions of PA. I see that there is a complete ...
1
vote
0answers
34 views

Soundness of Propositional Logic proof.

Let $$\begin{align} A1&=(p\implies (q\implies p)) \\ A2&=(((p\implies (q \implies r)) \implies ((p\implies q)\implies (p\implies r))) \\ A3&=((\neg p \implies \neg q ) \implies ((\neg p ...
1
vote
0answers
19 views

Logic behind an IFF statement

If we have an iff statement such as: $A$ iff $B$, to show $A \Rightarrow B$ is it enough to show that not $B \Rightarrow$ not A?
1
vote
0answers
52 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
32 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
66 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
23 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
62 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
112 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
46 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
47 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

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
88 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
81 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
54 views

Is my proof of the Division Algorithm 'enough'?

Recently when learning number theory I was introduced to the proof of the division algorithm, it can be found here http://www.oxfordmathcenter.com/drupal7/node/479. However, I decided to prove it ...
0
votes
0answers
23 views

What is this P4 correspond to in proposition as types?

I was reading "Proofs and Types", so there came across that any proposition can be converted to lambda form. So was trying out with Hilbert system's axioms P1. $A \rightarrow A $ P2. $A \rightarrow ...
0
votes
0answers
45 views

Euler - Lagrange Equations proof

I have been searching on the internet about Euler - Lagrange Equations and I didn't find anywhere the proof for Euler - Lagrange Equations. I need to find a proof for this equations. From where can I ...
0
votes
0answers
42 views

Pythagorian theorem in language of Hilbert's system of geometry

How can one formulate the Pythagorian theorem in the language of Hilbert's system of geometry? How can one speak about the length of the hypotenuse for example?
0
votes
0answers
49 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 ...
0
votes
0answers
30 views

Is it always possible to algebraically express a function defined by a set of rules?

Let's say you have an arbitrary function defined by a set of rules such that for example: Domain $\hspace{9mm}$ Range $\hspace{5mm}$ 1 $\hspace{23mm}$ 2 $\hspace{5mm}$ 2 $\hspace{23mm}$ 2 ...
0
votes
0answers
69 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
63 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
39 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
95 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
22 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
62 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
111 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 ...
-1
votes
0answers
23 views

What does meant “Uncounditional proof” and why should believe it that is a complet proof?

I have tried many times to understand what it does meant "Uncounditionally proof" but i don't succed , only I think that is the proof which produced from Insufficient conditions and and havn't enough ...