Proof theory is an area of logic that studies proof as formal mathematical objects. For questions asking how to write proofs or for checking an informal proof, please use the proof-writing or proof-strategy tags instead.
22
votes
4answers
557 views
What is a proof?
I am just a high school student, and I haven't seen much in mathematics (calculus and abstract algebra).
Mathematics is a system of axioms which you choose yourself for a set of undefined entities, ...
3
votes
2answers
74 views
Can the nonexistence of a constructive proof be proven when an existential proof exists?
Proofs are usually constructive or existential. For example, we know there are an infinite number of primes, and therefore the centillionth prime exists. We don't know what it is, though we can make ...
5
votes
1answer
136 views
Are coinductive proofs necessary?
I've been exploring corecursion in Coq (specifically, infinite streams of natural numbers) lately and so far any coinductive predicate I've constructed and its coinductive proof can be transformed ...
37
votes
13answers
3k views
Is there such a thing as proof by example (not counter example)
Is there such a logical thing as proof by example?
I know many times when I am working with algebraic manipulations, I do quick tests to see if I remembered the formula right.
This works and is ...
5
votes
3answers
141 views
Pythagorean theorem and its cause
I'm in high school, and one of my problems with geometry is the Pythagorean theorem. I'm very curious, and everything I learn, I ask "but why?". I've reached a point where I understand what the ...
4
votes
1answer
104 views
Tricks for Constructing Hilbert-Style Proofs
Several times in my studies, I've come across Hilbert-style proof systems for various systems of logic, and when an author says, "Theorem: $\varphi$ is provable in system $\cal H$," or "Theorem: the ...
1
vote
1answer
39 views
If $x,y$ are elements of $\mathbb{R}$ and $x>0$ then there is a positive integer $n$ s.t. $nx > y$
Im reading a proof about this
The proof is here.
Let $A$ be the set of all $nx$, where $n$ runs through the positive integers.
If $nx \le y$, then $y$ would be an upper bound of $A$.
(start ...
6
votes
1answer
115 views
What are the formal properties of Godel numbering that are required to make it 'work'?
Godel numbering assigns a number to every formula. It appears to me that any encoding will do. However its also apparent, though I'm not sure how, that certain properties of the encoding used in Godel ...
-4
votes
1answer
54 views
Transformation Existence Proof: A Call for Critique [duplicate]
QUESTION
Prove that there exists a $T:V\rightarrow W$ such that $N(T)=V'\subset V$ and $R(T)=W'\subset W$
ATTEMPTED ANSWER
Let $V$ and $W$ be finite-dimensional vector spaces over $F$. Let ...
0
votes
1answer
33 views
Explanation of proof common divisor divides gcd needed
I have been given a proof that uses the gcd to show that there is no biggest prime. However (coming from a less mathematical background) I am having trouble actually understanding what it means and ...
2
votes
2answers
109 views
question about vacuous proof
Hi i have a question about vacuous true and it always make me confused~
if I want to proof empty set is the subset of all the set A, the proof is as following:
if x is in empty set, then x is in A. ...
1
vote
2answers
59 views
Induction proof [ little-o notation ]
I have to prove that $ 2^n = o(n!) $, that is, $ \forall c \gt 0 \quad \exists$ $ n_0 \in \mathbb N$ such that $ \forall n \ge n_0$ we have $ 2^n \lt c.n! $
Well, this is what I did so far:
First I ...
2
votes
0answers
155 views
Is the $ϵ,δ$ definition of a limit not well-defined?
I just watched this youtube video:
http://www.youtube.com/watch?v=K4eAyn-oK4M
He lays out his objections against the $ϵ,δ$ definition around 14 min.
Here is the discription of the video:
In ...
1
vote
2answers
47 views
Are the lengths from this recursive construction a geometric sequence?
In his 1999 review of Edward Tufte's Visual Explanations in the Notices of the AMS (third page), Bill Casselman gives a very pretty proof of the irrationality of the golden mean. More precisely, ...
0
votes
1answer
66 views
What is the official proof (if there is any) for the area of a circle of radius 'r'?
What is the official proof (if there is any) for the area of a circle of radius 'r' ?
I remember in my school days they simply told that area of a circle of radius 'r' is $\pi*r^{2}$.
The teacher ...
1
vote
0answers
27 views
Question about proof of bounded real lemma
My question is: it is possible to proof the bounded real lemma for $H_\infty$ performance with the following procedure?
The $H_\infty$ performance is defined as:
\begin{align}
\parallel ...
0
votes
1answer
74 views
Problem on set of zeros
Is it true that for each prime ideal $\mathfrak{p}$ then $V(\mathfrak{p}) \neq \emptyset$?
I know that there are prime ideals with $V(\mathfrak{p}) \neq \emptyset$, but I don't know if this is ...
6
votes
3answers
329 views
Why are $\Delta_1$ sentences of arithmetic called recursive?
The arithmetic hierarchy defines the $\Pi_1$ formulae of arithmetic to be formulae that are provably equivalent to a formula in prenex normal form that only has universal quantifiers, and $\Sigma_1$ ...
0
votes
1answer
47 views
Proofs Invertible & Diagonal matrix
Given:
$P$ is an invertible matrix.
$D$ is a diagonal matrix.
$A$ is an $n\times n$ matrix.
AND
$A = PDP^{-1}$
Prove that the determinant of A equals the product of the diagonal entries of $D$.
2
votes
4answers
98 views
Is there Problem with an Answer that can't be found?
I have been thinking about something and I don't know whether it's possible or a contradiction, 't is as follows:
Is there a mathematical problem for which we know there is an actual answer, but for ...
0
votes
1answer
119 views
Löb's theorem and provability
I learned Löb's theorem. As I understanding, if a statement is formed like "I am provable", the statement should be provable.
I want to ask further about Löb's theorem.
There is two sentences, P and ...
1
vote
0answers
62 views
proof checking machine vs. provability checking machine
Let M be a proof-checking Turing machine which takes two inputs, A and B. :
M(A,B) = 0 if A codes a valid proof of the sentence coded by B in ZFC.
M(A,B) = 1 if A does not code a valid proof of the ...
2
votes
1answer
68 views
What is the difference between $Γ⊭Φ$ and $Γ⊭¬Φ$?
Did I understand this correctly?
$Γ⊨Φ$ ($Φ$ is considered true)
$Γ⊨¬Φ$ ($Φ$ is considered false)
$Γ⊭Φ$ ($Φ$ is considered neither true nor false)
$Γ⊭¬Φ$ ???
Please help me understand. How can ...
0
votes
4answers
159 views
will computers replace (most) mathematicians? [closed]
We already have computers doing proofs and assisting mathematicians with generating proofs. I would expect that their presence will only grow larger with time as the algorithms become more practical.
...
1
vote
0answers
31 views
Direct Proof and Proof by Contradiction [duplicate]
This might seem like a random question but I am wondering can every theorem that can be proved through contradiction be proved directly or vice versa, that is is one a subset of the other or is there ...
1
vote
0answers
50 views
Examining every mathematical result in purely formal, ZFC language.
My main interest is physics. However, being self-taught in mathematics for the most part, my proofs tend to be more intuitive than it is acceptable. Yet, I recognize my inaptitude in rigor, and I ...
5
votes
2answers
121 views
What quantifies as a rigorous proof?
Okay I have been thinking about this common combinatorial identity. $$\sum_{r=0}^{n} \binom{n}{r} = 2^n.$$ It is simple to prove this by induction, but it requires some annoying algebraic manipulation ...
8
votes
2answers
174 views
Ordinal interpretation of Friedman's $n$?
I heard that Kruskal's tree theorem can be turned into a finite form that creates an extremely fast growing function because ordinals could be encoded into trees.
On this wiki page it mentions that ...
6
votes
0answers
85 views
Is there a useful Galois connection between Languages and Grammars?
I've just beginning to learn logic and proof theory - and the following rather vague and perhaps ill-formed question occurred to me.
Given an alphabet it's straightforward to construct the Language, ...
10
votes
2answers
195 views
Gentzen Cut elimination: Why do we have to “go infinite”?
I found some slides here that say you can't do cut elimination on PA with axioms like $$\frac{P(Z)\;\;\;\;\;\forall n,\,P(n) \implies P(Sn)}{\forall n,\,P(n)}$$ (which denotes infinitely many axioms ...
2
votes
0answers
63 views
Disprove the statement “every positive integer is the sum of cubes of 8 non negative integers”
Disprove the statement "every positive integer is the sum of cubes of 8 non negative integers"
May I know how can I disprove it.
As far as concern,
0, 1, 2, 3... is can be obtained using the cubes ...
1
vote
2answers
86 views
Uncertainty of process used in simple proof that there exists no rational number whose square is 2.
Hardy goes on by saying that suppose $\frac {p^2}{q^2}=\frac mn,$ where $p$ has no factor in common with $q,$ and $m$ no factor in common with $n.$ Then $n{p^2}=mq^2$.
Here is where I get confused.
...
0
votes
0answers
65 views
Proof for the upper bound on entropy $H(S)$?
I was trying to prove the upper bound on $H(S)$ using the inequalities $\ln(x)\le(x-1)$ and $\ln(1/x)\ge(1-x)$ for independent and memory less source symbols $s_1,\dots,s_q$ .
I am trying to prove ...
5
votes
1answer
87 views
First order logic - how to prove a specific part of the completeness theorem?
I am working with the proof system for FOL described in Chang and Keisler. It contains the following axiom schemes:
$\alpha \to (\beta \to \alpha)$
...
1
vote
3answers
70 views
help for proving an equation by induction
For this equation:
$$-1^3+(-3)^3+(-5)^3+\ldots+(-2n-1)^3=(-n-1)^2(-2n^2-4n-1)$$
how can I prove this by induction?
When I set $n = 1$ for the base case I got:
$$-1^3 + (-3)^3 + (-5)^3 + \ldots + ...
1
vote
2answers
107 views
How can we know arithmetical axioms are consistent?
If we assume both distributivity and the opposite of the law of signs (ie, that $-1\times-1 = -1$) for the relative integers, then we can derive that two different numbers are actually equal.
...
13
votes
5answers
812 views
If it takes infinite steps to prove a statement, is that a valid proof?
In Cantor's diagonal argument, it takes (countable) infinite steps to construct a number that is different from any numbers in a countable infinite sequence, so in fact the proof takes infinite steps ...
2
votes
1answer
138 views
A pedantic question about defining new structures in a path-independent way.
Sometimes there are multiple equivalent ways of defining the same structure; for example, topological spaces are determined by their open sets, but also by their closed sets. I'm looking for a way of ...
2
votes
2answers
148 views
Induction Proof: $\sum_{i=1}^{n+1} i \cdot 2^i = n \cdot 2^{n+2}+2 $
Prove by Mathematical Induction . . .
$$\sum_{i=1}^{n+1} i \cdot 2^i = n \cdot 2^{n+2}+2 $$
for all $n \geq 0$
I tried solving it, but I got stuck near the end . . .
a. Basis Step:
$1\cdot 2^1 ...
21
votes
6answers
1k views
If all sets were finite, how could the real numbers be defined?
An extreme form of constructivism is called finitisim. In this form, unlike the standard axiom system, infinite sets are not allowed. There are important mathematicians, such as Kronecker, who ...
24
votes
2answers
833 views
Proof by contradiction vs Prove the contrapositive
What is the difference between a "proof by contradiction" and "proving the contrapositive"? Intuitive, it feels like doing the exact same thing. And when I compare an exercise, one person proofs by ...
1
vote
2answers
67 views
The standard approach to second-order axiom systems
This is a very basic question, but for some reason I couldn't find an answer elsewhere on the Internet.
Suppose we have an axiom system $A$ written in the language of second-order logic. In order to ...
1
vote
1answer
80 views
proof that a function is integrable on a interval $[a,b]$
a) Divide a interval $[a,b]$ into $n$ equal subintervals.
here I'm thinking $P_{n} =(x_0,x_1,x_2,x_3,x_{n-1}, x_n)$ where $a = x_0 < x_1 < x_2 < x_3 <\dots< x_{n-1} < x_n = b$
...
1
vote
0answers
44 views
Want to show the a proof of the sequent $\forall x \forall y R(x,y) \Rightarrow R(y,y)$ must have a cut
Want to show the a proof of the sequent $\forall x \forall y R(x,y) \Rightarrow R(y,y)$ must have a cut. For this question we are in the Gentzen calculus. I am even having trouble just finding a ...
3
votes
2answers
80 views
Currying and Uncurrying of logical formulas, is $(A \land B) \to C \leftrightarrow (A\to B)\to C$
With a truth table its easy to see that the two formulae $A\land B \to C$ and $A \to B \to C$ are not equivalent, for example, if $A = B = C = 0$, than the first evaluates to $1$ and the second to $0$ ...
4
votes
2answers
111 views
Why does this step work in this proof?
I'm trying to learn discrete math and am brushing up on proofs by reading Richard Hammack's Book of Proof. I'm tripped up on this proof... I understand that it's contrapositive, and why contrapositive ...
34
votes
2answers
675 views
Is it possible to prove a mathematical statement by proving that a proof exists?
I'm sure there are easy ways of proving things using, well... any other method besides this!
But still, I'm curious to know whether it would be acceptable/if it has been done before?
-1
votes
2answers
117 views
formal proof about inequality in numbers
This problem appears in some material about cryptography related to negligible and non-negligible functions.
In the material says :
epsilon is negligible if
For all $d$, there exists some ...
4
votes
2answers
116 views
Sequent calculus and first incompletness theorem
Wikipedia says that sequent calculus is sound and complete (http://en.wikipedia.org/wiki/Sequent_calculus#Properties_of_the_system_LK). Godel first incompleteness theorem says that system capable of ...
0
votes
0answers
45 views
Jacobis method?
I am studying the module mathematical methods and came accross this question in a past paper:
any help is hugely appreciated! thank you :)
