# Tag Info

5

The solution is nothing more than some computation and observing $2\cdot27 = 90 - 36.$ \begin{align*} \tan^2(27^\circ) + 2 \tan(27 ^ \circ) \tan (36^\circ) &= \tan^2(27^\circ) + 2 \tan(27 ^ \circ) \cot (54^\circ) \\[1ex] &= \tan^2(27^\circ) + 2 \, \frac{\tan(27 ^ \circ)}{ \tan(54^\circ)} \\[1ex] &= \tan^2(27^\circ) + 2 \, \frac{\tan(27 ^ ...

5

So I don't know about Karp's work in this setting (and google doesn't seem to know either), but I do know that Lopez-Escobar developed a proof system for $L_{\omega_1\omega}$. I believe this was originally done in his Ph.D. thesis, "Infinitely long formulas with countable quantifier degrees," which I don't have access to. However, his paper ...

3

Definition: A waterfall is a system of differential equations of the form$\cdots\cdots\cdots$. [fluid mechanics stuff] $\blacksquare$ But that's not a waterfall; that a mathematical model of a waterfall. Likewise proofs studied in mathematical logic, written in a form suitable to submit them to proof-checking software, are not proofs; rather, formal ...

3

The paper does not claim that automated theorem provers cannot handle the case of such arguments, and indeed shows how to formalize them. The fact is that humans do not write proofs in the same way that ATPs do - very much is left for the reader to do. Indeed, this often rises to the level of little lemmas that could have their own proofs, and the author may ...

3

Robert's hint is superb. Full solution: If $k$ is the leftmost digit of $n$ then the number resulting from removing the leftmost digit of $n$ is congruent to $n-k\bmod 9$. Hence if we add $k$ to this number we obtain a number congruent to $n\bmod 9$. Conclusion: The congruence $\bmod 9$ is invariant under the operation of removing the leftmost digit of $n$ ...

2

Your "statement" is false as it stands. An easy counter-example is taking $n=2$ and $a=2$ to get $x = \sqrt{2} \neq \frac{a}{b}$ since $\sqrt{2}$ is irrational. Another counter-example would be $n=2$, $a=3, 5, 6, 7, 8, 10, \ldots$ the list goes on. Due to this, it's going to be quite hard to prove your (untrue) statement. Mainly because such a proof is ...

2

Example: Consider the statement: If it is raining, then it is cloud. $Raining \implies Cloudy$ This does not mean that rain causes cloudiness, or that cloudiness causes rain. Neither is the case. It means only that it is not both raining and not cloudy. $\neg [Raining \land \neg Cloudy]$ In mathematics then, if not in everyday usage, $A\implies B\equiv ... 2 The metamath website does contain the somewhat brash claim: Essentially everything that is possible to know in mathematics can be derived from a handful of axioms known as Zermelo-Fraenkel set theory, which is the culmination of many years of effort to isolate the essential nature of mathematics and is one of the most profound achievements of mankind. ... 2 By the Unique Factorization Theorem, it is enough to prove the result for integers$a, b, c$which are each powers of a prime$p$. Let$a=p^\alpha$,$b=p^\beta$, and$c=p^\gamma$. Without loss of generality we may assume that$0\le \alpha\le \beta\le \gamma$. Then$\text{lcm}(ab,bc,ca)=p^{\beta+\gamma}$and$\gcd(a,b,c)=p^\alpha$, so the product is ... 2 If you have a contradiction as a premise (or a correctly deduced conclusion from contradictory premises), then you are allowed to deduce anything you want through ⊥ elimination. Assuming a contradiction is no different than assuming what you want to conclude though, so I'm not sure what the point of assuming the contradiction is. "Modern" logic: If you ... 2 Not knowing how much mathematics experience you've had, it can be difficult to explain the difference in viewpoint. Intutionism, and constructive logic in general, are very much inspired by the fact that we as mathematicians do not know the answers to all mathematical questions. Classical logic is based on the idea that all mathematical statements are ... 2 Intuitionistic logic, a.k.a. constructive logic, differs from classic logic in that it focuses on 'provability' of a statement rather than 'truth'. In classical logic, all propositions are considered to be either true or false; one xor the other. However in constructive logic, a proposition is only ever considered definitely true or false if it can ... 1 If you could prove the law of the excluded middle, then it would be true in all systems satisfying intuitionistic axioms. So we just need to find some model of intuitionistic logic for which the law of the excluded middle fails. Let$X$be a topological space. A proposition will consist of an open set, where$X$is "true", and$\emptyset$is "false". ... 1 If you add to Peano arithmetic the negation of a theorem whose shortest proof is very long, then you've got it. There can be no finite upper bound on the ratio of the length of the shortest proof of a theorem to the length of the theorem. Suppose there were such a bound$B$. Then, since only finitely many sequences of characters have length less than$B$... 1 Yes, of course it's conceivable. Suppose we have a consistent system$S$that has a short theorem$T$whose shortest proof is very long. Consider the inconsistent system$S'$obtained from$S$by adjoining the axiom$\neg T$. From any proof of$A \wedge \neg A$in$S'$you can produce (without much increase in length) a proof of$T \implies (A \wedge \neg ...

1

Does the proof writing in first-order logic "precede" the ordinary proof writing used in mathematics [. . .] I think there are different understandings of "proof" and of "precede". "Proof" in formal logic has a technical sense referring to a symbol sequence satisfying certain formal rules. However, "proof" in ordinary English (the original sense of the ...

1

Your question as asked prompts good answers pointing to the study of foundations, the history of mathematics and the philosophy of mathematics. You may be asking (as a student) about how working mathematicians answer your question. I think the answer is that most don't. You write proofs to convince yourself and other mathematicians that what you've ...

1

Technically, you can't say anything about what would happen in domain B. Depending on the domains, and the optimization problems, the optimization problem 2 could be defined in such a way that it is easy in domain A but NP-hard in domain B, or easy in both domains even though your "tool" as you say doesn't work in domain B. As far as determining what's ...

1

Well, it turns out the type of le_n is indeed a dependent product: le_n : ∀ (n : nat), n ≤ n The fact that it is displayed as a function with named arguments is syntactic sugar. In fact, when I check le_n in my version of Coq it displays this: le_n : forall n : nat, n <= n And whenever you write something like this: Definition f (a1 : T1) (a2 ...

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