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

4
votes
0answers
78 views

Are there any proofs that only exist by induction?

I've come to learn more about induction recently for proving things, and one thing stands out to me. It seems like you could just data-mine patterns and guess a relationship you think might be ...
-4
votes
1answer
62 views

help in real analysis [on hold]

How can I use this definition to prove that $a^{\frac{1}{n}}$ converge to $1$? where a >0
2
votes
2answers
79 views

What kind of proof is this? - Examining all the possibilities.

To prove the following : If $f : X \rightarrow Y$ is a measurable function, and $E$ is a Borel set, then $f^{-1} (E)$ is a measurable set. Prove) First, define $\Omega$ a collection of all $E \subset ...
2
votes
2answers
81 views

Are theorems like subroutines for math? [closed]

I've been developing more appetite for math just lately, as I study electromagnetics to deepen my understanding of electric circuits and devices. I'm finding that doing derivations as exercises helps ...
5
votes
2answers
96 views

Meta proof-searching

Suppose you have a particular theory (ex: $ZFC$) in which you want to prove a statement $\phi$. One can attempt to find a proof of $\phi$ that can be verified, but another tactic can be to find a ...
1
vote
1answer
26 views

Sequents: if-introduction and discharging assumptions

I am reading through "Mathematical Logic by Ian Chiswell & Wilfred Hodges"(amazon, and publisher) for context I am reading through this for self-study, so I don't have the normal support of a ...
1
vote
1answer
48 views

How do I prove this derivation of a definite integral?

Q,How to prove that $\int_{0 }^{\Pi /2}\sin ^{m}x \cos ^{n}x dx =\left [{(m-1)(m-3)(m-5)...2 or 1}\right ]\left [ \left ( n-1)\left ( n-3 \right )..2 or 1 \right ) \right ]\div \left [ \left ( m+n)(...
0
votes
4answers
50 views

How can be proven that any number X is greater,lesser or equal to any other number Y?

I have looked for it on the internet, really, but all I have found are particular cases like 1 > 0, or such. Is there an algebraic proof for proving that x > y or, x = y, or x < y? I thought of ...
1
vote
1answer
63 views

Battle between Intuition and Rigor in Mathematics in the Context of Computers [closed]

I understand the reason behind the inclusion of rigor in mathematics: to ensure that all new theorems, axioms, and postulates are 100% correct. However, with the advent of computer simulations and so ...
2
votes
2answers
28 views

Isn't it problematic to cite the Gödel sentence as a proposition asserting 'This sentence is unprovable' since it isn't really on point?

In the proof of Gödel's incompleteness theorem the Diagonalization Lemma is applied to the negated provability predicate $¬Prov_F(x)$: this gives a sentence $G_F$ such that $F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉) $...
0
votes
2answers
41 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 ...
-5
votes
1answer
59 views

Elementary proof of Fermats Last Theorem [closed]

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 ...
1
vote
2answers
65 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 ...
0
votes
2answers
48 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}...
2
votes
1answer
54 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$...
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 ...
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 $...
21
votes
5answers
3k 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 ...
1
vote
0answers
85 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
201 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
4answers
111 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 ...
1
vote
2answers
26 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
58 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 ...
0
votes
1answer
19 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 ...
2
votes
2answers
82 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))$ ...
1
vote
2answers
45 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 ...
2
votes
3answers
50 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 ...
3
votes
6answers
55 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 ...
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
50 views

Recursion Proof by Induction

Given: f(1) = 2 f(n) = f(n-1) + 3, for all n>1 It can be evaluated to: ...
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 ...
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
31 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
49 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 ...
3
votes
3answers
146 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 ...
2
votes
0answers
26 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: $$\...
4
votes
1answer
117 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 ...
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 ...
2
votes
1answer
105 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
44 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
78 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
1answer
23 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 ...
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
52 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)...
3
votes
3answers
160 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
68 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) ->...