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

184
votes
14answers
7k 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 ...
63
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 ...
109
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 ...
5
votes
4answers
464 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] ...
8
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 ...
14
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 ...
4
votes
1answer
401 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 ...
45
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, ...
31
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 ...
6
votes
4answers
404 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 ...
7
votes
1answer
418 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; ...
5
votes
3answers
611 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 ...
4
votes
3answers
386 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
4answers
544 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: ...
0
votes
2answers
38 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
45 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 ⇒ ...
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 ...
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?
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 ...
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 ...
11
votes
4answers
450 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 ...
8
votes
1answer
166 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
241 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 ...
6
votes
3answers
350 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 ...
5
votes
1answer
240 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
2answers
273 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 ...
3
votes
2answers
136 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 ...
3
votes
3answers
412 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
3answers
350 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 ...
1
vote
2answers
175 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
412 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
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 ...
1
vote
1answer
246 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 ...
8
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 ...
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
3answers
46 views

Proof by Strong Induction for $a_k = 2~a_{k-1} + 3~a_{k-2}$

$$\begin{align} a_0 &= 1 \\ a_1 &= 1 \\ a_k &= 2~a_{k-1} + 3~a_{k-2} \quad \text{ for } k \ge 2 \end{align}$$ Proof by Strong Induction: For all non-negative integers $n$, $a_n$ is an ...
4
votes
2answers
201 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
204 views

Proof that SAT is NPC

I am not really sure I understand the idea behind Cook theorem (it says that SAT is a NP-complete problem). I read the proof with all its parts corresponding to the Turing machine TM solving it (TM ...
3
votes
5answers
121 views

Difference between bound and free variable

What is the difference between $\forall x (P(x)\implies Q(x))$ and $P(x)\implies Q(x)$ I know in the first one the variable x is bound but in the second one the variable is free. What are the ...
3
votes
2answers
407 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
1answer
129 views

Non-self-referential undecidable sentences in arithmetic

Are there any known undecidable sentences for PA are neither "self-referential" (like a sentence equivalent to its own nonprovability) nor imply consistency of PA (like in the Paris Harrington ...
2
votes
1answer
86 views

Proof negation in Gentzen system

I am provided with the L¬ and R¬ Gentzen rules for negation (besides “Cut” rule and some rules for ⋀ and →): $${\Gamma\vdash\Delta,\varphi\over \Gamma,\lnot\varphi\vdash \Delta}\ L\lnot \\[4ex] ...
2
votes
1answer
90 views

Quasi-interactive proof on real numbers

[This is a cleaner and simpler restatement of a question I asked earlier on Theoretical CS forum. Please re-tag as appropriate.] Suppose you have two oracles (black boxes) that represent real ...
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
293 views

Löb's theorem and provability

I learned Löb's theorem. As I understanding, if a statement is formed like "I am provable", the statement should be provable. I want to ask further about Löb's theorem. There is two sentences, P and ...
0
votes
1answer
82 views

How to show the inductive step of the strong induction?

Note: This problem is from Discrete Mathematics and Its Applications [7th ed, prob 2, pg 341]. Problem: Use strong induction to show that all dominoes fall in an infinite arrangement of dominoes if ...
0
votes
3answers
250 views

Using rules of inference (Leibniz) to prove theorems.

Leibniz: If $A \equiv B$ is a theorem, then so is $C[p:= A] \equiv C[p:= B]$. Note: p is "fresh" means p doesn't occur in $A, B, C$. I am trying to understand how to use Leibniz rule of inference for ...