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
1answer
36 views

Two tangents BC and BD are drawn. Prove that Ob=2BC

Two tangent segments BC & BD are drawn to a circle with centre O such that $\angle$CBD=120$^{\circ}$. Prove that OB=2BC. What I've tried, BC=BD[two tangents drawn from a single point to the ...
3
votes
1answer
42 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 ...
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$. ...
0
votes
1answer
62 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 ...
45
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. ...
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
80 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 ...
1
vote
1answer
41 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 ...
-1
votes
0answers
24 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
51 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
35 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$ ...
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 ...
-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
402 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 ...
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
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 ...
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 ...
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
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 ...
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 ...
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 ...
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} | ...
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 ...
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
44 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?
2
votes
1answer
27 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. ...
0
votes
1answer
84 views

Can you prove that something is provable/unprovable? Give an example [closed]

Also, can something be unprovable by definition?
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
50 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), ...
1
vote
2answers
101 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", ...
3
votes
2answers
98 views

Proofs about theorem-provers in ZFC, in ZFC

Is the following statement provable in ZFC for some $A$: "$A$ is an algorithm which, when given as input a proposition $p$ in the language of ZFC, outputs 'yes' only if $p$ is provable in ZFC, 'no' ...
0
votes
1answer
60 views

Why aren't definitions well formed formulas?

Why aren't definitions well formed formulas? For instance, the definition of an additive inverse is: "Let $x \in \Bbb Z$. Then the additive inverse of $x$ is $y \in \Bbb Z$ such that $x+y=0$". Why ...
0
votes
1answer
44 views

Equivalence Rule for Sequent Calculus

Why are there no inference rules for equivalence (≡ on the right and ≡ on the left) for the sequent calculus, and if there was, how would they look like? e.g. (1) $\cfrac{?}{\Gamma,(A \supset B) ≡ ...
1
vote
2answers
61 views

Prove $\emptyset \vdash(\alpha\rightarrow (\neg\alpha\rightarrow \neg \beta))$.

Prove $\emptyset \vdash(\alpha\rightarrow (\neg\alpha\rightarrow \neg \beta))$. Using the axioms: $(\phi \rightarrow(\psi \rightarrow \phi))$ ...
2
votes
1answer
115 views

Example of a probability theorem that requires axioms in addition to Kolmorogov's?

Probability theory, in it's more general form, is axiomatized by Kolmorogov's axioms: Kolmorogov's Probability Axioms Let $(\Omega,\mathcal{F},P)$ be a measure space. The three axioms are: ...
0
votes
1answer
51 views

Is there some result that says a theory cannot prove the consistency of any of its extensions?

Is there some result that says a (sufficiently strong) theory cannot prove the consistency of any of its extensions? Or something along these lines?? More generally, is there a result that says a ...
0
votes
2answers
83 views

Induction is the only way? [closed]

Are there any statements that are true and can only be proved by induction? (In most of the proofs I saw the induction proof shed some light on another way of proving a statement e.g. with ...
0
votes
0answers
54 views

Is my proof of the Division Algorithm 'enough'?

Recently when learning number theory I was introduced to the proof of the division algorithm, it can be found here http://www.oxfordmathcenter.com/drupal7/node/479. However, I decided to prove it ...
33
votes
11answers
2k views

What is exactly the difference between a definition and an axiom?

I am wondering what the difference between a definition and an axiom. Isn't an axiom something what we define to be true? For example, one of the axioms of Peano Arithmetic states that $\forall ...