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
8 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
61 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
37 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
40 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
15 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
53 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 ...
0
votes
0answers
73 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 ...
5
votes
2answers
65 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
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 ...
3
votes
1answer
60 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 ...
7
votes
1answer
1k views

Why can't reachability be expressed in first order logic?

I'm wondering why we can't express graph reachability in first order logic in pretty much exactly the same way we express it in second order existential logic. For SOL, one definition is : 1 . L is ...
0
votes
0answers
37 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 ...
218
votes
15answers
10k views

Can every proof by contradiction also be shown without contradiction?

Are there some proofs that can only be shown by contradiction or can everything that can be shown by contradiction also be shown without contradiction? What are the advantage/disadvantages of proving ...
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 ...
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 ...
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 ...
1
vote
1answer
81 views

Proof in sequent calculus without cut

I met an exercise in Gaisi Takeuti, Proof Theory [Exercise 2.7, page 14]. How to construct a cut-free proof of$\ \forall xA(x)\rightarrow B\vdash \exists x(A(x)\rightarrow B)$, where A(a) and B are ...
2
votes
1answer
171 views

Sequent calculus - proofs as trees or sequences

First at all, I am new at proof theory, so excuse this perhaps redundant question. I am wondering what is the 'most appropriate' definition of a proof in a sequent calculus (e.g. LK). Proofs as trees ...
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) ≡ ...
0
votes
0answers
44 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 ...
3
votes
0answers
446 views

Difference between soundness and correctness

Is there any actual semantic difference between soundness and correctness? Can I use these words interchangeably when talking about formal reasoning, proof, logics, etc.? Otherwise, is there a ...
1
vote
0answers
42 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
41 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 ...
6
votes
3answers
632 views

What does “rigorous proof” mean?

I have heard several times that some mathematician has given another and more rigorous for an established theorem, but I don't know what does it really mean and what differences makes it to be more ...
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 ...
6
votes
2answers
144 views

Is every proof for natural numbers equivalent to an induction proof?

The other day I had the following idea: Suppose one could show that a theorem for natural numbers is not provable by induction for all $n$, in other words, there do not exist useful induction steps ...
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 ...
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. ...
120
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
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 ...
0
votes
1answer
31 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
92 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
417 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
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 ...
5
votes
5answers
186 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
64 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
3answers
126 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.
3
votes
3answers
202 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. ...