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

1
vote
0answers
22 views

Has the abc conjuncture been proved by Shinichi Mochizuki? [duplicate]

I'd like to know is his proof was reviewed, and what exactly happened.
0
votes
0answers
10 views

Cartesian product proof with counterexample

I was asked to disprove the following statement by counterexample: Let A, B and C be sets. If A x C = B x C then A = B I was under the impression that: (x1, y1) = (x2, y2) if and only if x1 = x2 and ...
0
votes
1answer
14 views

Proving order of magnitude

Generally how much proof must be given to prove a statement of order-of-magnitude? for example: $n^2 + 2 log (n) = O(n^2)$ $2 log (n)$ has a lower order of magnitude than $n^2$ so it can be argued ...
2
votes
2answers
105 views

Is constructive proof of non-existence possible

Constructive proof construct(indicates) object that satisfies given predicate. Question is whether one can give constructive proof of non-existence of an object with given property e.g. that every ...
1
vote
1answer
27 views

Weakening and Contraction

I saw this site saying weakening is a structural rule where the hypotheses or conclusion of a sequent may be extended with additional members and that contraction is a rule where two equal (or ...
0
votes
1answer
50 views

What is really a “complete” deductive system for first-order theories.

Given some first-order language and a set of axioms therefrom one still needs to specify a deductive system to turn it into a full-fledged first-order theory. Currently I'm under the following ...
1
vote
0answers
55 views

Is a sentence in $\Pi_1$ true given $Q \vdash \lnot\varphi$?

If $Q \vdash \lnot\varphi$ (Q is the Robinson arithmetic), and if I assume that $\varphi \in \Pi_1$; Can I say that $\varphi$ is a true sentence? My thoughts are that, given that Q is $\Sigma_1$- ...
1
vote
1answer
68 views

A simple question on Gödel's functional interpretation

I've been recently reading the Gödel's functional interpretation (or Dialectica). It is generally defined inductively, as could be found here: http://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf ...
3
votes
1answer
145 views

Problems with nesting proof predicates in first order logic.

Whenever I start nesting proof predicates, I always seems to run into these bizarre situations. I was wondering if anyone knows about this and could shed some light on it or provide me with some ...
4
votes
2answers
160 views

Is there a minimal axiomatization of ZFC?

Working in ZFC, does there exist a set $\Sigma$ of sentences which axiomatizes ZFC (i.e. every sentence in $\Sigma$ is provable from your favorite axiomatization of ZFC, and vice versa) and is minimal ...
4
votes
1answer
41 views

Sufficient and necessary conditions

Is it correct to say that sufficiency and necessity of a condition is like saying "if and only if"?
7
votes
2answers
161 views

Theorems with one-line proofs [closed]

Inspired by this very concise answer, which proves that $$\sin^2(\theta)+\cos^2(\theta) \equiv 1 $$ as follows: $f(\theta)=\cos^2\theta+\sin^2\theta \quad;$ then it's simple to see that ...
15
votes
16answers
1k 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 ...
8
votes
3answers
135 views

The category of theorems and proofs

On a philosophy website, it said that you could have a category with theorems as objects and proofs as arrows. This sounds awesome, but I couldn't find anything on the web that has both "category" and ...
4
votes
2answers
122 views

What if a conjecture were provably unprovable?

Suppose we found a proof that "The Twin Prime Conjecture cannot be proven", without any conclusion as to the conjecture itself being true or false. Is it then possible for the conjecture to be true? ...
4
votes
1answer
74 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 ...
0
votes
2answers
34 views

Prove that the set $C = \{x \in\Bbb R : ax\le b\}$ is convex

Prove that if a and b are real numbers, then the set $C = \{x \in\Bbb R : ax\le b\}$ is a convex set. My solution so far: To show that a set $C$ is convex it needs to be shown that for for every ...
0
votes
2answers
35 views

Trying to disprove a statement - some partial working included

I am trying to find a counter example to show that the statement below is false, but I am having difficulty in trying to find a reasonable argument. Here is the statement: $n^2-12n + 35 \geq 0$ for ...
1
vote
2answers
92 views

Is it possible to prove that the encoding of existentials in System F is valid?

In Girard's Proofs and Types, under item 11.3.5, second-order existential quantification is encoded in System F using universal quantification as follows: $$ \Sigma X.V \equiv \Pi Y. (\Pi X.(V \to ...
1
vote
0answers
87 views

Do we know that if $\pi$ is normal then there is a proof of it?

We do not know whether $\pi$ is normal or it is not and many other weaker statements, e.g. (*) $\pi$ contains infinitely many $0$s. Inspired by the Godel's incompleteness theorem that there are some ...
2
votes
1answer
136 views

What if 'proof by contradiction' is not a valid method of proof?

I've just been reading this question about the existence (or lack thereof) of contradictions in maths. I've been wondering: What if 'proof by contradiction' is not a valid method to (dis)prove a ...
2
votes
1answer
57 views

Use a proposition to prove another proposition

I'd like to ask for help with an exercise from Solow - How to Read and Do Proofs(3.16). I've tried to get through it but I can't make the proper connection between the two properties. I figured that ...
4
votes
3answers
113 views

Deriving $A \rightarrow ( B \rightarrow C ) \rightarrow ( ( A \rightarrow B ) \rightarrow ( A \rightarrow C ) )$ in the sequent calculus

I need to prove the following theorem: $A\to (B\to C) \to ((A\to B) \to (A\to C))$ using the sequent calculus method. Using the rules: $$ G, A \Rightarrow B,D \over G \Rightarrow A \to B , D ...
0
votes
2answers
34 views

Proof exercise: finding hypothesis and conclusion in a statement

I am starting learn mathematical proofs and I was doing some exercise that needed to identify the hypothesis and the conclusion in a given statement. And I'm having trouble trying to figure it out in ...
1
vote
2answers
155 views

Mathematical statements that cannot be proved or disproved [closed]

I've recently been reading about the continuum hypothesis and am fascinated by the fact that it cannot be proved or disproved, despite the fact that the statement itself is either true or false. What ...
0
votes
3answers
81 views

Proof by contradiction using counterexample

Why can't we use one counter example as the contradiction to the contradicting statement? Example: Let a statement be A where a-->b. We can prove A is not true by finding a counter example. Now, in ...
2
votes
0answers
63 views

Can we always give a direct proof? [duplicate]

This is something I was wondering about for quite a while. Is it possible to construct a statement that can only be proven by using 'proof by contradicition' or contraposition? Or to put it ...
4
votes
2answers
46 views

Biconditional statements with an “easy” direction.

I was reading through Lax's Functional Analysis, when I came across the following statement: Theorem: X is a normed linear space over $\mathbb{R}$, $M$ a bounded subset of $X$. A point $z$ of $X$ ...
-1
votes
3answers
95 views

Examples of revisited proofs after new theorems are discovered… [closed]

Are there any nice examples of "old" complicated proofs that become much simpler after new math is discovered years later? For instance, we know now that Pn+16< Pn+1 occurs infinitely often (where ...
0
votes
1answer
61 views

Existential introduction - required or not?

Consider a theory $T$ in first order logic, and a formula $C$. If there exist a proof of $C$, and that all formulas in $T$ and $C$, none of them contains $\exists$. The question is: does there always ...
9
votes
1answer
182 views

Gödel's way of teaching non-standard models to Takeuti.

In Memoirs of a Proof Theorist, Gaisi Takeuti relates how Gödel taught him about nonstandard models in an "interesting" way: It went as follows. Let T be a theory with a nonstandard model. By ...
0
votes
1answer
56 views

particular property and completeness?

I was puzzeling with the almost standard definition of completeness: In mathematical logic and metalogic, a formal system is called complete with respect to a particular property if every formula ...
1
vote
3answers
91 views

Defining a partial function in a formal theory

Assume we have a first-order theory $T$ of arithmetic (i.e., number theory). Suppose I wish to introduce a new function symbol $f$ in the theory, so that $f$ is a partial number function (namely, it ...
1
vote
3answers
77 views

$\neg(A\Rightarrow B) \iff A\land \neg B$

When considering the question: Rewrite the following using only the symbols $A, B, \lor, \land, \neg$ : $$\neg(A\Rightarrow B)$$ I do not understand how to interpret this and what method to ...
1
vote
0answers
37 views

A question about $KP + V = L$ and $KP$ set theory.

In reading Rathjen (Choice principles in constructive set theories) and Jager (On Feferman's OST) I've come across two facts that are taken as obvious/well known, and probably are, but for which I ...
3
votes
1answer
39 views

$HA^{\omega}$ is a conservative extension of $HA$. But why?

This is definitely a silly question, but I've no one to ask... $HA^{\omega}$ is an extension of $HA$ in all finite types. One can formalize a model of $HA^{\omega}$ in $HA$ using indicies of partial ...
3
votes
2answers
80 views

Idea of a proof by contradicton

Is the idea of a contradiction to prove that the desired conclusion is both true and false or can it be any derived statement that is true and false (not necessarily relating to the conclusion)? Or ...
3
votes
2answers
113 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 ...
1
vote
2answers
135 views

Is there a specific name for a corollary of a conjecture?

How do you call a corollary of a conjecture? Is there a specific name for it? Can it be called simply 'corollary'? Can't it be called 'corollary'? I mean, does the label 'corollary' imply that the ...
0
votes
4answers
359 views

Prove: if x is odd, then sqrt(x) is odd.

If $x$ is odd, then $\sqrt{x}$ is odd, where $x$ is an integer. Any hints welcome and preferred. Thank you!
0
votes
1answer
25 views

Proove that cos(x / 2) + cos(y / 2) - cos(z / 2) = 4 * sin((pi - x) / 4) * sin((pi - y) / 4) * sin ((pi + z) / 4

Help me proove that cos(x / 2) + cos(y / 2) - cos(z / 2) = 4 * sin((pi - x) / 4) * sin((pi - y) / 4) * sin ((pi + z) / 4 where x + y + z = pi I've reached 2 * sin((x + z) / 4) * (cos((x + z) / 4) - ...
0
votes
5answers
89 views

Is proof by algorithm credible?

I have found this question How to prove that the inverse of a matrix is unique? And while the accepted answer is fine I was wondering if it's possible to proof the uniqueness by algorithm. There is ...
0
votes
2answers
42 views

Proving $A+2B+3C+4D < 2.5$ with given conditions

I want to prove follow inequality. Conditions: $$A+B+C+D=1$$ $$A>B>C>D>0$$ Prove: $$A+2B+3C+4D < 2.5$$ Thanks in advance.
0
votes
1answer
35 views

double implication proof

How would I go about said proof: I know how to do it with just a single logical equivalence, but how would I prove a double implication?
3
votes
5answers
95 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 ...
0
votes
1answer
176 views

Formal proofs and Deduction Theorem

In this question i will explain one idea i had about basic formal proofs and the use of Deduction Theorem. I'm considering a formula γ to be a logical consequence of a set A of formulas if and only ...
3
votes
2answers
96 views

Law of excluded middle. Do we need it in proofs?

Quite often when I am making a natural deduction proof, and I have no fixed idea on how to continue. I find myself thinking: "lets start with some form of the law of the excluded middle (LEM) and ...
4
votes
2answers
80 views

Graph that represents logical reasoning

The proof of a statement $X$ in terms of assumptions $A$, $B$ and $C$ can sometimes be represented using a directed graph: $$ \begin{matrix} & & X\\ & \nearrow & & ...
10
votes
1answer
148 views

Can all math results be formalized and checked by a computer?

Can all math results, that have been correctly proven so far, be formalized and checked by a computer? If so, what type of logic would need to be used there? I've heard that the first-order logic is ...
3
votes
2answers
122 views

General view of Theorems

I'm trying to see almost all theorems ( at least the non-existential ones ) as affirming that some formula ( mostly of first-order logic language ) is a logical consequence of other formulas. So, ...