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
130 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
254 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
209 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
137 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
87 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
72 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 ...
3
votes
1answer
121 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
252 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
79 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? ...
2
votes
1answer
52 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
71 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 negative-...
2
votes
2answers
132 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 ...
10
votes
2answers
937 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 ...
2
votes
0answers
57 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...)
13
votes
3answers
476 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 ...
2
votes
1answer
103 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
127 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, ...
1
vote
0answers
65 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
86 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
117 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 ...
9
votes
1answer
220 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 ...
0
votes
1answer
68 views

Proofs with binary trees [duplicate]

Now I have a binary tree which is How would I go about proving binary tree with $n$ leaves has exactly $2 n - 1$ nodes ?
0
votes
2answers
78 views

Unique set of inference rules for a deductive system?

I have the impression that for a deduction system there are many sets of inference rules to describe it. Simple example, the inference rules for (classical or intuitionistic, this is not the matter) ...
0
votes
1answer
88 views

Is this deduction in normal form?

Definition: A deduction is in normal form if there is no formula which is a conclusion of an introduction rule and the main premise of the elimination rule of the same connective. So, in a natural ...
2
votes
2answers
123 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 ...
2
votes
2answers
58 views

On provability within minimal logic

In its most naive form my question boils down to this: when is a proposition that is provable "by contradiction" also provable "directly"? IOW, is it possible to know, a priori, that a ...
0
votes
3answers
551 views

Using rules of inference (Leibniz) to prove theorems.

Leibniz: If $A \equiv B$ is a theorem, then so is $C[p:= A] \equiv C[p:= B]$. Note: p is "fresh" means p doesn't occur in $A, B, C$. I am trying to understand how to use Leibniz rule of inference for ...
6
votes
4answers
659 views

What is the “correct” reading of $\bot$?

I have some doubts about the "natural" interpretation of $\bot$ in Natural Deduction and sequent calculus. In Prawitz (1965) $\bot$ (falsehood or absurdity) is called a sentential constant [page 14] ...
1
vote
2answers
107 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 ...
3
votes
2answers
612 views

How to prove consistency of Natural Deduction systems

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
2answers
537 views

What are some good introductory books on mathematical proofs?

There was a time when I avoided math proofs, but now I am starting to enjoy them. I am taking Intro to Linear Algebra and am falling in love with proofs. Are there any introduction to mathematical ...
3
votes
1answer
69 views

Using an automatic tool for checking geometric conjectures

I do a lot of research about squares, and I thought of using some automatic tool for proving / disproving some geometric conjectures. As a simple example, consider the following Square coloring ...
0
votes
1answer
82 views

Prove by Hilbert deduction: ⊢∃x(AvB)→(∃xAv∃xB); ⊢(∃xAv∃xB)→∃x(AvB)

I'd really like your help proving: 1)⊢∃x(AvB)→(∃xAv∃xB) 2)⊢(∃xAv∃xB)→∃x(AvB) Our proof system contains next Hilbert's axioms: 1.A→(B→A) 2.(A→B)→((A→(B→X))→(A→X)) 3.(A&B)→A 4.(A&B)→B 5.(...
3
votes
1answer
156 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 theorem)...
1
vote
2answers
118 views

Probabilistic “proof” that a sentence is provable (proof “density”).

Is it possible to (or even useful) to calculate the probability that a certain statement is provable? I had this idea that any two statements say A and B could be compared to each other by comparing ...
122
votes
11answers
13k views

Do we know if there exist true mathematical statements that can not be proven?

Given the set of standard axioms (I'm not asking for proof of those), do we know for sure that a proof exists for all unproven theorems? For example, I believe the Goldbach Conjecture is not proven ...
3
votes
0answers
90 views

What is the proof-theoretic strength of the predicative second-order theory of real numbers?

The first-order theory of real numbers, AKA the theory of real closed fields, is obtained by added to the axioms for ordered fields an axiom schema of completeness, which states that for each formula $...
4
votes
2answers
193 views

About theorem's proof length in propositional calculus

In PC(propositional calculus) system, how long will a formula's proof be? That is to say if there exists a computable function $f$ such that for any formula $A$, if $\vdash_{\mathrm{PC}}A$ then $A$ ...
0
votes
1answer
93 views

Is it possible to prove $p\rightarrow\diamond (p\land q)$ in modal logic?

I need to prove $p\rightarrow\diamond (p\land q)$ in B axiomatic, which contains next conversion rules: 1.$(p\land q)\rightarrow(q\land p)$ 2.$(q\land p)\rightarrow p$ 3.$p\rightarrow(p\land p)$ 4.$p\...
9
votes
4answers
351 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 ...
0
votes
2answers
60 views

Why this first-order logic formula is not correct?

I'm studing computer science at university, in specific Artificial Intelligence. We are using Otter as Theorem prover. I'm having some problems formalizing this: "John, Mary and Derek are three ...
6
votes
2answers
146 views

Is every proof for natural numbers equivalent to an induction proof?

The other day I had the following idea: Suppose one could show that a theorem for natural numbers is not provable by induction for all $n$, in other words, there do not exist useful induction steps ...
2
votes
0answers
90 views

How much arithmetic can Predicative Second-Order EFA do?

As discussed in this MathOverflow question, I'm trying to find what the result would be of applying a Feferman-Scutte-like analysis to the predicativism of Edward Nelson and Charles Parsons, who ...
2
votes
2answers
209 views

How can we define infinitary proofs?

In the first order logic the usual notion of a formal proof for a sentence $\sigma$ from a theory $T$ is a "finite" sequence ($<\omega$ - sequeance) of sentences which each one of them is a valid ...
0
votes
1answer
86 views

Can necessity rule be derived from box introduction rule?

I need to find a proof of $\top \vdash \Box \top$ (where $\top$ is the truth constant and $\Box$ is the necessity modal operator) in the natural deduction system of IS4 modal logic. In the axiomatic ...
3
votes
1answer
157 views

Type Theory (Proof tree)

Suppose $B(x)$ set $(x:A)$ is a family of sets and $D$ is a set. Prove $(\Sigma x:A)B(x) \times D \to (\Sigma x:A)(B(x) \times D)$. Using the so called Curry-Howard correspondence one may translate ...
3
votes
2answers
98 views

Proofs with Induction Imply Proofs Without Induction?

Assume we can prove $\forall x P(x)$ in first order Peano Arithmetic (PA) using induction and modus ponens. Does this mean we can prove $\forall x P(x)$ from the other axioms of PA without using ...
2
votes
3answers
128 views

Proof of $\exists x \exists y (\varphi(x)\rightarrow \psi(y)) \rightarrow \exists x (\varphi(x)\rightarrow \psi(x))$ in natural deduction

How to show the following trivial implication with natural deduction? $\exists x \exists y (\varphi(x)\rightarrow \psi(y)) \rightarrow \exists x (\varphi(x)\rightarrow \psi(x))$ Thx.
4
votes
1answer
162 views

Curry-Howard Correspondence (Proof Theory)

As you all know, the Curry-Howard correspondance provides a link between type theory and predicate logic. Concepts featured in the former, such as $\Pi$-type and $\Sigma$-type can, by the ...
1
vote
1answer
76 views

Given a theorem can it always be reduced logically to the axioms?

It's probably a silly question but I’ve been carrying this one since infancy so i might as well ask it already. let ($p \implies q$) be a theorem where $p$ is the hypotheses and $q$ is the ...