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
16 views

The product of any two even integers is a multiple of 4

The product of any two even integers is a multiple of 4." This is what I have so far: let n, m be even integers and let D be a integer that is divisible by 4. n=2k. m=2l. d=4p. such that k,l,p ...
0
votes
0answers
21 views

Unprovable identity over the integers

I was thinking about Tarski's problem, and was wondering what happens if we have a theory $T$ with two sorts $N,Z$ with intended interpretations $\def\nn{\mathbb{N}}$$\def\zz{\mathbb{Z}}$$\nn,\zz$ ...
22
votes
7answers
2k views

Can you use both sides of an equation to prove equality?

For example: $\color{red}{\text{Show that}}$$$\color{red}{\frac{4\cos(2x)}{1+\cos(2x)}=4-2\sec^2(x)}$$ In high school my maths teacher told me To prove ...
0
votes
1answer
60 views

What kind of proof is this?

Let's say that we want to prove that object A is blue. Is the following reasoning true? First assume that $A$ is indeed blue. Then, use other axioms to show that depending on a control parameter ...
0
votes
1answer
16 views

Suppose $C = AB$. Show $\hat{c}_j = \sum_{k} b_{kj}\hat{a}_{k}$.

Suppose $C = AB$. Show $\hat{c}_j = \sum_{k} b_{kj}\hat{a}_{k}$. $A$, $B$, and $C$ are square matrices of the same size. $\hat{c}_j$ is the $j$th column of $C$, $\hat{a}_k$ are the columns of $A$, ...
0
votes
0answers
62 views

Profane Model Theory, sacred Proof Theory

Dirck van Dalen starts the Preface to his Logic and Structure with the following words: "Logic appears in a ‘sacred’ and in a ‘profane’ form; the sacred form is dominant in proof theory, the ...
0
votes
1answer
39 views

Rules for getting rid of assumptions for certain variables which do not appear in the conclusion of a proof

From my understanding, sometimes in proofs we may 'let' a certain variable be equal to a mathematical object in question for ease of referring to it. Then later on in the conclusion we may substitute ...
2
votes
1answer
42 views

Proof related to pigeon hole principle to be done with induction

since the question is about a positive integer m, it's obvious that the use of mathematical induction needed, but to prove the fact for n = k+1 we have to use the pigeon hole principle, i am so ...
0
votes
0answers
16 views

Show that $σ(i_1, i_2, . . . , i_k)σ^{−1} = (σ(i_1), σ(i_2), . . . , σ(i_k))$

Here's the full question: If $σ ∈ S_n$ is any permutation and $i_1, . . . , i_k $ are $k$ distinct elements of $\{1, . . . , n\}$, show that $σ(i_1, i_2, . . . , i_k)σ^{−1} = (σ(i_1), σ(i_2), . . . , ...
3
votes
2answers
47 views

learning linear algebra [duplicate]

So I'm a college student that has taken 3 semesters of calc/diff eq/linear algebra and I think linear algebra has been by far my favorite course so far and I would love to know more in the subject, ...
0
votes
1answer
54 views

Interpretation help: Showing that Riemann Hypothesis holds “almost surely”

I was perusing this textbook on algorithmic number theory, where I came across this page where they appear to prove that the Riemann Hypothesis holds almost surely. This seems like an odd statement ...
3
votes
4answers
116 views

Mathematical Rigor in Proving Limits by $\epsilon-\delta$ Definition

I am trying to find the most mathematically rigorous way to prove limits, using the $\epsilon-\delta$ definition of a limit, so far I have found two clear cut methods of proving limits using the ...
5
votes
2answers
66 views

Proof by induction, 1 · 1! + 2 · 2! + … + n · n! = (n + 1)! − 1

So I'm supposed to prove that $$1 · 1! + 2 · 2! + \dots + n · n! = (n + 1)! − 1$$ using induction. What I've done Basic Step: Let $n=1$, $$1\cdot1! = 1\cdot1 = 1 = (n+1)!-1 = 2!-1 = 2-1 = 1$$ ...
0
votes
0answers
74 views

In what formal proof systems is the deduction theorem taken as a primitive rule of inference?

Wikipedia's article on the deduction theorem states: Although the deduction theorem could be taken as primitive rule of inference in [Hilbert-style] systems, this approach is not generally ...
3
votes
1answer
61 views

Does no non-standard model of Peano Arithmetic make the integers a principal ideal domain?

Though I do not find a reference now, I have heard no non-standard model of Peano Arithmetic has a principal ideal domain as its ring of integers. Is that right? Is it trivial? Or is there a good ...
0
votes
1answer
30 views

Gentzen-style proof system with global states?

I'm sorry if my question looks stupid or does not make sense. However, I want to ask if it is normal/common to have a global state, which is shared by all inference rules, in a Gentzen-style proof ...
0
votes
0answers
38 views

Is there a standard notation for coding finite sets of numbers as numbers?

Hajek and Pudlak Metamathematics of First-Order Arithmetic use the Ackermann encoding of hereditarily finite sets, but they use no notation for codes. They let the reader see from context when a ...
0
votes
0answers
10 views

Proving weak simulation

I want to prove something but I am not sure if it is the right way to do it. I have two LTS that define different semantics. A=($Q_a,Λ,\to)$, and B=$(Q_b,Λ\cup\{\beta\},\leadsto)$, where $\beta$ is ...
38
votes
3answers
4k views

Can proof by contradiction 'fail'?

I am familiar with the mechanism of proof by contradiction: we want to prove $P$, so we assume $¬P$ and prove that this is false; hence $P$ must be true. I have the following devil's advocate ...
1
vote
1answer
51 views

HPC: Prove that $\vdash A\to \lnot\lnot A$

Prove that $\vdash A\to \lnot\lnot A$ By Deduction Rule we know that it is sufficient to show that ${A}\vdash \lnot\lnot A$ I am also familiar with the formula: $\lnot A \vdash (A\to B)$. So if ...
0
votes
0answers
45 views

Prereqisites for: Subsystems of second order arithmetic

As the title suggests, im wondering what the prerequisites for Simpsons book, Subsystems of... are? Unfortunately I cant find it in the preface. My background is a Bachelor in Philosophy and ...
1
vote
0answers
47 views

Can we prove that induction is impossible for some proofs?

I read in a book that Andrew Wiles first attempted proof by induction to prove Fermat's last theorem and that he gave up proving it with induction. Instead as far as I understand, Wiles proved some ...
4
votes
2answers
78 views

Why is it so hard to translate some proves into machine-readable form?

I have just read a topic on mathoverflow about man vs. machine in mathematics. The topic was inspired by the recent victory of Alpha Go over the World Go Champion, Lee Sedol. It reminded me of an ...
1
vote
1answer
16 views

Cannot create algorithm for decidable language

L2 = {<M> : M is a TM and there exists an input string w such that M halts within 10 steps on input w} Hi. I am creating an algorithm to show above L2 is ...
0
votes
0answers
37 views

Algebraic embeddings and isomorphisms in formalized ZFC

Example: It is always said that we can embed $\mathbb{Z}$ within $\mathbb{Q}$ by identifying $z \in \mathbb{Z}$ as $(z,1) \in \mathbb{Q}$. This is because there is an injective ring homomorphism $\phi ...
1
vote
0answers
43 views

Do we sometimes prove things based on the assumption that mathematics is self-consistent?

Do we sometimes prove things based on the assumption that mathematics is self-consistent? I recently started to be dubious about proofs by contradiction. It seems to me that it is somehow based ...
1
vote
0answers
28 views

Equivalence between sequent calculi with different cut rules

Let G4' be a sequent calculus G4 for classical logic with the addition of the following pair of "left" and "right" cut rules: Let now be G4'' a second calculus G4 for classical logic with the ...
1
vote
1answer
35 views

Is $\neg \neg \forall \neg \neg A \leftrightarrow \forall \neg \neg A$ intuitionistic derviable?

Is the following a rule which is derivable in intuitionistic logic: $\neg \neg \forall \neg \neg A \leftrightarrow \forall \neg \neg A$ I thought that I read it somewhere,... hope that someone can ...
40
votes
12answers
6k views

Are proofs by contradiction really logical? [closed]

Let's say that I prove statement $A$ by showing that the negation of $A$ leads to a contradiction. My question is this: How does one go from "so there's a contradiction if we don't have $A$" to ...
1
vote
1answer
52 views

How is the non-existence of a solution proven?

I've been wondering how an argument that a solution to a particular problem doesn't exist is put together. For instance "Pour-El and Richards found an ordinary differential equation ...
1
vote
0answers
75 views

Incompleteness theorems in encoding schemes other than Gödel numbering

Gödel's proof of his incompleteness theorems makes use of Gödel numbering, which is a device that allows a theory of arithmetic $S$ (e.g. PRA) to express and reason about metamathematical statements ...
3
votes
1answer
60 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 ...
0
votes
1answer
69 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
32 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 = ...
3
votes
2answers
96 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
58 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, ...
2
votes
0answers
54 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
1answer
38 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 ...
5
votes
2answers
418 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 ...
5
votes
5answers
187 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 ...
0
votes
1answer
38 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
130 views

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

Also, can something be unprovable by definition?
2
votes
2answers
106 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 ...
3
votes
2answers
107 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
54 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) ≡ ...
2
votes
1answer
121 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
52 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
87 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 ...
34
votes
11answers
3k 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 ...