Tagged Questions

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-* ...

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$, ...
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 ...
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 ...
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 ...
15 views

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 ...
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 ...
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 ...
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 ...
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 ...
37 views

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 ...
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, ...
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 ...
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 ...
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 ...
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 ...
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 ...
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} ...
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.