29
$\begingroup$

I'm reading some materials on mathematical logic. I wonder how we can "prove" metalogical properties (soundness, completeness, etc.)? As at this point, the proof system has not been verified yet. Isn't this a chicken-and-egg question (we may then have meta-metalogic)? What types of proofs are considered valid at this stage?

$\endgroup$
  • $\begingroup$ +1 I like your question. Meta-maths is not my area of knowledge, let alone the philosophy behind it, but I think Munchhausen's trilemma is going to forbid having a non-circular, self-justified system, unless it's some kind of infinite regression (meta-maths, meta-meta-maths, meta-meta-meta-maths, etc). $\endgroup$ – Theo Bendit Jun 26 '17 at 21:50
  • $\begingroup$ I think this may be a duplicate of math.stackexchange.com/questions/201703/… but I will let others vote if they agree. $\endgroup$ – Carl Mummert Jun 27 '17 at 0:37
  • 2
    $\begingroup$ a) Yes, there is a building of meta-meta-meta-logic. b) I saw your title as "How are metallurgic proofs valid?". ;) $\endgroup$ – AnoE Jun 27 '17 at 9:39
  • $\begingroup$ Isn't soundness a definition and not something to be proved? A theory is sound when all proofs in the theory are sound (that is their premises is true, and the implication is valid (valid meaning the consequent must be true when the antecedent is)). $\endgroup$ – user400188 Jun 28 '17 at 1:12
22
$\begingroup$

Short answer: yes, it is essentially a chicken-and-egg problem, or perhaps a hermeneutical circle or a spiral. The common interpretation of the incompleteness theorems is that this circularity cannot be avoided.

You can use normal mathematical reasoning for the metatheory - which is not formalized in the first place - or you can choose some formal theory. In the latter case, you can choose a stronger metatheory, like ZFC, or a weaker one, like PRA.

In principle, you would then be able to choose a meta-metatheory, a meta-meta-metatheory, etc., but in practice essentially all the interesting issues arrive at the theory/metatheory level, and the higher levels just repeat these issues rather than giving new issues.

$\endgroup$
15
$\begingroup$

This is actually not a disagreement with Carl Mummert's answer, but another way of thinking about it. No, it isn't circular. But you don't prove what you might imagine you prove.

All actual proofs in mathematics are in what we call "mathematical English" -- we believe this is all completely rock solid, but essentially it is in the form of sentences and paragraphs and so on. Sometimes (rarely) you even diagram those sentences and break them down into something that looks more like formulas, and follow rigid rules (see Russell's "game on paper" interpretation of math), but ultimately the idea is to be "completely convinced" that a statement is true.

The informality of the above is completely necessary and unavoidable!

When we "prove theorems about theorems" or any other meta-mathematical idea, what we really do is design (in our informal mathematical English) a model where we represent statements as numbers, and so on, so that we can say "this number represents a sentence" and "this number represents a proof of this statement from this set of statements" and so on, we're actually making a statement about numbers.

You convince yourself that this statement about the natural numbers is really the same as the metamathematical statement you care about. This can't be formalized either, but should be seen as "obvious" once explained properly. Then you can prove this statement about numbers in the normal mathematical sense.

$\endgroup$
  • $\begingroup$ "Necessary" and "unavoidable" are not the same as "valid" and "justifiable". Does mathematics have more intrinsic validity than just how convincingly it is explained? $\endgroup$ – Theo Bendit Jun 27 '17 at 2:57
  • 1
    $\begingroup$ @TheoBendit Depends on who you ask. Many people believe that (a) proofs done at the extreme standard of Russell's "game on paper" are completely valid and trustworthy, and that (b) all correct mathematical proofs can be expanded to the standard of the "game on paper" [in fact they would argue that this is what "correct" means]. If you believe (a) and (b) then mathematics is "valid." But [cont] $\endgroup$ – Richard Rast Jun 27 '17 at 12:55
  • 1
    $\begingroup$ [from cont] in the end we're all communicating in some natural language which is necessarily ambiguous and imprecise, and relying on an (unprovable!) belief in rules (a) and (b) above to decide that math is trustworthy. Empirically it seems to be working well so far :P $\endgroup$ – Richard Rast Jun 27 '17 at 12:57
  • $\begingroup$ I don't see how proofs are what you call 'mathematical English'. If something is proven, then it has a truth value of true. We do not simply belive it to be true. If you think this truth value is not absolute, you need only look at the logic gates on computers, or any line of code that involves truth values. The machine doesn't simply change its mind; it will not output from a gate something that does not logically follow from the input and the gate itself, or execute a false line of code. $\endgroup$ – user400188 Jun 28 '17 at 1:41
  • $\begingroup$ @user400188 I'm not clear on what your comment means. You're talking about proofs, but then you're talking about computers which are, in this case, physical objects and not proofs. There isn't really a "truth value" here. There is a physical sense of truth for a computer (or at least usually-easily-distinguished states which we call "true" and "false"), but that's not really the same thing. $\endgroup$ – Richard Rast Jun 28 '17 at 2:19
12
$\begingroup$

I think Richard Rast's answer is basically right, but I want to add a little to it.

Ordinary logic, as practiced by mathematicians, studies a formalized copy of mathematics. It studies that copy using the same tools, and the same level of rigor, as any other field of mathematics. People get confused about this because the object being studied and the tools being used to study it look so similar.

For instance, the soundness theorem specifies a relationship between certain combinatorial objects (proofs) and certain algebraic objects (models). In mathematical logic, the fact that these objects remind us mathematical proofs has no bearing on what constitutes a proof: the standard of validity is the same as for any other combinatorial proof.

Using logic as a philosophical foundation for mathematics is a more delicate task, and is fundamentally a philosophical project, not a mathematical one, though it obviously has to be heavily informed by mathematical ideas. There, as in any other attempt at a foundation for mathematics, the question of what can be taken as basic and what gets built on top of what is very difficult. In particular, materials on mathematical logic don't generally concern themselves with these issues.

$\endgroup$
-2
$\begingroup$

Yes, it's all circular. You can have weird cases (maybe not in math), were you are proving metatheoretical stuff in a different logic (many sorted, polivalued, second order, etc.), but your theory is in first order. In math this never happens, as far as i know, but in logic people do these weird combinations. But again in these cases are kind'a cirular because you have to know the theory of your metatheory, so one assumes it.

$\endgroup$
  • 3
    $\begingroup$ Downvoted for drawing a false distinction between logic and math. Also, this isn't really circular, it's a question of deciding exactly what your theorem means, and proving that (in the same sense that you prove anything else in mathematics). $\endgroup$ – Richard Rast Jun 27 '17 at 2:25
  • $\begingroup$ @RichardRast I do think there's a distinciton between logic and math. Leaving that behind, i did not say that when i wrote my answer. I paraphrase: not all logicians devote themselves to math, but they use circular thinking. And not all mathematicians devote themselves to logic, and when they do, they use this chicken-egg thinking. $\endgroup$ – edgar alonso Jun 27 '17 at 16:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.