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
2answers
143 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
5answers
597 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
37 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
96 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
44 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
62 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
121 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
332 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
176 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
93 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 & & ...
12
votes
1answer
180 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
130 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, ...
1
vote
1answer
121 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 ...
0
votes
1answer
34 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 ...
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 ...
2
votes
1answer
50 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. ...
0
votes
1answer
22 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$ ...
1
vote
3answers
174 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 ...
2
votes
1answer
168 views

Provable formulas in everyday Mathematics

Basically all statements ( lemmas, theoremas, corollaries ) in Mathematics can be expressed as a conditional statement in first-order language, or existential statement ( existence proofs ). Here ...
4
votes
2answers
201 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
2answers
49 views

How to quantify this statement

How do I quantify this statement? Let $x \in \mathbb{R}$. $1 \le x \le 2$ if and only if $1 \le x \le 1+ 1/n$ for some $n \in \mathbb{N}$. When I am trying to prove this, I am led (in the course of ...
1
vote
1answer
44 views

The approximation rule implies the equality rule in systems of type assignments

I'm reading Barendregt's Lambda calculi with types (1992). In Proposition 4.1.4.1., he "proves" a lemma which shows the approximation rule implies the equality rule in typed lambda-calculi à la ...
0
votes
0answers
71 views

Proof by contradiction and order of statements

Order matters, take sequences tending towards a limit: $$\forall\epsilon>0\exists N\in\mathbb{N}:n>N\implies|x_n-L|<\epsilon$$ "For all $\epsilon$ there exists an $N$" is totally different to ...
50
votes
8answers
5k views

Is it possible that “A counter-example exists but it cannot be found”

Then otherwise the sentence "It is not possible for someone to find a counter-example" would be a proof. I mean, are there some hypotheses that are false but the counter-example is somewhere we ...
1
vote
4answers
69 views

Show that if $3\mid(a^2+1)$ then $3$ does not divide $(a+1)$.

Show that if $3\mid(a^2+1)$ then $3$ does not divide $(a+1)$. using proof of contradiction can someone prove this using contradiction method please
1
vote
2answers
109 views

Does generalization of axioms apply also to theorems?

In Enderton's book "A Mathematical Introduction to Logic" (second edition), he includes six axiom groups, and allows also for a generalization of those axioms such that if $\Psi$ is an axiom then ...
3
votes
4answers
93 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 ...
3
votes
1answer
84 views

Intuitionistic Linear Logic

I am currently going through some papers that use the "intuitionistic version" of Girard's Linear Logic. Problem is, i seem to find very little literature on it. There is a lot done on Linear Logic ...
0
votes
2answers
67 views

assuming the conclusion

A natural deduction proof goes from premmisses to conclusion, and under normal circumstances you will not assume the conclusion. Sometimes you may assume the negation of the conclusion and do some ...
3
votes
2answers
136 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 ...
8
votes
1answer
166 views

Can all theorems of $\sf ZFC$ about the natural numbers be proven in $\sf ZF$?

I know a proof of Hindman's theorem that uses ultrafilters on the natural numbers, and ultimately, the axiom of choice. But the theorem itself is essentially a combinatorial property of the natural ...
2
votes
1answer
86 views

Proof negation in Gentzen system

I am provided with the L¬ and R¬ Gentzen rules for negation (besides “Cut” rule and some rules for ⋀ and →): $${\Gamma\vdash\Delta,\varphi\over \Gamma,\lnot\varphi\vdash \Delta}\ L\lnot \\[4ex] ...
1
vote
1answer
70 views

If $\phi$ is $\Delta^{0}_{1}$ in the language of arithmetic, does Heyting Arithmetic prove $\forall x [\phi (x) \vee \neg \phi (x)]$?

PA is conservative over HA for $\Pi^{0}_{2}$ sentences. If $\phi$ is $\Delta^{0}_{1}$, then $\forall x [\phi (x) \vee \neg \phi (x)]$ is equivalent to a $\Pi^{0}_{2}$ sentence. Since PA trivially ...
1
vote
1answer
69 views

Infinitely many proofs?

While compiling a list of my favorite proofs of the infinitude of primes, the following came to mind; Proposition: There are infinitely many non-isomorphic proofs of the infinitude of primes. I'm ...
2
votes
1answer
84 views

Does second-order arithmetic (Z2) prove soundness and uniform reflection for first-order arithmetic (PA)?

(1) Does full second-order arithmetic (Z2) prove soundness and uniform reflection schemas for first-order arithmetic (PA)? That is, do we have for all formulas $\phi$: $$ \underset \phi \forall \; ...
4
votes
1answer
183 views

What are those “things that cannot be proved using only ordinary rules of inference”?

The online edition of the book Introduction to Logic by Michael Genesereth and Eric Kao, has a detail that left me confused. CHAPTER 4 [...] 4.2 Linear Proofs [...] The ...
1
vote
1answer
45 views

Probability of 2 identical events

My professor said that probability of 2 identical events in a very short amount of time (dt converges to 0) is 0. However, I did not agree with him about this. Is there a proof for that assertion? ...
6
votes
3answers
352 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
1answer
44 views

Introduction to functional interpretations

Any good recomendations for an introduction to functional interpretations? I understand this is a little vague but i haven't had much contact with the area. I am particularly interested in the ...
0
votes
1answer
59 views

Help with positive- and negative-forms in Proof Theory

I need help in understanding a device used bu Kurt Schütte, Proof Theory (1977). In treating classical sentential calculus, he use - in place of truth-tables - the device of positive- and ...
2
votes
2answers
124 views

Proof for $\{p,p\rightarrow (q\rightarrow r)\}\vdash (p\rightarrow q)\rightarrow r$ in HR

I can't find a for $\{p,p\rightarrow (q\rightarrow r)\}\vdash (p\rightarrow q)\rightarrow r$ in HR HR is the following system: axioms: $A\rightarrow A$ $(A\rightarrow B)\rightarrow ((B\rightarrow ...
8
votes
2answers
555 views

Who stole the axioms in Natural Deduction?

The study of Gentzen's sequent calculus give me the opportunity to propose some reflections about the concept of logical truth. I'll refer to the english edition of Gentzen's works : The collected ...
1
vote
0answers
37 views

Girard's System $F$ (also named Polymorphism)

I have been studying Girard's Polymorphism and a question came to my mind: why is it (also) called system $F$? Where does the $F$ come from? (i searched it online but didn't get any luck...)
12
votes
3answers
417 views

On Pudlak's “Life in an Inconsistent World”

In his Logical Foundation of Mathematics and Computational Complexity (2013), Pavel Pudlak invites the readers to ponder about fictitious people whose natural numbers are nonstandard. His exposition ...
1
vote
1answer
60 views

Enumeration of proofs

Is it possible to enumerate short proofs of short statements, so as to make sure that, say, Goldbach's conjecture doesn't have one of those? How hard would it be? Is it being done? It's seems likely ...
1
vote
1answer
97 views

“Measure” of induction for cut-elimination in sequent calculus

I'm not very familiar with proof thoery, so I'm in trouble understanding different versions of the proof of the Cut-elimination Theorem for sequent calculus. In Sara Negri & Jan von Plato, ...
0
votes
0answers
51 views

Proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in $\lambda\pi $ calculus $\equiv$

What is the right representation of the proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in simple type theory as a term of $\lambda\pi $ calculus $\equiv$? Note on notation: The epsilon ...
1
vote
2answers
71 views

Restrictive Rules for LK System

I have a question regarding the restrictive nature of $\forall(R)$ and $\exists(L)$ rules in sequent calculus LK. I don't really understand why the restrictions exists in the first place, so why: $$ ...
3
votes
1answer
81 views

A problem about sequent calculus for classical logic

In Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 51, various properties of the system G3cp of classical propositional logic are showed. Theorem 3.1.1 [page 49] proves that all ...
7
votes
1answer
144 views

Proof-theoretic characterization of the primitive recursive functions?

The total recursive functions are exactly those number-theoretic functions that can be represented by a $\Sigma_1$ formula of first-order arithmetic. Is there a similar characterization of the ...