# Tag Info

9

One of the computability results is that there must exist provable theorems in number theory that require very long proofs relative to their statements. If $n$ is the encoding of a statement in number theory which can be proven, and $f(n)$ is the length of the shortest proof of that statement, then the function $$G(n)=\max \{f(k): k\leq n, k \text{ encodes ... 6 For any integer x, exactly one of \{x, x+1\} is even. Now factor x^2 + x. 4 I have worked with Mizar for over two years now and studied it basically on my own (with the help of your mentioned references as well as getting answers to occasional questions about errors I couldn't grasp answered by the very helpful Mizar User Service (see)). I'm about to submit my forth article to the MML these days and when I started I encountered ... 4 The fact that such a program exists is actually an important concept, in fields such as foundations of mathematics, computability theory and complexity theory. Foundations: When you want to reason about mathematics in general, you can either fix an axiomatic system, such as ZF (or a variant like ZFC), or take a general one. However, when you consider a ... 4 If the question asked is (i.e., the first fraction inside the sum is \frac{n}{r} instead of \frac{n}{r+1}) as follows, it makes sense. \begin{eqnarray*} \sum_{i+r=n}{ \frac{n}{r} \binom{n-1}{r-1} \binom{n-r}{i} (-1)^{i}} &=& 1\\ \end{eqnarray*} This comes straightforward from multinomial expansion. \begin{eqnarray*} \left(x_{1}+x_{2}+x_{3}... 4 The proof-checker CalcCheck takes input via \TeX{} in the form of formulas and accompanying English hints/justifications. Given the input file, the system will output that the proof is valid at all steps or indicate which steps are poorly justified. To the best of my knowledge, it currently recognizes most theorems of first order logic and set theory ---... 3 Let g=f^2. Then g has a periodic point of period 2. Can you finish? 3 These axioms are sufficient. Here's an outline of the proof in natural language: Since x\leq s(s(0)), there exists z such that x + z = s(s(0)). Case 1: z = 0. Then x = x + z = s(s(0)), and we're done (x = 2). [Note that you've stated as an axiom \text{add}(x,0) = 0, and I assume you meant \text{add}(x,0) = x!] Case 2: z\neq 0. Then ... 3 Part of what you seem to be talking about is either computability theory (also called recursion theory) or complexity theory, depending on whether or not the problems you're interested in are solvable by a computer. If you're primarily interested in solvable problems, complexity theory considers which problems can be used to efficiently solve other problems. ... 3 The short answer is that almost all mathematicians do not write proofs in a sufficiently formalized manner, because they rely on the intelligence of other mathematicians who read their proofs. It is not an issue of unambiguous formatting (type-setting), but an issue of strictly enforced structure and syntax, in much the same way as a compiler will reject a ... 3 Inductive proofs can only directly prove properties of the set of finite initial subsequences of streams - it cannot directly prove anything about infinite streams. This is because the induction only "reaches" well-founded elements of the type constructor, while coinductive proofs reach all of these elements and the ill-founded elements, such as the ... 3 It is reasonable to believe that everything that has been (or can be) formally proved can bew proved in such an explicitly formal way that a "stupid" proof verification system can give its thumbs up. In fact, while typical everyday proofs may have some informal handwaving parts in them, these should always be able to be formalized in a so "obvious" manner ... 3 For the first part, as I pointed out in the hints, the integrand is decreasing, as x^{n+1} \le x^n for x between 0 and 1. Therefore, a_n is also decreasing. For the second part, try integration by parts. The trick is to view the function as$$x^{n-1} \cdot x (1 - x^2)^{1/2}.Then, \begin{align*} a_n &= \int_0^1 x^{n-1} \cdot x (1 - x^2)^{1/2}... 2 As you pointed out in the comments, a primality certificate is essentially what you're looking for: it's a compression of the proof that a particular number is prime. The Pratt certificate for N, for instance, relies on a witness a < N, the prime factorization q_1^{a_1}q_2^{a_2}\ldots q_k^{a_k}=N-1, and the following facts: a is coprime to N ... 2 Here's a formal proof, copied and pasted from my Fitch software program (sorry for the lack of formatting!) which says it all checks out .. meaning that no: you don't need any further axioms (I did use all 9 axioms). It follows Alex's more informal proof: Nat(0) Axiom ∀x (Nat(x) → Nat(s(x))) Axiom ∀x ∀y ((Nat(x) ∧ Nat(y)) → Nat(x + y)) Axiom ∀x (Nat(x) ... 2(n+n^2)\bmod2=((n\bmod2)+(n\bmod2)^2)\bmod2=((n\bmod2)+(n\bmod2))\bmod2=0.$$2$$(2n)+(2n)^2=2n+4n^2=2(n+2n^2)$$and$$(2n+1)+(2n+1)^2=2n+1+4n^2+4n+1=2(1+3n+2n^2).$$1 The proof that the term \text{pred} encodes the predecessor function over natural numbers is quite technical and requires a lemma. For any n \in \mathbb{N}, let \underline{n} = \lambda f \lambda x. f^{n} x = \lambda f \lambda x. \overbrace{f (\cdots (f}^{n \text{ times}} x) \cdots) (in particular, \underline{0} = \lambda f \lambda x.x). Lemma. ... 1 Of course. If "greater than" is true, then "greater than or equal to" is true. Look at the truth table under OR here: https://medium.com/i-math/intro-to-truth-tables-boolean-algebra-73b331dd9b94. 1 Your answer for 2 dimensions can be true even for d>2. Consider the vectors: (1, 0, 0, ..., 0) (0, 1, 0, ..., 0) (1, 1, 0, ..., 0) You can't have w1, w2 s.t. w_1>0, w_2 >0 w_1 + w_2 \leq 0 edit: this is for the equations that you posted for when b=0, for b \neq 0, see Arthur's answer 1 By induction,$$1+1^2=2$$and$$n+n^2=2k\implies n+1+(n+1)^2=n+n^2+2n+2=2(k+n+1)=2k'.

1

As pointed out by commenter ThorbenK, Case 1: $x$ even. Then $x^2$ is even, and the sum of even numbers is even. Case 2: $x$ odd. Then $x^2$ is odd, and the sum of two odd numbers is even.

1

$\forall x : A \implies B \land B \implies \lnot A$ can be combined to say $\forall x : A \implies \lnot A$ $\therefore \forall x :\lnot A$ similarly, $\forall x :\lnot B$ now, $\exists x : B \implies A$ is always the same as $\exists x : False \implies False$. "if False, then False" is vacuously true. In this case not just for some x but for all x. You ...

1

You might look at the Flyspeck project. That involved a lot of analysis.

1

Finally , the answer : enter image description here and the proof: enter image description here

1

You also need: $\forall x (Member(Club1,x) \rightarrow (x = John \lor x = Mary \lor x = Helen \lor x = George))$ Since these four are the only members of the club, i.e. there are no others! Also, let's make sure they are all different people: $John \not = Mary$ $John \not = Helen$ $John \not = George$ $Mary \not= Helen$ $Mary \not = George$ \$Helen \...

1

I am working in a version of ZFC set theory that attempts to formalize the notion of context used in mathematics textbooks at undergraduate and graduate level. It is named Contextual ZFC or CZFC. By trying to achieve this goal, I found myself working in three separate but very related lines: 1) Developing an implementation of CZFC, a language I named ...

1

I like Prover9 for theorem proving. I think OTTER is better for some purposes.

1

In my course of mathematical logic we use this: http://www.spass-prover.org/

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