# Tag Info

1

It's sometimes possible to show existence of proof of a statement in ZF by showing that the statement is true in ZFC, and arguing using absoluteness. An example would be answer to this question, in which Andreas Blass argues as follows: for any model of ZF, Monsky's theorem holds in an inner model satisfying axiom of choice, and this statement is "simple ...

1

Many. Such questions amount to some finite computation, since you can just search for a proof and simultaneously disproof until you find (enumerate all proofs and check if its a proof or disproof). So just pick one which requires a large computation such as; Is there an odd number of pairs of twin primes below 10^999999999999999 ? This is provable, just ...

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 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". ... 3 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 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 ... -2 Ok I found the answer in the textbook. If$x = \frac{b}{c}$and$gcd (b,c) = 1$then if$x^n = a$implies that$b^n = ac^n$but since$b$and$c$have no common divisor then$c$must be$1$which proves the theorem. Thanks for your help and effort. 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 ... 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 ... 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 ... 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 ... 0 If you like, you can do this as an exercise in proof by infinite descent. Suppose there were such an$x$. Since we're squaring it, we can assume$x\ge0$, and it's easy to see that we can assume$x\ge3$as well, since$4$,$5$, and$8$are not divisible by$3$. But if$x^2+4=3k$, then $$(x-3)^2+4=x^2+4-6x+9=3(k+2x+3)$$ which means there is no minimal ... 0 Assume that$x^4 +4$is divisible by$3$. Then$x^2 + 1 = (x^2 +4) -3$is divisible by$3$. Now (following http://math.stackexchange.com/a/630761/26188) you have that one of the following is divisible by$3$:$x-1xx+1$. If$x$is divisible by$3$, then so is$x^2$and so$x^2 + 1$would not be divisible by$3$. If$x$is not divisible by$3$, then ... 0 $$x \equiv 0 \equiv 1 \equiv -1 \pmod{3} \space \text{for all cases}$$ Then: $$x^2 \equiv 0 \equiv 1 \equiv 1 \pmod{3}$$ In any of the cases, $$4 \equiv 1 \pmod{3}$$ $$x^2 + 4 \equiv 1 \equiv 2 \equiv 2 \pmod{3}$$ ALSO: $$x^2 + 4 = (x + 2)^2 - 4x$$ Suppose it is divisible by$3$then, $$x + 2 \equiv 2\sqrt{x} \pmod{3}$$ But$\sqrt{x}\$ isn't ...

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

No. At least not how most mathematicians interpret the term theorem. Some logicians might regard their notions of what constitutes a theorem as wrongheaded, but that isn't the issue here. Notice that the Metamath people say things like this: "... it certainly doesn't help us make progress towards a proof of ( 2 + 2 ) = 4" So, almost surely, terms have ...

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. ...

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 ...

Top 50 recent answers are included