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

0
votes
2answers
31 views

Non model-theoretic, constructive proof that it is valid to introduce new unique constants in a first order theory with equality

I'm currently reading through Mendelson's `Introduction to Mathematical Logic', and one of the proofs has left me dissatisfied. In general, I am fine with seeing metamathematical results proven ...
1
vote
4answers
108 views

natural deduction: introduction of universal quantifier and elimination of existential quantifier explained

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\phi_1,\dots, \phi_n,\phi$ are formulas, then ...
4
votes
1answer
98 views
+50

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
1answer
51 views

What is the intutition behind the negative exponential ? in linear logic?

The positive exponential ! has a very satisfying interpretation in terms of the standard resource interpretation of linear logic. Given a resource $a$, we know that $!a$ means an infinite supply of $a$...
1
vote
2answers
59 views

Basic: Sequent definition, and-introduction, and iff

I am reading through "Mathematical Logic by Ian Chiswell & Wilfred Hodges"(amazon, and publisher) So far have it has covered $\land$-Introduction and $\land$-Elimination Sadly this text only has ...
-5
votes
1answer
52 views

Elementary proof of Fermats Last Theorem [on hold]

Considering the number of possible combinations of 5 pages of elementary algebra, isnt it exceedingly likely that there exists an elementary proof of FLT using only elementary algebra and a couple of ...
0
votes
2answers
47 views

Natural Deducion: assumptions can be used more than once?

Im trying to prove: $ \forall{x}\forall{y}(P(x,y)\rightarrow{}\sim P(y,x)) \vdash \forall{x} \sim P(x,x)$ What i have: $\forall{x}\forall{y}(P(x,y)\rightarrow{}\sim P(y,x))\;$ Premise $ \forall{y}...
3
votes
2answers
27 views

induction proof over graphs

I have a question about how to apply induction proofs over a graph. Let's see for example if I have the following theorem: Proof by induction that if T has n vertices then it has n-1 edges. So what ...
21
votes
5answers
2k views

Is a proof also “evidence”?

Can I use the terms proof and evidence synonymously or is there a difference? You usually see mathematicians writing about "proof" while other sciences instead discuss "evidence" - is there a ...
41
votes
12answers
6k views

Are proofs by contradiction really logical?

Let's say that I prove statement $A$ by showing that the negation of $A$ leads to a contradiction. My question is this: How does one go from "so there's a contradiction if we don't have $A$" to ...
19
votes
6answers
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?
1
vote
1answer
21 views

On proofs by induction

The traditional structure of a proof by induction goes like this: basis: we show that the statement holds for the initial natural number $n$ Inductive step: We show that if the statement holds for $...
2
votes
2answers
61 views

Number of proofs for a statement

On this site, people ask questions and then answers and proofs for those answers come from readers. Readers mark the best answer and then people focus on the next interesting topic. Sometimes, a ...
3
votes
5answers
131 views

Are geometric proofs less reliable than others?

When I submit a homework with a proof that uses a graph, ball, shape etc., most of the time the professors are not happy with them. They respond with a statement like: "The proof you made seems very ...
1
vote
0answers
79 views

easy proof of the completeness theorem [closed]

The completeness theorem of first-order logic states: If $\Phi\models\phi$, then $\Phi\vdash\phi$. Assume that I have a calculus $\vdash$ in mind for which I want to prove this completeness theorem. ...
4
votes
4answers
198 views

Calculus of Natural Deduction That Works for Empty Structures

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\Gamma$ is a set of formulas and $\phi$ a ...
1
vote
2answers
25 views

Set-Theoretic Probability

Consider $\{B_i | i \in I\}$ be a collection of events where $I$ is an arbitrary index set. I would like to show that $$\left(\bigcup_{i \in I} B_i\right)^c = \bigcap_{i \in I} B_i^c.$$ My friend ...
1
vote
2answers
56 views

A question regarding contrapositive for implications

I am slightly confused about the negation for an implication after encountering two questions as follows: "Let P be the statement: If 3 is even, then 6 is even or divisible by 5. Write the negation ...
2
votes
2answers
79 views

Changing Hilbert-style axioms

Consider the following system for Hilbert-style deduction: Axioms: $A \rightarrow (B \rightarrow A)$ $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$ ...
0
votes
1answer
17 views

Proof of the lack of existence of a Hamiltonian Cycle

Consider a graph of $|V| = 2k+1$ vertices with $k+1$ of those vertices having exactly degree $2$ such that none of those degree $2$ vertices are adjacent to each other. I want to go about proving that ...
1
vote
2answers
43 views

How to generalize the principle of mathematical induction for proving statements about more than one natural number?

Suppose that $P(n_1, n_2, \ldots, n_N)$ be a proposition function involving $N >1$ positive integral variables $n_1, n_2, \ldots, n_N$. Then how to generalise the familiar induction to prove this ...
7
votes
4answers
2k 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: ...
2
votes
3answers
43 views

How is the entropy of the normal distribution derived?

Wikipedia says the entropy of the normal distribution is $\frac{1}2 \ln(2\pi e\sigma^2)$ I could not find any proof for that, though. I found some proofs that show that the maximum entropy resembles ...
6
votes
1answer
85 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 ...
3
votes
6answers
54 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
167 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
vote
1answer
31 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
72 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
48 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
440 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
144 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
54 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
30 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
44 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
0answers
25 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
104 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
42 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?
2
votes
0answers
75 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
60 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 g(...
1
vote
1answer
50 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 Thm(k)...
0
votes
1answer
20 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
103 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
155 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
27 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
62 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
147 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 n:0\...