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

1
vote
2answers
31 views

What does this proposition mean?

$∀x ∈ P(\Bbb{N}), x \notin \{\} \Rightarrow ∃y ∈ x, ∀z ∈ x \ | \ y < z$ Where $P(x)$ is the power set. I'm interpreting it as "in all subsets of the natural numbers, there exists a value smaller ...
1
vote
1answer
165 views

How to check homeomorphic embedding relation programmatically?

This is a follow up to this question and Deedlit's answer. I'm looking for a precise definition of the "hem?" (tree A homeomorphically embeddable in tree B?) relation, preferably in terms of a ...
-2
votes
1answer
49 views

Z / 6Z being a set of well dedfined equivalence classes, and a congruent to b(mod 6)

why is this = [0],[1],[2],[3],[4],[5],[6] and how would I define f Z/6Z - Z/6Z by f([a]) = ([2a]). I have the proof but I don't understand it. Proof: Assume [a1] = [a2] in Z/6Z. then a1 congruent to ...
0
votes
1answer
70 views

Proving Theorem: subspace of polynomials of degree two or less?

How can I prove that the set $S$ of polynomials of degree $2$ or less, whose coefficients sum to zero, is a subspace of all polynomials with degree $2$ or less? I know I need to show that $a+b+c=0$ ...
1
vote
5answers
112 views

Proof by Induction Divisibility.

$6^n-5n+4$ is divisible by 5 for all positive integers $n$. $n >=1$ Prove By Induction My attempt is as follows: $n=1$ $6^1-5(1) +4$ $=5$, Therefore 5 is divisible by 5 so $n=1$ is true ...
1
vote
1answer
99 views

Uncountable reals in the theory

The Question I'm looking for a possibility to somehow proof the "essence" of Cantor's diagonal argument within a recursive first-order theory which is satisfied by the reals (better: within a theory ...
2
votes
0answers
62 views

How far can-I rewrite in lambda functions?

I am quite new with the lambda calculus. I am experimenting lambda-calculus proofs through the coq proof assistant, but the question I have is not related to coq (I guess). However, I'm going to use ...
0
votes
1answer
90 views

Euclid's proof for infinitely many prime numbers

Prove that there are infinitely many primes congruent to 3mod4 using euclid's proof for infinitely many prime number. I guess I don't really know where to start because I don't understand euclid's ...
1
vote
1answer
75 views

Comparing Statements and predicates using Truth Tables

Consider the four statements: $∃x$ $∀y$ $p(x, y)$ $∃y$ $∀x$ $p(x, y)$ $∀x$ $∃y$ $p(x, y)$ $∀y$ $∃x$ $p(x, y)$ which we call S1, S2, S3 and S4 respectively. Does there exist a predicate p such ...
1
vote
1answer
59 views

Model-theoretic question about language of field theory.

Let $\mathscr{L}=\{+,·\}$ be the language of the theory of fields. Let $\phi$ be a sentence in this language. Show, using the compactness theorem of first-order logic, that if $\phi$ holds in finite ...
13
votes
2answers
1k views

How to find the shortest proof of a provable theorem?

Roughly speaking, there are some fundamental theorems in mathematics which have several proofs (e.g. Fundamental Theorem of Algebra), some short and some long. It is always an interesting question ...
3
votes
2answers
73 views

Undecidability and truth

Are there undecidable problems for which a single truth exists? For example, the question about parallels is not decidable from Euclid axioms. But multiple answers are valid and give different kinds ...
0
votes
2answers
63 views

Prove the Cauchy-Schwarz Inequality (missing a step)

during lecture notes I only caught most of the proof and couldnt write a step down fast enough, and I'm having a touch trouble seeing how to get from the previous step to the next. Here is what i have ...
1
vote
1answer
72 views

How can Goodstein's theorem be expressed in PA

I understand Goodstein's Theorem and its proof. I'm trying to understand the proof of why Goodstein's Theorem cannot be proved in PA. However, it's not immediately clear to me that Goodstein's Theorem ...
8
votes
1answer
462 views

Why wouldn't someone accept Gentzen's consistency proof?

Reading the consistency section of the Peano Axioms wikipedia page, I came across this sentence: The vast majority of contemporary mathematicians believe that Peano's axioms are consistent, ...
1
vote
1answer
67 views

Question about the incompleteness proof (Theorem V)

Question in short: Where do I find a complete proof of Theorem V from Gödels incompleteness proof? If it does not exists, can someone provide it? Question in detail: I am trying to understand ...
4
votes
1answer
193 views

Birkhoff's completeness theorem

I have two simple questions. A) Does Birkhoff's completeness theorem follow directly from Gödel's completeness theorem? B) Is Birkhoff's completeness theorem constructive in the following sense: ...
3
votes
2answers
210 views

Is constructive proof of non-existence possible

Constructive proof construct(indicates) object that satisfies given predicate. Question is whether one can give constructive proof of non-existence of an object with given property e.g. that every ...
2
votes
2answers
403 views

Weakening and Contraction

I saw this site saying weakening is a structural rule where the hypotheses or conclusion of a sequent may be extended with additional members and that contraction is a rule where two equal (or ...
0
votes
1answer
110 views

What is really a “complete” deductive system for first-order theories.

Given some first-order language and a set of axioms therefrom one still needs to specify a deductive system to turn it into a full-fledged first-order theory. Currently I'm under the following ...
1
vote
0answers
64 views

Is a sentence in $\Pi_1$ true given $Q \vdash \lnot\varphi$?

If $Q \vdash \lnot\varphi$ (Q is the Robinson arithmetic), and if I assume that $\varphi \in \Pi_1$; Can I say that $\varphi$ is a true sentence? My thoughts are that, given that Q is $\Sigma_1$- ...
1
vote
1answer
77 views

A simple question on Gödel's functional interpretation

I've been recently reading the Gödel's functional interpretation (or Dialectica). It is generally defined inductively, as could be found here: http://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf ...
3
votes
1answer
301 views

Problems with nesting proof predicates in first order logic.

Whenever I start nesting proof predicates, I always seems to run into these bizarre situations. I was wondering if anyone knows about this and could shed some light on it or provide me with some ...
5
votes
2answers
216 views

Is there a minimal axiomatization of ZFC?

Working in ZFC, does there exist a set $\Sigma$ of sentences which axiomatizes ZFC (i.e. every sentence in $\Sigma$ is provable from your favorite axiomatization of ZFC, and vice versa) and is minimal ...
11
votes
3answers
202 views

The category of theorems and proofs

On a philosophy website, it said that you could have a category with theorems as objects and proofs as arrows. This sounds awesome, but I couldn't find anything on the web that has both "category" and ...
4
votes
2answers
262 views

What if a conjecture were provably unprovable?

Suppose we found a proof that "The Twin Prime Conjecture cannot be proven", without any conclusion as to the conjecture itself being true or false. Is it then possible for the conjecture to be true? ...
8
votes
1answer
132 views

Is there a way to tell how many different ways you can prove a theorem?

Consider the question. Given the nature of a sentence $S$, it there any way to tell how many different ways you can prove this sentence? Proofs are not distinct if we have a situation such as: $P ...
1
vote
2answers
121 views

Is it possible to prove that the encoding of existentials in System F is valid?

In Girard's Proofs and Types, under item 11.3.5, second-order existential quantification is encoded in System F using universal quantification as follows: $$ \Sigma X.V \equiv \Pi Y. (\Pi X.(V \to ...
1
vote
0answers
112 views

Do we know that if $\pi$ is normal then there is a proof of it?

We do not know whether $\pi$ is normal or it is not and many other weaker statements, e.g. (*) $\pi$ contains infinitely many $0$s. Inspired by the Godel's incompleteness theorem that there are some ...
2
votes
2answers
220 views

What if 'proof by contradiction' is not a valid method of proof?

I've just been reading this question about the existence (or lack thereof) of contradictions in maths. I've been wondering: What if 'proof by contradiction' is not a valid method to (dis)prove a ...
4
votes
3answers
148 views

Deriving $A \rightarrow ( B \rightarrow C ) \rightarrow ( ( A \rightarrow B ) \rightarrow ( A \rightarrow C ) )$ in the sequent calculus

I need to prove the following theorem: $A\to (B\to C) \to ((A\to B) \to (A\to C))$ using the sequent calculus method. Using the rules: $$ G, A \Rightarrow B,D \over G \Rightarrow A \to B , D ...
2
votes
0answers
64 views

Can we always give a direct proof? [duplicate]

This is something I was wondering about for quite a while. Is it possible to construct a statement that can only be proven by using 'proof by contradicition' or contraposition? Or to put it ...
4
votes
2answers
119 views

Biconditional statements with an “easy” direction.

I was reading through Lax's Functional Analysis, when I came across the following statement: Theorem: X is a normed linear space over $\mathbb{R}$, $M$ a bounded subset of $X$. A point $z$ of $X$ ...
0
votes
1answer
82 views

Existential introduction - required or not?

Consider a theory $T$ in first order logic, and a formula $C$. If there exist a proof of $C$, and that all formulas in $T$ and $C$, none of them contains $\exists$. The question is: does there always ...
10
votes
1answer
248 views

Gödel's way of teaching non-standard models to Takeuti.

In Memoirs of a Proof Theorist, Gaisi Takeuti relates how Gödel taught him about nonstandard models in an "interesting" way: It went as follows. Let T be a theory with a nonstandard model. By ...
0
votes
2answers
78 views

particular property and completeness?

I was puzzeling with the almost standard definition of completeness: In mathematical logic and metalogic, a formal system is called complete with respect to a particular property if every formula ...
1
vote
0answers
46 views

A question about $KP + V = L$ and $KP$ set theory.

In reading Rathjen (Choice principles in constructive set theories) and Jager (On Feferman's OST) I've come across two facts that are taken as obvious/well known, and probably are, but for which I ...
3
votes
1answer
62 views

$HA^{\omega}$ is a conservative extension of $HA$. But why?

This is definitely a silly question, but I've no one to ask... $HA^{\omega}$ is an extension of $HA$ in all finite types. One can formalize a model of $HA^{\omega}$ in $HA$ using indicies of partial ...
3
votes
2answers
397 views

Proof that SAT is NPC

I am not really sure I understand the idea behind Cook theorem (it says that SAT is a NP-complete problem). I read the proof with all its parts corresponding to the Turing machine TM solving it (TM ...
0
votes
5answers
1k views

Prove: if x is odd, then sqrt(x) is odd.

If $x$ is odd, then $\sqrt{x}$ is odd, where $x$ is an integer. Any hints welcome and preferred. Thank you!
0
votes
1answer
86 views

Proove that cos(x / 2) + cos(y / 2) - cos(z / 2) = 4 * sin((pi - x) / 4) * sin((pi - y) / 4) * sin ((pi + z) / 4

Help me proove that cos(x / 2) + cos(y / 2) - cos(z / 2) = 4 * sin((pi - x) / 4) * sin((pi - y) / 4) * sin ((pi + z) / 4 where x + y + z = pi I've reached 2 * sin((x + z) / 4) * (cos((x + z) / 4) - ...
0
votes
5answers
118 views

Is proof by algorithm credible?

I have found this question How to prove that the inverse of a matrix is unique? And while the accepted answer is fine I was wondering if it's possible to proof the uniqueness by algorithm. There is ...
0
votes
2answers
48 views

Proving $A+2B+3C+4D < 2.5$ with given conditions

I want to prove follow inequality. Conditions: $$A+B+C+D=1$$ $$A>B>C>D>0$$ Prove: $$A+2B+3C+4D < 2.5$$ Thanks in advance.
0
votes
1answer
555 views

Formal proofs and Deduction Theorem

In this question i will explain one idea i had about basic formal proofs and the use of Deduction Theorem. I'm considering a formula γ to be a logical consequence of a set A of formulas if and only ...
3
votes
2answers
374 views

Law of excluded middle. Do we need it in proofs?

Quite often when I am making a natural deduction proof, and I have no fixed idea on how to continue. I find myself thinking: "lets start with some form of the law of the excluded middle (LEM) and ...
4
votes
2answers
132 views

Graph that represents logical reasoning

The proof of a statement $X$ in terms of assumptions $A$, $B$ and $C$ can sometimes be represented using a directed graph: $$ \begin{matrix} & & X\\ & \nearrow & & ...
12
votes
1answer
246 views

Can all math results be formalized and checked by a computer?

Can all math results, that have been correctly proven so far, be formalized and checked by a computer? If so, what type of logic would need to be used there? I've heard that the first-order logic is ...
3
votes
2answers
139 views

General view of Theorems

I'm trying to see almost all theorems ( at least the non-existential ones ) as affirming that some formula ( mostly of first-order logic language ) is a logical consequence of other formulas. So, ...
1
vote
1answer
163 views

Hilbert calculus: Proof that every provable formula has a proof

For my indroduction to logic course I have to proof, that every provable formula has a proof. It sounds first very funny, second also very logic, still I don't get to make of formally work.. The ...
0
votes
1answer
37 views

Proving that operations give equal results given equal inputs

I was reading about the 9 or 12 basic properties of 'fields' (if that's what they're called) in a book called Spivak's Calculus, 3rd Edition, and got quite befuddled by dealing with as basic stuff as ...