# Tag Info

1

A proof system is a Formal system with logical axiom (possibly none) and rules of inference (at least one). Some examples : Hilbert-style proof system : usually more than one (logical) axioms and few rules : modus ponens and generalization. See Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 109, for a system with few axioms ...

3

No theory containing at least the peano axioms can prove its own consistency (proven by Gödel). But there can be a stronger theory proving the consistency of the weaker theory. The catch is, to prove the consistency of the stronger theory, you need an even stronger one. ZFC is believed to be consistence and can be used to prove the consistency of PA. To be ...

0

Provided your language is countable, then the answer is yes, though this answer has little to do with automated theorem proving. Let $T$ be a theory in a countable language $L$. Then the set of sentences in $L$ is countable, so the set of finite sequences of sentences in $L$ is countable. Hence the set of proofs of $T$-provable sentences is countable. So ...

0

An algorithm can enumerate all consequences of the axioms, and so eventually list all the provable statements and all the disprovable statements. An algorithm can take any non-independent statement and (if it really is not independent) determine if the statement, or its negation, has a proof. An algorithm cannot tell, given an arbitrary statement, whether ...

1

If you are going to bring in the question of bugs, then no: there is no way to use any program to prove any conjecture, ever. Even if it is open source, being able to look at the code doesn't insure it works properly. A bug could be inherent in the programming language even! If you are willing to trust software, then you need to make some theoretical ...

0

Very simple: if $x<0$, $x<0<\lvert x\rvert$; if $x\ge 0$, $\lvert x\rvert =x$, a fortiori, $\lvert x\rvert \ge x$.

1

Just go back to the definition : $$|x| = \left\{\begin{array} .x & \text{if} & x\geq 0 \\ -x & \text{if} & x< 0 \end{array} \right.$$ So if $x\geq 0, |x| = x \geq x$ if $x< 0, |x| = -x > 0 \geq x$ Hence $\forall x \in \mathbb{R}, |x| \geq x$ Note that you can also define $|x| = \max\{ x, -x\}$ and the result is then ...

0

First note that we can assume that $a=1$ so we have $f(x,y,z)=xyz+b(xy+yz+zx)+c(x+y+z)+d$. We have that $xyz+r(xy+yz+zx)+r^2(x+y+z)+r^3=(x+r)(y+r)(z+r)$ for the if part. Noe looking at this as an expression polynomial in $x$ it has degree $1$. Because we can invert scalars any factorisation will be of the form $$B(x+A)$$ where $A,B$ are polynomial in ...

1

It's nice question, and little hard too, and I think it's Olympiad question, I wounder from what Olympiad did you take this question?, This is my solution : Suppose that $f$ is reducible. Therefore it has a factor $g$ of degree $1$. Suppose that $g$ is symmetric. We may assume that $$g = x + y + z + k$$ for some constant $k.$ Now put $x = 0$, so y ... 0 We have: \begin{align*} f(x,y,z) & = axyz + b(xy + yz + zx) + c(x + y + z) + d.\\ & = axyz + b(xy) + b(yz + zx) + c(x+y)+ cz + d\\ & = xy(az+b) + (x+y)(bz+c) + (cz+d)\\ \end {align*} The only way we can make it reduce further is if(az+b), (bz+c)$and$(cz+d)$are related geometrically, i.e.,$(bz+c)$and$(cz+d)\$ are of the type ...

2

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

Top 50 recent answers are included