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

6
votes
1answer
80 views

Examples of provably${}^n$ unprovable statements

Given any statement $A$ and a classical theory $T$ which we assume is at least as strong as Peano Arithmetic ($\sf PA$), we have that $T\vdash A$ implies $T\vdash T\vdash A$ (that is, if a statement ...
2
votes
6answers
36 views

Using induction to prove for $n ≥ 1, $ $1 \times 5+2\times6+3\times7 +\cdots +n(n + 4) = \frac 16n(n+1)(2n+13).$

This is a very interesting problem that I came across in an old textbook of mine. So I know its got something to do with mathematical induction, which yields the shortest, simplest proofs, but other ...
3
votes
5answers
158 views

Mathematical Rigor in Proving Limits by $\epsilon-\delta$ Definition

I am trying to find the most mathematically rigorous way to prove limits, using the $\epsilon-\delta$ definition of a limit, so far I have found two clear cut methods of proving limits using the ...
-1
votes
2answers
26 views

How to approach Proofs? [on hold]

I'm currently in a CS course and a big part of it is proving proofs. I am struggling and want to become better. I have always struggled with proofs ever since I first encountered them in highschool - ...
1
vote
1answer
28 views

Completeness theorem for second-order logic in the language $\{\}$

It is well-known that the completeness theorem fails for second-order logic. In particular, there is no calculus $C$ that proves exactly those second-order sentences $\phi$ in the language $\{0, s, +, ...
2
votes
3answers
63 views

Logical limitations of Proofs by Contradiction

In general proofs by contradiction go as follows: Given an arbitrary hypothesis, $\ p \implies q$, we assume $\left(p\implies q\right) = T$, and then we show that by assuming the hypothesis to be ...
2
votes
3answers
44 views

Recursion Proof by Induction

Given: f(1) = 2 f(n) = f(n-1) + 3, for all n>1 It can be evaluated to: ...
3
votes
2answers
426 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
3answers
125 views

On “why” questions in mathematics

In response to the question How would one be able to prove mathematically that $1+1 = 2$?, Asaf Karagila explains: In a more general setting, one needs to remember that $0,1,2,3,…$ are just ...
0
votes
1answer
52 views

Gödel number for contradicting modus ponens?

When Gödel numbered statements, for instance modus ponens and connectives got their own numbers, does it matter which number each connective gets as long as they are different? Sometimes I'm not ...
0
votes
0answers
26 views

What are some active areas of research in proof theory?

Is there any research activity going on in the field of proof theory today? If so, what are some of the most active areas, what types of questions do they deal with, and where can I go to find out ...
1
vote
2answers
40 views

How to prove facts regarding sentential logic

Recently I have been very fascinated by the claim and impact of Godel's incompleteness theorem. To understand the proof given by Godel, I felt the need to read an introductory book in logic to begin ...
2
votes
1answer
71 views

Does PA prove that Con(PA) implies Con(ZF-I) and Con(NFU)?

I read from many sources that PA and ZF-I (a suitable axiomatization of ZF minus Infinity plus its negation) are bi-interpretable, but is PA enough to prove that they are equiconsistent? Specifically ...
2
votes
0answers
23 views

Why don't the quantifiers split in linear logic?

Every presentation of linear logic I've seen seems to either omit or treat quantifiers as an after-thought. Even Girard says that there is "little to say" about them. However, if we view universal ...
0
votes
0answers
21 views

Proof that the union of rational and irrational numbers sets is a set of real numbers [duplicate]

I see it all the time but is there a nice way to show that this is true? Or is this just a definition? I know that $\mathbb{Q} \subset \mathbb{R}$ and $\mathbb{I} \subset \mathbb{R}$, but how do we ...
0
votes
0answers
27 views

Proof tree of $[(\phi\lor \psi)\land (\phi \lor \chi)] \to [\phi \lor (\psi \land \chi)]$

I need to construct a proof tree of: $$[(\phi\lor \psi)\land (\phi \lor \chi)] \to [\phi \lor (\psi \land \chi)]$$ Could someone check the following proof tree? I first proved the following: ...
2
votes
1answer
101 views

Is it possible that Gödel's completeness theorem could fail constructively?

Gödel's completeness theorem says that for any first order theory $F$, the statements derivable from $F$ are precisely those that hold in all models of $F$. Thus, it is not possible to have a theorem ...
2
votes
1answer
38 views

Are there other methods of proof other than contrapositive, induction, contradiction, construction, and counter example?

I have only heard of a few methods of proof, namely, contrapositive, induction, contradiction, construction, and counter example. Are there other types of proofs?
1
vote
0answers
61 views

What is the relationship between Realizability and the Curry-Howard isomorphism?

I have recently been studying the Curry-Howard isomorphism/correspondence. My sources have primarly been Sørensen [1] and Girard [2]. Realizability is introduced here in the form of Kleene's ...
0
votes
3answers
57 views

prove limit of 2-variable using (ε,δ)-definition

I have to prove using (ε,δ)-definition of limit: $$ \lim_{(x,y) \to (0,1)} ye^x = 1 $$ The problem is to work with $$|ye^x-1|$$ and show that that is less than a formula involving δ, let´s call it ...
1
vote
1answer
47 views

Weak Representability and Derivability Condition 1

Can someone point out the error in the following reasoning? Let K be an axiomatizable, consistent extension of Peano Arithmetic. Let P' denote the Gödel number for P. K is axiomatizable, thus ...
0
votes
1answer
17 views

proof by induction of a graph theorem

I would like to proof the following theorem by induction: Theorem: If G is a graph that is not complete, then it is possible to add at least one edge to it. Inductive proof: Base case: Assume we ...
1
vote
1answer
29 views

Proof for: Let A and B be sets s.t $ A \cap B = A $ iff $ A \subseteq B $

I am practicing some proofs involving sets and I would like to see if what I did was a valid proof because it seemed to be different from the one provided in the textbook I am using given that it did ...
2
votes
1answer
93 views

Can we prove that induction is impossible for some proofs?

I read in a book that Andrew Wiles first attempted proof by induction to prove Fermat's last theorem and that he gave up proving it with induction. Instead as far as I understand, Wiles proved some ...
3
votes
3answers
138 views

In which order should I learn the foundations of mathematics? [closed]

I know from Wikipedia that those are the four pillars of the foundations of mathematics: Proof theory Aximatic Set theory Model Theory Recursion Theory and I want to learn all of them, the problem ...
3
votes
0answers
25 views

What to call a term-in-context whose context contains exactly the variables occurring in the term?

In type theory, a term-in-context $\Gamma \vdash t : \tau $ is only well-formed when $\Gamma$ contains all the variables occurring in $t:\tau$. Is there a name for when it contains exactly the ...
0
votes
1answer
61 views

The problem about the Gödel proposition V in 1931 paper?

Proposition V says that every recursive function R can find a relation symbol in system P such that: R(v1, v2....,vn) -> prove(subst( r(u1,u2,...,u3), (z(v1),z(v2),...,z(vn))) ~R(v1, v2....,vn) ...
9
votes
1answer
146 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 ...
35
votes
11answers
3k 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 ...
1
vote
0answers
32 views

Unprovable identity over the integers

I was thinking about Tarski's problem, and was wondering what happens if we have a theory $T$ with two sorts $N,Z$ with intended interpretations $\def\nn{\mathbb{N}}$$\def\zz{\mathbb{Z}}$$\nn,\zz$ ...
0
votes
0answers
67 views

Profane Model Theory, sacred Proof Theory

Dirck van Dalen starts the Preface to his Logic and Structure with the following words: "Logic appears in a ‘sacred’ and in a ‘profane’ form; the sacred form is dominant in proof theory, the ...
0
votes
1answer
44 views

Rules for getting rid of assumptions for certain variables which do not appear in the conclusion of a proof

From my understanding, sometimes in proofs we may 'let' a certain variable be equal to a mathematical object in question for ease of referring to it. Then later on in the conclusion we may substitute ...
2
votes
1answer
47 views

Proof related to pigeon hole principle to be done with induction

since the question is about a positive integer m, it's obvious that the use of mathematical induction needed, but to prove the fact for n = k+1 we have to use the pigeon hole principle, i am so ...
0
votes
0answers
17 views

Show that $σ(i_1, i_2, . . . , i_k)σ^{−1} = (σ(i_1), σ(i_2), . . . , σ(i_k))$

Here's the full question: If $σ ∈ S_n$ is any permutation and $i_1, . . . , i_k $ are $k$ distinct elements of $\{1, . . . , n\}$, show that $σ(i_1, i_2, . . . , i_k)σ^{−1} = (σ(i_1), σ(i_2), . . . , ...
3
votes
2answers
48 views

learning linear algebra [duplicate]

So I'm a college student that has taken 3 semesters of calc/diff eq/linear algebra and I think linear algebra has been by far my favorite course so far and I would love to know more in the subject, ...
0
votes
1answer
63 views

Interpretation help: Showing that Riemann Hypothesis holds “almost surely”

I was perusing this textbook on algorithmic number theory, where I came across this page where they appear to prove that the Riemann Hypothesis holds almost surely. This seems like an odd statement ...
0
votes
0answers
74 views

In what formal proof systems is the deduction theorem taken as a primitive rule of inference?

Wikipedia's article on the deduction theorem states: Although the deduction theorem could be taken as primitive rule of inference in [Hilbert-style] systems, this approach is not generally ...
5
votes
2answers
71 views

Proof by induction, 1 · 1! + 2 · 2! + … + n · n! = (n + 1)! − 1

So I'm supposed to prove that $$1 · 1! + 2 · 2! + \dots + n · n! = (n + 1)! − 1$$ using induction. What I've done Basic Step: Let $n=1$, $$1\cdot1! = 1\cdot1 = 1 = (n+1)!-1 = 2!-1 = 2-1 = 1$$ ...
0
votes
1answer
30 views

Gentzen-style proof system with global states?

I'm sorry if my question looks stupid or does not make sense. However, I want to ask if it is normal/common to have a global state, which is shared by all inference rules, in a Gentzen-style proof ...
3
votes
1answer
70 views

Does no non-standard model of Peano Arithmetic make the integers a principal ideal domain?

Though I do not find a reference now, I have heard no non-standard model of Peano Arithmetic has a principal ideal domain as its ring of integers. Is that right? Is it trivial? Or is there a good ...
7
votes
1answer
1k views

Why can't reachability be expressed in first order logic?

I'm wondering why we can't express graph reachability in first order logic in pretty much exactly the same way we express it in second order existential logic. For SOL, one definition is : 1 . L is ...
0
votes
0answers
45 views

Is there a standard notation for coding finite sets of numbers as numbers?

Hajek and Pudlak Metamathematics of First-Order Arithmetic use the Ackermann encoding of hereditarily finite sets, but they use no notation for codes. They let the reader see from context when a ...
219
votes
15answers
10k 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 ...
38
votes
3answers
4k views

Can proof by contradiction 'fail'?

I am familiar with the mechanism of proof by contradiction: we want to prove $P$, so we assume $¬P$ and prove that this is false; hence $P$ must be true. I have the following devil's advocate ...
0
votes
0answers
11 views

Proving weak simulation

I want to prove something but I am not sure if it is the right way to do it. I have two LTS that define different semantics. A=($Q_a,Λ,\to)$, and B=$(Q_b,Λ\cup\{\beta\},\leadsto)$, where $\beta$ is ...
1
vote
1answer
52 views

HPC: Prove that $\vdash A\to \lnot\lnot A$

Prove that $\vdash A\to \lnot\lnot A$ By Deduction Rule we know that it is sufficient to show that ${A}\vdash \lnot\lnot A$ I am also familiar with the formula: $\lnot A \vdash (A\to B)$. So if ...
1
vote
1answer
83 views

Proof in sequent calculus without cut

I met an exercise in Gaisi Takeuti, Proof Theory [Exercise 2.7, page 14]. How to construct a cut-free proof of$\ \forall xA(x)\rightarrow B\vdash \exists x(A(x)\rightarrow B)$, where A(a) and B are ...
2
votes
1answer
176 views

Sequent calculus - proofs as trees or sequences

First at all, I am new at proof theory, so excuse this perhaps redundant question. I am wondering what is the 'most appropriate' definition of a proof in a sequent calculus (e.g. LK). Proofs as trees ...
0
votes
1answer
55 views

Equivalence rule for sequent calculus

Why are there no inference rules for equivalence (≡ on the right and ≡ on the left) for the sequent calculus, and if there was, how would they look like? e.g. (1) $\cfrac{?}{\Gamma,(A \supset B) ≡ ...
0
votes
0answers
46 views

Prereqisites for: Subsystems of second order arithmetic

As the title suggests, im wondering what the prerequisites for Simpsons book, Subsystems of... are? Unfortunately I cant find it in the preface. My background is a Bachelor in Philosophy and ...