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
1answer
58 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 ...
34
votes
5answers
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
25 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 ...
1
vote
1answer
38 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
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
24 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$ ...
2
votes
4answers
65 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
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 ...
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
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?
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. ...
0
votes
1answer
79 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
48 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
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", ...
3
votes
2answers
97 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
53 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 ...
0
votes
0answers
23 views

What is this P4 correspond to in proposition as types?

I was reading "Proofs and Types", so there came across that any proposition can be converted to lambda form. So was trying out with Hilbert system's axioms P1. $A \rightarrow A $ P2. $A \rightarrow ...
3
votes
0answers
50 views

Can every mathematical proof be seen as the verification of some algorithm's action?

Put another way: Can every mathematical proof be reformulated to be about some class of Turing Machines? Example Any proof of the existence of infinite prime numbers is equivalent to the statement: ...
2
votes
1answer
40 views

Number of proofs for a statement

On this site, people ask questions and then answers and proofs for those answers come from readers. Readers mark the best answer and then people focus on the next interesting topic. Sometimes, a ...