# Formal logic systems, how do we prove theorems about them?

One of the reasons for the existence of formal logic systems is to establish the foundations of mathematics. To have all theories constructed and proven using particular syntactic rules based on a proof theory.

If so, how do we prove that a formal logic system satisfies a certain property, Soundness for example? We can't use the rules of deduction defined in our formal logic system on itself (we haven't established its validity yet), so we have to write a proof in "human" language before we can use the system.

How can this make sense? Foundations of mathematics now rely on "human" informal language proofs at its base.

-
I think this is the goal of metatheory. – gary Sep 2 '11 at 22:47
@gary - using metatheory brings up the same question again. Can I trust the metatheory? is it consistent? and so on – leolol Sep 4 '11 at 8:32
@leolol: please consider registering your account. Unregistered accounts sometimes get disassociated when you change computers or IP addresses, and results in duplicated accounts and your being unable to comment on your own question. I've merged your two accounts for now, but if you don't register, something similar may happen again in the future. – Willie Wong Sep 4 '11 at 11:47
@leolol: yes; it is the same as the issue of infinite regress, and I don't see how it can be avoided. – gary Sep 11 '11 at 3:55

Informal language is (informally) considered as a "shortcut" that can be, in principle, translated to formal logic. So, in theory, we're never relying on human language, though in practice, one rarely actually writes a formal proof (though there are large-scale project for doing exactly this using the help of computers).

In the beginning of the 20th century, some people though that it is important to lay mathematics on a formal foundation; other people disagreed. From the point of view of the acting mathematician, foundations are only needed if they're your specialty. Occasionally they come into play, and they definitely cannot be ignored - math has turned into such a game - but they're normally left in the shadow.

At any rate, the dream was shattered by Gödel, who proved that a non-trivial (in some exact sense) proof system cannot prove its own consistency, let alone the consistency of a stronger system. So for all we know, math is inconsistent as usually thought of. Will that be so bad? Not really. Perhaps some "foundations" stuff will have to be revised, but $\sin^2\alpha + \cos^2\alpha = 1$ will stay true nonetheless.

When people do prove theorems about proof systems, they always "work" in a stronger proof system, which can be taken formally as some subset of ZFC in most cases (but we shouldn't really care most of the time). This is why we can only prove unconditional results about weak proof systems. Stronger results are relative, for example all forcing arguments.

Finally, a last plea from me to you: please don't take this formal stuff too seriously. While entertaining and fruitful, it is only one way to look at math. Save the thought and reconsider in a few years. (As an aside, I'm a logic and set theory fan myself.)

-
Don't worry, this is the reconsideration phase for me. – leolol Sep 2 '11 at 22:29
I do no understand how mathematicians believed formal proof systems could help establish a foundation. You can't prove something about X using X. X being the proof system. So the "foundation" can never be truly formal. Why did they wait for Godel to shatter their already seemingly shattered dreams. – leolol Sep 2 '11 at 22:35
@Yuval: I disagree on your claim that every day language can be translated to formal language; the main reason for the design of formal languages is precisely that everyday language is too ambiguous for situations when high precision is needed; formal languages (ideally) eliminate the ambiguity of everyday language. – gary Sep 3 '11 at 0:16
@gary: The working mathematician doesn't think of it this way (unless they're Harvey Friedman). I suggest you try to convert any non-trivial proof into formal language to see the difference. The "informal" proof is much more convincing than the formal one. The concept of proof as a formal object is as alien to math as denotational semantics are to computer science, or formal logic to philosophy, or semiotics to literature. It misses the point. – Yuval Filmus Sep 3 '11 at 10:28
@leolol: Until Gödel, perhaps there was the belief that a sufficiently clever formal system would be able to prove its own consistency. We must always remember that we have the benefit of hindsight. – Zhen Lin Sep 4 '11 at 13:36