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

0
votes
0answers
19 views

A question about an special kind of proof [on hold]

Is there some proof method in which I can prove the existence of a mathematical object? How can I prove a conjecture that it is an existence statement of a mathematical object? Which are the ...
3
votes
3answers
73 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 ...
1
vote
2answers
260 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 ...
0
votes
2answers
24 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
132 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 ...
4
votes
2answers
41 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$ ...
0
votes
3answers
61 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 ...
3
votes
2answers
103 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 ...
0
votes
1answer
60 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 ...
7
votes
4answers
161 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
-1
votes
3answers
88 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 ...
1
vote
3answers
90 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
1answer
331 views

proof of validity of tautology in first order logic

Every first-order logic formula which has a tautological shape in propositional logic is a valid formula. Will it be possible to give a formal proof for the above ? Thanks and Regards.
2
votes
1answer
43 views

Are there statments which do not have a constructive proof?

I understand that a lot of statements are just non-nonconstructive in nature (like negative statements), and I understand that a lot of statements are not provable without the axiom of choice. ...
7
votes
1answer
155 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 ...
13
votes
7answers
4k views

Difference between “Show” and “Prove”

In many mathematics problems you see the phrase "prove that..." or "show that..." something is. What's the difference between these two phrases? Is "showing" something different from "proving" ...
3
votes
1answer
112 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 ...
1
vote
3answers
76 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 ...
3
votes
2answers
78 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 ...
7
votes
2answers
246 views

Consistency of PA: why other proofs?

Completeness theorem affirms that a formal first order system is consistent iff it has a model. The FOL number theory(PA) or First Order Arithmetic has a model, which is the natural numbers structure. ...
1
vote
0answers
36 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
36 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
102 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 ...
0
votes
4answers
340 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!
1
vote
2answers
133 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
1answer
16 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) - ...
11
votes
7answers
1k views

Why do statements which appear elementary have complicated proofs?

The motivation for this question is : http://math.stackexchange.com/questions/4066/rationals-of-the-form-fracpq-where-p-q-are-primes-in-a-b and some other problems in Mathematics which looks as if ...
0
votes
5answers
88 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 ...
3
votes
5answers
87 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
2answers
40 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
32 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?
9
votes
3answers
333 views

Prove by Hilbert deduction: $\vdash _{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$

I'd really like your help proving: $\vdash_{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$ Where $HFOL$ is the proof system which contains the Hilbert relevant ...
2
votes
2answers
88 views

Want to show the a proof of the sequent $\forall x \forall y R(x,y) \Rightarrow R(y,y)$ must have a cut

Want to show the a proof of the sequent $\forall x \forall y R(x,y) \Rightarrow R(y,y)$ must have a cut. For this question we are in the Gentzen calculus. I am even having trouble just finding a ...
2
votes
1answer
42 views

$LK-\Phi$ proof of $\exists y Pby$

I am having difficulty with the concept of $LK-\Phi$ proofs, here is a question I have been working on: Let $\Phi = \{Pafa\}$, where $P$ is a binary predicate symbol and $f$ is a unary function ...
0
votes
1answer
125 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 ...
4
votes
2answers
76 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 & & ...
3
votes
2answers
89 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 ...
9
votes
1answer
142 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, ...
0
votes
1answer
32 views

Proving that operations give equal results given equal inputs

I was reading about the 9 or 12 basic properties of 'fields' (if that's what they're called) in a book called Spivak's Calculus, 3rd Edition, and got quite befuddled by dealing with as basic stuff as ...
0
votes
1answer
65 views

Hilbert calculus: Proof that every provable formula has a proof

For my indroduction to logic course I have to proof, that every provable formula has a proof. It sounds first very funny, second also very logic, still I don't get to make of formally work.. The ...
7
votes
8answers
2k 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 ...
2
votes
2answers
72 views

Natural Deduction rules for $\lnot$ in classical and intuitionstic logic

Following the very useful answer by Peter Smith to my prevoius post , I'm still reflecting about the "imperfection" connected with the Intro- ans Elim-rules for $\lnot$ in Natural Deduction (I mean ...
3
votes
2answers
61 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 ...
6
votes
3answers
221 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 ...
1
vote
2answers
72 views

A question about consistent fragments of formalized mathematical theories with Natural Deduction

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 ...
1
vote
3answers
138 views

ZFC Axioms to be extended?

Sorry if this is going to be a really loaded question. I was told several times that for virtually all theorems/corollaries/propositions of mathematics (except those cases not compatible with ZFC ...
0
votes
1answer
18 views

Struggling with proof, by contrapositive?

I am having trouble solving this proof. I tried to do a proof by contrapositive. Q = $(u+z)/(v+w) < z/w$ P = $(u/v < x/y \land x/y < z/w)$ Assuming $\lnot Q$ got me: $u/v \ge z/w$ ...