# Tag Info

## Hot answers tagged proof-theory

18

There are various ways to interpret the question. One interesting class of examples consists of "speed up" theorems. These generally involve two formal systems, $T_1$ and $T_2$, and family of statements which are provable in both $T_1$ and $T_2$, but for which the shortest formal proofs in $T_1$ are much longer than the shortest formal proofs in $T_2$. One ...

10

Henkin's completeness proof is an example of what you seek: It demonstrates that for a certain statement there is a proof, but does not establish what that proof is.

8

One can prove that either there is a proof that $1361$ is prime or a proof that $1361$ is composite without knowing which alternative is right. But what if I can prove that there is a proof that $X$, where $X$ is some proposition? Is that a proof of $X$? In one sense it is: it is a convincing argument showing that $X$ must be true. However, logicians ...

7

I'd like to expand Brian Tung's answer above, and add a further example. In the following I'll be talking about first order (FO) sentences and structures. In a nutshell, a FO structure is a set $A$ with some operations and relations attached to it (e.g., a group, an ordered field, a graph), and a FO sentence is a statement you can write about $A$ with the ...

6

There are two different notions of proof that other answers did not distinguish. Proofs from 'without' One is when we are in a meta-system and talking about proofs inside a formal system. For example, the completeness theorem for first-order logic says that for any set $S$ of formulae and formula $φ$, we have $S \vdash φ$ if and only if $S \vDash φ$, which ...

4

There are many proofs, in fact, I have seen a book with a title like "100 Proofs of the Pythagorean Theorem." One of the proofs listed there was developed by a President of the United States (Grover Cleveland). Here is a site with many proofs: http://www.cut-the-knot.org/pythagoras/ The first proof I did (and I am obviously not the first one to find this ...

2

If you take a purely mechanical notion of "proof" as suggested in some of the comments, then yes, there are lots of "different" proofs for any given theorem. If a "proof" is just a sequence of statements, starting with assumptions/axioms, where each subsequent statement logically follows from those before it, and the last statement is the conclusion of the ...

2

If $x+y=0$ then we have \eqalign{x &=x+0\cr &=x+yy'\cr &=(x+y)(x+y')\cr &=0(x+y')\cr &=0\ .\cr}

1

I'm not sure if anyone has tried to make a direct connection (probably they have, though not quite in these terms), but there is a very straightforward indirect connection. Local soundness and local completeness are the triangle identities of the adjunctions that define logical connectives; parallel, no junk and no noise are also represented by the triangle ...

1

First, you need the statement you are trying to prove to be correct. You want your sums to go up to an even number, not to an odd number. If you look at your examples the highest power on the right is even. The power of $b$ on the right should be one greater than the upper limit of the sum. You also start the sum with $1=b^0$, so the lower limit of the ...

1

Let's pose $$A_s = \sum_{k=1}^{2s+1} (-b)^{2s+1-k} = \frac{b^{2s+1}+1}{b+1}.$$ We start from $A_1$: $$A_1 = b^2-b+1 = \frac{b^3+1}{b+1} = \frac{b^{2s+1}+1}{b+1}.$$ Now we need to find the inductive rule. $$A_{s+1} = \sum_{k=1}^{2(s+1)+1} (-b)^{2(s+1)+1-k} = \sum_{k=1}^{2s+3} (-b)^{2s+3-k} = \\ = \sum_{k=1}^{2s+1} (-b)^{2s+3-k} + (-b)^{2s+3-(2s+2)} + ... 1 Here's some structure: Your base case is when the list is null. Assume that the property holds for a list of length n, and look at lists of length n + 1. Now we can split the list into head and tail. The tail is a list of length n. Apply the above definitions, but keep in mind that a = b. Let me know in the comments if you'd like a hint. 1 If the measure of the angle can be divided by two, then there is a bisector. Since any number can be divided by two, then any angle has a bisector. Edit: I found another question similar to this one that you asked, but it was about midpoints and line segments. You could just apply the same thing written here. 1 Here's an informal sketch. Assume we've proved A and \neg A, and fix any proposition P. Then we have$$\neg P\implies \neg A, since we have the stronger proposition $\neg A$ (this uses AX1). Similarly, we have $\neg P\implies A$. So by AX3, we have $P$.

1

You can only find proofs for any given valid formula, if your calculus is complete. Under the precondition that your calculus is complete, it is possible to create an algorithm that will terminate for every valid formula. However, if your language is undecidable (e.g. first-order logic), you cannot find an algorithm that will terminate for every (valid and ...

Only top voted, non community-wiki answers of a minimum length are eligible