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

191
votes
14answers
8k views

Can every proof by contradiction also be shown without contradiction?

Are there some proofs that can only be shown by contradiction or can everything that can be shown by contradiction also be shown without contradiction? What are the advantage/disadvantages of proving ...
111
votes
11answers
12k views

Do we know if there exist true mathematical statements that can not be proven?

Given the set of standard axioms (I'm not asking for proof of those), do we know for sure that a proof exists for all unproven theorems? For example, I believe the Goldbach Conjecture is not proven ...
65
votes
8answers
4k views

Are the “proofs by contradiction” weaker than other proofs?

I remember hearing several times the advice that, we should avoid using a proof by contradiction, if it is simple to convert to a direct proof or a proof by contrapositive. Could you explain the ...
50
votes
8answers
5k views

Is it possible that “A counter-example exists but it cannot be found”

Then otherwise the sentence "It is not possible for someone to find a counter-example" would be a proof. I mean, are there some hypotheses that are false but the counter-example is somewhere we ...
47
votes
13answers
3k views

What is a proof?

I am just a high school student, and I haven't seen much in mathematics (calculus and abstract algebra). Mathematics is a system of axioms which you choose yourself for a set of undefined entities, ...
46
votes
2answers
1k views

Is it possible to prove a mathematical statement by proving that a proof exists?

I'm sure there are easy ways of proving things using, well... any other method besides this! But still, I'm curious to know whether it would be acceptable/if it has been done before?
36
votes
2answers
389 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 ...
35
votes
4answers
2k views

If all sets were finite, how could the real numbers be defined?

An extreme form of constructivism is called finitisim. In this form, unlike the standard axiom system, infinite sets are not allowed. There are important mathematicians, such as Kronecker, who ...
20
votes
3answers
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 ...
18
votes
5answers
2k views

How to prove the mathematical induction is true?

I have no idea about the underlying theory from which the mathematical induction was derived. How to prove the mathematical induction is true?
17
votes
5answers
1k views

If it takes infinite steps to prove a statement, is that a valid proof?

In Cantor's diagonal argument, it takes (countable) infinite steps to construct a number that is different from any numbers in a countable infinite sequence, so in fact the proof takes infinite steps ...
16
votes
4answers
4k views

Why an inconsistent formal system can prove everything?

I am reading a Set Theory book by Kunen. He presents first-order logic and claims that if a set of sentences in inconsistent, then it proves every possible sentence. Since he does not explicitly ...
15
votes
16answers
2k views

Beautiful, simple proofs worthy of writing on this beautiful glass door [closed]

What are some of the more beautiful proofs you know? I am measuring beauty in two dimensions -- first, how conceptually elegant is it and second, how aesthetically pleasing is it. Context: I work ...
15
votes
2answers
275 views

How much math do we need to prove all simple numeric identities?

Consider real numeric expressions build only from integers, operators $+,-,\times,/$ and taking a positive expression to a power (no variables involved), e.g. $$\frac{2}{7},\ 2^{1/2},\ ...
14
votes
7answers
2k views

Why do statements which appear elementary have complicated proofs?

The motivation for this question is : Rationals of the form $\frac{p}{q}$ where $p,q$ are primes in $[a,b]$ and some other problems in Mathematics which looks as if they are elementary but their ...
13
votes
7answers
2k views

Is a counterexample considered a rigorous proof that a property is not true?

This is my follow-up question to my own query earlier: How can I algebraically prove that $2^n - 1$ is not always prime? Almost half of the answers said that I provided my own proof by giving ...
13
votes
7answers
7k views

Difference between “Show” and “Prove”

In many mathematics problems you see the phrase "prove that..." or "show that..." something is. What's the difference between these two phrases? Is "showing" something different from "proving" ...
13
votes
6answers
2k views

Aren't constructive math proofs more “sound”?

Since constructive mathematics allows us to avoid things like Russell's Paradox, then why don't they replace traditional proofs? How do we know the "regular" kind of mathematics are free of paradox ...
13
votes
5answers
230 views

Does “=” have to be interpreted as equality?

To put it briefly: In model theory, we are allowed to interpret any relation symbol in any way we like. So why do people seem to require that "$=$" is interpreted as the actual equality? Let me ...
12
votes
1answer
202 views

Can all math results be formalized and checked by a computer?

Can all math results, that have been correctly proven so far, be formalized and checked by a computer? If so, what type of logic would need to be used there? I've heard that the first-order logic is ...
12
votes
8answers
3k views

Tricks for Constructing Hilbert-Style Proofs

Several times in my studies, I've come across Hilbert-style proof systems for various systems of logic, and when an author says, "Theorem: $\varphi$ is provable in system $\cal H$," or "Theorem: the ...
12
votes
3answers
442 views

On Pudlak's “Life in an Inconsistent World”

In his Logical Foundation of Mathematics and Computational Complexity (2013), Pavel Pudlak invites the readers to ponder about fictitious people whose natural numbers are nonstandard. His exposition ...
12
votes
2answers
277 views

Is it possible to formalize the relationship between different proofs of the same theorem?

Some theorems have many proofs. Examples include the Pythagorean Theorem and the Law of Quadratic Reciprocity. I was wondering if one could formalize the relationship between these proofs. Sure, they ...
12
votes
1answer
1k views

The Power of Lambda Calculi

A simple question here, which likely demands a somewhat complex answer... Or rather, a set of related questions. What are the advantages of typed lambda calculus over untyped lambda calculus in ...
12
votes
1answer
229 views

Unprovable unprovability

In general, mathematical conjectures are resolved by proof, disproof, or proof that they are neither provable nor disprovable. Is it possible that some open conjectures cannot be settled in any of ...
11
votes
2answers
995 views

How to find the shortest proof of a provable theorem?

Roughly speaking, there are some fundamental theorems in mathematics which have several proofs (e.g. Fundamental Theorem of Algebra), some short and some long. It is always an interesting question ...
11
votes
4answers
464 views

Is there a connection between length of sentence and length of proof?

My basic question is: "Do longer tautologies take longer to prove?" But obviously this is underdetermined. If you are allowed an inference rule "Tautological Implication" then any tautology has a 1 ...
11
votes
4answers
458 views

Existence Proofs

This may be a stretch, but are there examples of proofs that prove that a proof exists for a theorem. For example, if A is a theorem, and it is too tedious to prove that, is it possible to show that ...
11
votes
3answers
593 views

Gentzen Cut elimination: Why do we have to “go infinite”?

I found some slides here that say you can't do cut elimination on PA with axioms like $$\frac{P(Z)\;\;\;\;\;\forall n,\,P(n) \implies P(Sn)}{\forall n,\,P(n)}$$ (which denotes infinitely many axioms ...
10
votes
2answers
1k views

Definition of “non-constructive proof”

I was wondering if it is possible to define exactly what a non-constructive (nc) proof is. I have often seen the concept associated with the use of principles such as the axiom of choice or the law of ...
10
votes
2answers
421 views

Minimal difference between classical and intuitionistic sequent calculus

Consider propositional logic with primitive connectives $\{{\to},{\land},{\lor},{\bot}\}$. We view $\neg \varphi$ as an abbreviation of $\varphi\to\bot$ and $\varphi\leftrightarrow\psi$ as an ...
10
votes
0answers
181 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 ...
9
votes
5answers
2k views

List of Mathematical Impossibilities proved using special tools

It is always weird to see a proof that something is impossible, especially when the tools used in the proof have nothing to do(at a first sight) with the original statement of the problem. I know a ...
9
votes
3answers
118 views

role of definitions in proofs

Definitions are needed to define objects and such, however I am confused as to where definitions come from. I feel that they cannot be something that we arbitrarily define because simply saying ...
9
votes
3answers
173 views

The category of theorems and proofs

On a philosophy website, it said that you could have a category with theorems as objects and proofs as arrows. This sounds awesome, but I couldn't find anything on the web that has both "category" and ...
9
votes
2answers
663 views

Who stole the axioms in Natural Deduction?

The study of Gentzen's sequent calculus give me the opportunity to propose some reflections about the concept of logical truth. I'll refer to the english edition of Gentzen's works : The collected ...
9
votes
1answer
226 views

Gödel's way of teaching non-standard models to Takeuti.

In Memoirs of a Proof Theorist, Gaisi Takeuti relates how Gödel taught him about nonstandard models in an "interesting" way: It went as follows. Let T be a theory with a nonstandard model. By ...
9
votes
3answers
393 views

Prove by Hilbert deduction: $\vdash _{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$

I'd really like your help proving: $\vdash_{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$ Where $HFOL$ is the proof system which contains the Hilbert relevant ...
9
votes
1answer
456 views

Packing boxes and proof of Riemann Hypothesis

From Scott Aaronson's blog: There’s a finite (and not unimaginably-large) set of boxes, such that if we knew how to pack those boxes into the trunk of your car, then we’d also know a proof ...
9
votes
2answers
2k views

How can I learn about proofs for computer science?

I study computer science at a university. My school offers several courses where various proofs are expected, but there is no course that introduces the fundamental concepts of proofs and how to write ...
8
votes
1answer
340 views

Are the Godel's incompleteness theorems valid for both classical and intuitionistic logic?

I am studying an undergraduate text about math logic. The proofs of the two Godel's incompleteness theorems are not completely formal: they are admittedly simpler that the real proofs. For what I ...
8
votes
1answer
179 views

Can all theorems of $\sf ZFC$ about the natural numbers be proven in $\sf ZF$?

I know a proof of Hindman's theorem that uses ultrafilters on the natural numbers, and ultimately, the axiom of choice. But the theorem itself is essentially a combinatorial property of the natural ...
8
votes
4answers
310 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
8
votes
1answer
300 views

Why wouldn't someone accept Gentzen's consistency proof?

Reading the consistency section of the Peano Axioms wikipedia page, I came across this sentence: The vast majority of contemporary mathematicians believe that Peano's axioms are consistent, ...
8
votes
1answer
369 views

Intutive explanation of the PCP Theorem

The PCP theorem states that: Every decision problem in NP has probabilistically checkable proofs of constant query complexity and logarithmic randomness complexity. Can anyone give an ...
8
votes
1answer
243 views

Reverse Mathematics of Well-Orderings

In Simpson's book, a well-ordered set $X$ is a linear ordering such that there are no functions $f : \mathbb{N} \rightarrow X$ which is decreasing. However, a familiar definition of well-ordering is ...
8
votes
1answer
246 views

On the existence of closed form solutions to finite combinatorial problems

Is it possible that a finite combinatorial problem may admit a closed form solution, and for it to be impossible in practice to prove the validity of this solution? I'm not sure if a rigorous ...
8
votes
1answer
120 views

Is there a way to tell how many different ways you can prove a theorem?

Consider the question. Given the nature of a sentence $S$, it there any way to tell how many different ways you can prove this sentence? Proofs are not distinct if we have a situation such as: $P ...
8
votes
1answer
171 views

Proof-theoretic characterization of the primitive recursive functions?

The total recursive functions are exactly those number-theoretic functions that can be represented by a $\Sigma_1$ formula of first-order arithmetic. Is there a similar characterization of the ...
7
votes
3answers
486 views

Why are $\Delta_1$ sentences of arithmetic called recursive?

The arithmetic hierarchy defines the $\Pi_1$ formulae of arithmetic to be formulae that are provably equivalent to a formula in prenex normal form that only has universal quantifiers, and $\Sigma_1$ ...