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

1
vote
0answers
20 views

Is there a consistent arithmetically definable extension of PA that proves its own consistency?

Gödel's second incompleteness applies, for instance, to r.e. extensions of PA. I am wondering if it applies more generally to arithmetically definable extensions of PA. I see that there is a complete ...
41
votes
6answers
2k views

Proving the existence of a proof without actually giving a proof

In some areas of mathematics it is everyday practice to prove the existence of things by entirely non-constructive arguments that say nothing about the object in question other than it exists, e.g. ...
1
vote
2answers
37 views

Discrete math induction proof

I am trying to solve a induction proof and i got stuck at the end, some help would be great. This is the question and what i did so far: Statement: For all integers $n \geq 5$ we have $2^n \geq n^2$. ...
118
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 ...
0
votes
1answer
61 views

Is it possible to create a software to find formal proofs?

Let's say I have a Hilbert style system, with a few axioms and rules of inference, and I want to find a proof for some formula $\varphi$, is it possible to create an algorithm that would find a proof ...
0
votes
1answer
27 views

Prove in GL that no statement can be proven consistent with PA unless PA is inconsistent

I'm trying to do a exersie on page 16 of this paper. It says: Exercise. Show, using the rules of Godel-Lob modal logic (GL), that $\square⊥ ↔ \square \diamond p$; recall that $\diamond p = ...
2
votes
2answers
79 views

Can a mathematical theorem be proved in infinite ways?

This is a question that I really think about. I wanted to develop my mind, and started trying to prove the Pythagorean theorem of a triangle, trying each day, and now its been a week. I wonder if ...
2
votes
1answer
531 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.
1
vote
1answer
39 views

Is there a connection between local soundness and completeness in proof theory, and free objects in category theory?

I was watching Frank Pfenning's lecture series on proof theory, where he described the notions of local soundness, and local completeness. He described local soundness of a logical connective as, ...
0
votes
1answer
21 views

Boolean Algebra x+y=0 proof

So I am having a problem solving this proof of Boolean algebra. I am trying to prove that if x + y = 0 then x = 0 This is what I have tried ...
0
votes
2answers
133 views

Prove every angle has a bisector.

Prove every angle has a bisector. I have successfully constructed a bisector and justified by construction. Now I need to put it in proof form. However, I technically do not know midpoints and ...
-1
votes
0answers
23 views

What does meant “Uncounditional proof” and why should believe it that is a complet proof?

I have tried many times to understand what it does meant "Uncounditionally proof" but i don't succed , only I think that is the proof which produced from Insufficient conditions and and havn't enough ...
1
vote
1answer
25 views

If a set $S$ is inconsistent, does $S\vdash \alpha$ for all $\alpha$ in this system?

Let $S$ be an inconsistent set of propositional formulas. If our system consists of the axioms: \begin{align} AX1&\quad (P\implies (Q \implies P))\\ AX2&\quad (((P\implies(Q\implies ...
2
votes
1answer
45 views

Use induction to prove that any (finite) list is a permutation of itself—in other words, that the permutation relation is reflexive.

I'm having a bit of trouble with starting this proof by induction. I'm given that the definition of a permutation is: List a is a permutation of list b if any of the following are true: • list a and ...
2
votes
0answers
50 views

Does it make sense to claim that something cannot be proven without induction? [duplicate]

Often we have questions on this site which ask for a proof of some result without induction.1 It seems that when such a question is posted, it is quite well-understood what is meant by proof avoiding ...
1
vote
2answers
51 views

Is mathematical Induction possible in this situation?

Is mathematical Induction possible with this sigma sign? $\sum_{k=1}^{n} ((-1)^{n-k} * b^{n-k}) = \frac{b^{n}+1}{b+1}$ with $n = 2s+1 ; s \epsilon \mathbb{N}$ Statement: $\sum_{k=1}^{n} ...
1
vote
0answers
34 views

Soundness of Propositional Logic proof.

Let $$\begin{align} A1&=(p\implies (q\implies p)) \\ A2&=(((p\implies (q \implies r)) \implies ((p\implies q)\implies (p\implies r))) \\ A3&=((\neg p \implies \neg q ) \implies ((\neg p ...
1
vote
1answer
36 views

Can we assign a number to each theorem stating its complexity?

I was wondering if inside an axiomatic theory it could be possible to assign each theorem a number that indicates its complexity. Theorems with small complexity numbers would be "almost axioms"; if ...
2
votes
1answer
39 views

Is there a formula for general induction?

When I read about mathematical induction, there is no general formula, just a notion that is described: Show true for $n = 1$ Assume true for $n = k$ Show true for $n = k + 1$ ...
7
votes
4answers
338 views

mathematical proof vs. first-order logic deductions

For a long time I thought that the standard mathematical proofs, only were an informal or imperfect way of writing the proof in the language of first-order logic. When I say standard mathematical ...
2
votes
4answers
66 views

Does proving that there exists a maximum value in $[a,b]$ for a function $f(x)$ prove that there exists a minimum value too?

I've seen several proofs, such as this one http://math.duke.edu/~cbray/Stanford/2000-2001/math41/EVTProof.pdf, of the extreme value theorem where the writer has proved there exists a maximum value of ...
2
votes
2answers
46 views

Delta epsilon argument in general

When I want to prove something in mathematics fe an expression goes to zero, I can either use basic rules of 'limits' or I can use the epsilon-delta method. I have a feeling that it's more consistent ...
0
votes
2answers
35 views

Proofs with for all statements including uniqueness and divides

Let $\mathcal{A}$ be a nonempty finite set of positive integers, with $\forall$ r $\in$ $\mathcal{A}$, $\forall$ s $\in$ $\mathcal{A}$ : r|s or s|r. (i). Prove $\exists$t $\in$ $\mathcal{A}$: t|a, ...
-1
votes
1answer
47 views

For which $n_o \in \mathbb{N}$ is it possible to show with induction that $2\log_2(n) \leq n$ applies?

For which $n_o \in \mathbb{N}$ is it possible to show with induction that $2\log_2(n) \leq n$ applies? for all $n \in \mathbb{N} $ with $ n \geq n_0$? How to proceed to such questions? Hope somebody ...
5
votes
2answers
401 views

Programming and ZFC

Suppose I have a simple program that implements an algorithm (say depth-first search), written in a simple imperative programming language with the standard for loops, recursions, conditional ...
1
vote
2answers
83 views

Analysis and formal proofs.

Ever since I started learning formal logic I've had these kind of doubts: Is analysis ever studied in a completely axiomatic/formal proofy way? What I mean is, given a set of axioms and inference ...
0
votes
1answer
28 views

Must non-constructive existential proofs use axioms of foundation or choice?

I have been getting confused thinking about non-constructive proofs. Several axioms of ZFC imply existence of a set with certain properties, and for each axiom except foundation, infinity, and ...
2
votes
1answer
36 views

Prove that there exists only 1 prime number of the form $p^2−1$ where $p≥2$ is an integer.

by factoring $p^2−1$, we have $(p+1)(p-1)$. I know that p=2 which gives 3 is the only solution, however how do I prove that p=2 is the only integer which gives a prime?
5
votes
5answers
156 views

what is a valid mathematical proof?

from what i have seen in my experience with math we can say that a valid proof is one that uses some form of logic (usually predicate logic) and uses logical rules of deduction and axioms or ...
1
vote
1answer
63 views

Is the length of the proof of propositional tautology a PA-total function?

Suppose we have fix some interpretation of propositional (not first-order!) logic inside PA, and say $f(n) = $ {the maximum length of a proof of a tautology with $n$ propositional primitives} ...
2
votes
2answers
96 views

Prove by Natural deduction that $\lnot\exists xP(x)\rightarrow\forall x\lnot P(x)$

I got this problem: Prove by Natural deduction in First Order Logic that $\lnot\exists xP(x)\rightarrow\forall x \lnot P(x)$ I tried to prove it using the Contradiction Theorem but I got ...
2
votes
3answers
122 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.
1
vote
1answer
43 views

Motivation for signed tableaux rules for propositional intuitionistic logic

I've been studying a signed tableaux proof system for propositional intuitionistic logic, and I'm confused about two of the inference rules stipulated. Most of the inference rules are quite ...
3
votes
3answers
195 views

What is this proof syntax (Hoare 1974)?

I'm reading the seminal "Monitors" paper by Hoare. On page 4 he proceeds with a logical proof using syntax I've never seen before, and neither know what it's called or how to properly read it. ...
2
votes
1answer
33 views

“Relatively” functionally complete connectives

The Sheffer stroke (https://en.wikipedia.org/wiki/Sheffer_stroke) is functionally complete: any truth-functional connective (such as $\wedge, \vee, \rightarrow$, . . .) can be represented purely in ...
1
vote
3answers
50 views

Prove $\forall n\in\mathbb{Z}$ that if $n \equiv 3 \pmod 6$ then $36 \mid (n^2 + 27)$

Prove $\forall n\in\mathbb{Z}$ that if $n \equiv 3 \pmod 6$ then $36 \mid (n^2 + 27)$ I know that $n \not\mid 6$ therefore, $6 \not\mid n$ and $6$ is not a multiple of $n$. But it's not helping ...
1
vote
1answer
35 views

What is the order of precedence to $\Gamma \vdash \phi \Rightarrow \psi$?

In this context, $\phi$ and $\psi$ are formulas and $\Gamma$ is a set of formulas. I'm not quite sure what it means. Does it mean $\Gamma \vdash (\phi \Rightarrow \psi)$ or does it mean $(\Gamma ...
21
votes
3answers
2k views

Why is Gödel's Second Incompleteness Theorem important?

Given that the consistency of a system can be proven outside of the given formal system, Gödel says, It must be noted that proposition XI... represents no contradiction to the formalities ...
0
votes
1answer
42 views

Show proof technique

Given $\Gamma^n := \{\phi_{i} \rightarrow \phi_{i+1} | 1 \le i \le n-1 \} \bigcup \{\phi_{n} \rightarrow \phi_{1}\}$ . I want to show that $ \Gamma ^ {n} \vDash \{\phi_{i} \leftrightarrow \phi_{j} | ...
2
votes
2answers
39 views

Hilbert-style proof of $\Gamma\vdash\psi$ and $\Gamma\vdash\chi$ implies $\Gamma\vdash\psi\wedge\chi$

I am given the following Hilbert-style system (for intuitionistic propositional logic): Axiom schemes: $\phi\vee\phi\rightarrow\phi$ $\phi\rightarrow\phi\wedge\phi$ $\phi\rightarrow\phi\vee\psi$ ...
0
votes
2answers
43 views

Show that for any natural number $n>24$ there exist natural numbers $p$ and $q$ such that $ n=5p+7q$

Show that for any natural number n>24 we have : $n=5p+7q$ such that $p$ and $q$ are natural. I tried using induction 1) for $n=24$ we have $n=(7 \cdot 2)+(5 \cdot 2)$ 2) we suppose that ...
3
votes
0answers
18 views

Looking for references for learning the words and sentences used in proofs

I'm familiar with textbooks on logic, proof techniques, and sets. But I have yet to encounter a textbook that dives into the language used w/ definitions and sentence structure used in proofs, for ...
1
vote
0answers
19 views

Logic behind an IFF statement

If we have an iff statement such as: $A$ iff $B$, to show $A \Rightarrow B$ is it enough to show that not $B \Rightarrow$ not A?
1
vote
2answers
98 views

How to proofs work in three-valued Kleene logic?

In three-valued logics such as Kleene logic, there is a third truth value U, which represents "undefined", or "who knows?". It behaves like "either true or false", ...
2
votes
1answer
26 views

Piecewise function within a proof. Verification.

Prove or give a counterexample. If $f$ is decreasing on $(-\infty,0)$ and if $f$ is decreasing on $[0, \infty)$, then $f$ is decreasing on all real numbers. I have chosen to give a counterexample. ...
3
votes
1answer
71 views

What exactly is wrong with this argument (Lucas-Penrose fallacy)

Argument "For every computer system, there is a sentence which is undecidable for the computer, but the human sees that it is true, therefore proving the sentence via some non-algorithmic method." ...
2
votes
2answers
93 views

A philosophical question about an hypothetical theorem/equation of everything

Preamble I'm not a mathematician. I'm just curious. Please forgive my pseudo formalism. Please allow me, a non mathematician, to have just questions. Definition A mathematical theorem is a statement ...
1
vote
1answer
18 views

Induction T/F questions. How to know what the counterexample is.

Determine whether the statement is true of false. If true, provide a proof. If false provide a counterexample. for $n \in N, 2n-8 < n^2-8n+17$ I started off like a typical induction proof. ...
2
votes
1answer
49 views

De Morgan's Law proof?

The proof for (A ∪ B)' = (A' ∩ B') is: Let's say x ∈ (A ∪ B)'. This means x ∉ (A ∪ B), ...