Are inference laws consistent? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-24T08:11:42Z http://mathoverflow.net/feeds/question/68524 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/68524/are-inference-laws-consistent Are inference laws consistent? Qfwfq 2011-06-22T15:18:41Z 2011-06-22T18:21:41Z <p>Please forgive me if this question sounds too naive... Well, in mathematics a <em>formal theory</em> consists of a collection of axioms $T$ (such as Peano arithmetics, or Group Theory, or ZFC), which essentially are certain structured chains of symbols, and theorems can be derived from them by applying certain deduction rules (or "inference laws"). These deduction rules are themselves formalizable by some axioms $\Lambda$ (such as the Hilbert-Frege deduction system). </p> <p>Gödel's second incompleteness theorem states, roughly, that we cannot <em>prove</em> (and, to be able to <em>prove</em> something, we leave some fixed inference laws $\Lambda$ as understood) the consistency of any set of axioms $T$ (working within $T$). </p> <blockquote> <p>What about the consistency of the inference system $\Lambda$ itself alone? That is, does Gödel's theorem apply somehow also to $\Lambda$ so that nobody is able to "prove" that it will not lead to a contradiction? </p> </blockquote> http://mathoverflow.net/questions/68524/are-inference-laws-consistent/68526#68526 Answer by Emil Jeřábek for Are inference laws consistent? Emil Jeřábek 2011-06-22T15:42:15Z 2011-06-22T15:42:15Z <p>First, Gödel’s theorem says only that the theory itself cannot prove its own consistency (under some assumptions). It’s perfectly possible (and not particularly difficult) to prove the consistency of, say, Peano arithmetic (in usual mathematics, i.e., in ZFC).</p> <p>Likewise, we can prove the consistency of the predicate calculus without non-logical axioms (your $\Lambda$). One possibility is as follows: take a proof of contradiction, and show by induction on the length of proof that all formulas in the proof are valid in the one-element model which does not satisfy any predicates. (Note that satisfaction in a one-element model is easy to define, as it’s essentially just propositional logic: you can ignore quantifiers and terms.)</p> <p>If you are more syntactically-minded, you can also regard this as a reduction of first-order logic to variable-free propositional logic: strip all quantifiers, and replace all atomic formulas with $\bot$ (or any fixed false formula, if you do not have $\bot$ in the basic list of connectives). Then it suffices to show the consistency of (the variable-free fragment of) propositional calculus.</p> http://mathoverflow.net/questions/68524/are-inference-laws-consistent/68532#68532 Answer by Joel David Hamkins for Are inference laws consistent? Joel David Hamkins 2011-06-22T16:32:48Z 2011-06-22T16:32:48Z <p>A somewhat stronger property than mere consistency, which is universally desired in a proof system, is the property of <a href="http://en.wikipedia.org/wiki/Soundness" rel="nofollow">soundness</a>. </p> <p>A formal system is <em>sound</em>, if whenever it proves a statement $\varphi$ from some axioms $T$, then indeed $\varphi$ is true in any model satisfying $T$. In particular, when $T$ is the empty theory, then we want every statement $\varphi$ proved in the system to be true in every structure. This is usually very easy to prove for a given formal system, usually by induction on the length of the proof, simply by observing that the inference rules are truth-preserving. In contrast, the formal system is <em>complete</em> if it succeeds in proving $\varphi$ from $T$ whenever $\varphi$ is true in all models of $T$, and this is the nontrivial part of the completeness theorem.</p> http://mathoverflow.net/questions/68524/are-inference-laws-consistent/68540#68540 Answer by Timothy Chow for Are inference laws consistent? Timothy Chow 2011-06-22T17:35:29Z 2011-06-22T17:35:29Z <p>If I understand your question correctly, you're wondering whether the consistency of first-order logic without any axioms can be proved using first-order logic, without assuming any axioms.</p> <p>The trouble is that if you don't allow yourself any axioms, then it's unclear how you would even <i>express</i> the statement "first-order logic is consistent." The reason that Goedel's incompleteness theorem applies to systems that encode at least a minimal amount of arithmetic is so that you can encode concepts such as "axiom" and "inference rule," without which we cannot even define what "consistency" means.</p> http://mathoverflow.net/questions/68524/are-inference-laws-consistent/68541#68541 Answer by Gyorgy Sereny for Are inference laws consistent? Gyorgy Sereny 2011-06-22T18:09:01Z 2011-06-22T18:21:41Z <p>First, a remark. You formulate both Gödel's theorem and your question in a subjective way "we cannot prove", etc. However, this theorem is a mathematical one, therefore it is not about our ability to do something, but about the nonexistence of a mathematical object, namely a formal proof within the system concerned. You can draw some e.g. philosophical conclusions from this theorem, but this is a completely another matter. </p> <p>Now, as far as your question concerned, it is almost certain that nothing analogous to Gödel's theorem <em>can even be stated</em> for the pure first order logic itself. The reason is simple. The analogous theorem would claim the unprovability of the formula expressing the the fact that a contradiction is unprovable <em>within the pure first order logic</em>. But, in the absence of the formal provability predicate, this theorem cannot even be stated. Actually, what we would like to show is that there is a formula $Pr(x)$ such that, on the one hand, it can be considered a provability predicate (that is, for any formula $\varphi$, $Pr(\ulcorner \varphi \urcorner)$ is true just in case $\vdash \varphi$ (here, of course, $\ulcorner \varphi \urcorner$ is the Gödel number of $\varphi$), on the other hand, the formula expressing the fact that a contradiction is unprovable is itself unprovable: $\not\vdash \lnot Pr(\ulcorner 0=1\urcorner)$. Now, the proof of the existence of a provability predicate seems to require much more than pure logic.</p>