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

202
votes
14answers
9k 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 ...
74
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 ...
118
votes
11answers
13k 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 ...
6
votes
4answers
611 views

What is the “correct” reading of $\bot$?

I have some doubts about the "natural" interpretation of $\bot$ in Natural Deduction and sequent calculus. In Prawitz (1965) $\bot$ (falsehood or absurdity) is called a sentential constant [page 14] ...
12
votes
8answers
4k 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 ...
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 ...
48
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, ...
5
votes
3answers
417 views

Aftermath of the incompletness theorem proof

This is somewhat of a minor point about the incompletness theorem, but I'm always a little unsure: So one proves that there is a formula which is unprovable in the theory of consideration. Okay, at ...
4
votes
1answer
435 views

Can it be shown that ZFC has statements which cannot be proven to be independent, but are?

I am familiar with the concept that a statement can be proven indepent such as in the case of the continuum hypothesis where both ZFC+CH and ZFC+(CH is false) are both proven consistent, but I would ...
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 ...
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 ...
19
votes
5answers
3k 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?
10
votes
2answers
2k 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 ...
6
votes
4answers
429 views

Are there “essentially non-constructive” statements?

There exist constructive and non-constructive proofs. Sometimes, for a mathematical statement, we can have both non-constructive and a constructive proof. However, are there statements for which ...
5
votes
3answers
729 views

Is the negation of the Gödel sentence always unprovable too?

The incompleteness theorem says that certain theories+deduction system contain at least one sentence (the Gödel sentence "$G$"), which can't be proven (in the system in which it holds). (i) Is ...
7
votes
1answer
448 views

Can Robinson's Q prove Presburger arithmetic consistent?

I made an assertion in What are some examples of theories stronger than Presburger Arithmetic but weaker than Peano Arithmetic? that Q has higher consistency strength than Pres, Presburger arithmetic; ...
6
votes
4answers
1k views

What is the difference between ⊢ and ⊨?

I want to know the difference between ⊢ and ⊨. http://en.wikipedia.org/wiki/List_of_logic_symbols ⊢ means ”provable” But ⊨ is used exactly the same: ...
1
vote
2answers
2k views

Prove that if a|b and b|c then a|c using a column proof that has steps in the first column and the reason for the step in the second column.

Let $a$, $b$, and $c$ be integers, where a $\ne$ 0. Then $$ $$ (i) if $a$ | $b$ and $a$ | $c$, then $a$ | ($b+c$) $$ $$ (ii) if $a$ | $b$ and $a$|$bc$ for all integers $c$; $$ $$ (iii) if $a$ |$b$ and ...
0
votes
1answer
43 views

How to show that the displaying numbers of a onto function is k!S(n,k)?

Let it be $A$,$B$ sets that $|A|$=$n$, $|B|$=$k$ and $|A|>|B|$. How to show that the displaying numbers of an onto function $f$:$A$ $\rightarrow$ $B$ is: $\begin{Bmatrix} n \\ k\end{Bmatrix}$$k!$ ...
0
votes
4answers
79 views

Proving that $x^2 + 4$ is not divisible by $3$

I need to show the following: For any integer $x$, $x^2 + 4$ is not divisible by $3$. I was trying proof by contraposition, but I do not believe that is the most efficient way to go about this. ...
0
votes
2answers
44 views

How do I complete a proof with intersection and complements?

For all sets $A$ and $B$, $(A \cap B)^c = A^c \cup B^c$ I am confused how complements play a role in the proof. Can somebody explain that please. Thank you!
0
votes
1answer
52 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 ⇒ ...
33
votes
11answers
2k views

What is exactly the difference between a definition and an axiom?

I am wondering what the difference between a definition and an axiom. Isn't an axiom something what we define to be true? For example, one of the axioms of Peano Arithmetic states that $\forall ...
34
votes
2answers
409 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 ...
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
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 ...
11
votes
2answers
495 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 ...
13
votes
3answers
458 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
1k 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
468 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 ...
18
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 ...
8
votes
1answer
197 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
1answer
258 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 ...
5
votes
1answer
244 views

What are various proofs good for?

There are plenty of questions around here, which are proven to be right or wrong in various ways. I wonder, what one can learn from these differing ways of how to prove something, despite the fact ...
6
votes
3answers
592 views

Give a proof that “p & ~p” implies “q”?

Context: This is not a textbook or homework problem. I was hoping you younger folks could help my tired old brain. "Everybody knows" a contradiction implies anything. What I'm looking for is a ...
6
votes
2answers
278 views

Ideas about Proofs

If there are two different proofs for one theorem, at some level are the two proofs the same, or can they be fundamentally different? In other words, if you have two proofs of a theorem, can one show ...
4
votes
3answers
598 views

What do we mean by an “Elegant Proof”? [closed]

What do we mean when we say that a mathematical proof is elegant? Of course one can say that the proof is beautiful, but what do we precisely mean when we say that a proof is beautiful ? Is there a ...
3
votes
2answers
225 views

Double Negation is sequent calculus systems LK and LJ

In sequent calculus LK (see Gaisi Takeuti, Proof Theory (2nd ed - 1987)) we have a "standard" derivation of Double Negation in the form $\rightarrow \lnot \lnot A \supset A$. We have to start from an ...
1
vote
1answer
254 views

Complexity of verifying proofs

My question can be read on many levels and so I welcome answers to any reading. The general question is: What is the computational complexity of verifying a proof? One way of looking at a ...
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?
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
2answers
322 views

Model-theory and Proof-theory in Propositional Logic

I'm trying to link results of model theory and proof-theory in propositional language. Here i will use $\models$ to denote logical consequence, in the model-theory sense. Being $x,y$ two formulas of ...
3
votes
2answers
566 views

How to prove consistency of Natural Deduction systems

In Dag Prawitz, Natural Deduction A Proof-Theoretical Study (1965), we have the system I of intuitionistic (first-order) logic based on eleven introduction- and elimination-rules : the 3 couples for ...
3
votes
3answers
402 views

Impossibility theorems

I've been wondering how you go about proving an impossibility e.g. when I looked up Abel's impossibility theorem it says nothing about the proof and only restates the theorem when I'd like to know how ...
2
votes
4answers
270 views

How do I know which of these are mathematical statements?

While reading this book called "How to Read and do Proofs" by Daniel Solow(Google) I found the following exercise at the end of the first chapter. So how do I know if something is a mathematical ...
1
vote
1answer
25 views

If a set $S$ is inconsistent, does $S\vdash \alpha$ for all $\alpha$ in this system?

Let $S$ be an inconsistent set of propositional formulas. If our system consists of the axioms: \begin{align} AX1&\quad (P\implies (Q \implies P))\\ AX2&\quad (((P\implies(Q\implies ...
1
vote
2answers
203 views

Simple proof theory - Propositional Logic

When addressing the questions, which are featured below, I use the following definition and two lemmas. Definition: $\phi$ is a tautology if $[[\phi]]_{v}=1$ for all valuations $v$. Moreover, ...
1
vote
2answers
596 views

Axiom Systems and Formal Systems

I'm a really beginner in Mathematical Logic.I'm currently reading Shoenfield Mathematical's Logic and i'm having a hard time trying to relate the concept of Formal Systems with the concept of Axiom ...
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 ...
7
votes
1answer
168 views

Learning how to prove that a function can't proved total?

In proof-theory one can prove that in, say, Peano Arithmetic one can't prove a function $f$ total. Often this seems to mean $f$ is growing too fast to be provably total. I have some background in ...