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
1answer
60 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 ...
3
votes
2answers
71 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
23 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
24 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
37 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 ...
42
votes
8answers
4k 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
57 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
71 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
68 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
52 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
44 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 ...
2
votes
1answer
25 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
92 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
50 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
56 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
66 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
41 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
120 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
31 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? ...
4
votes
3answers
165 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
27 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 ...
1
vote
3answers
23 views

Greatest Common Divisor written proof

Here is what I am trying to prove: Let $a,b,c,d \in ℤ_+$ with gcd$(a,b)=1$. If $a|c$ and $b|c$, prove that $ab|c$. Does the result hold if gcd $(a,b)\neq 1$ ? I know that gcd $(a,b)=1$ can be ...
0
votes
1answer
41 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
83 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 ...
6
votes
2answers
220 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
19 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...)
11
votes
3answers
371 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
40 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
43 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
35 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
53 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: $$ ...
2
votes
1answer
40 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
82 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
33 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
40 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
54 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
1answer
50 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 ...
1
vote
1answer
34 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
131 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 ...
4
votes
4answers
313 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] ...
0
votes
2answers
61 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 ...
0
votes
2answers
124 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 ...
0
votes
2answers
86 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
0answers
37 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
47 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 ...
2
votes
0answers
69 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 ...
0
votes
1answer
85 views

Proof by contradiction: May I assume $P$ (true) in $\neg Q \land P \Rightarrow P \land \neg P$ to prove $Q$ by contradiction

Suppose I wish to do a proof by contradiction the statement $Q$. In proving $Q$ may I assume $\neg Q \land P$ (where $P$ is a statement known to be true) and show the implication $\neg Q \land P ...
3
votes
2answers
95 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 ...
88
votes
11answers
10k 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 ...
1
vote
0answers
47 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 ...