8
$\begingroup$

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.

  • 0
    I think this is the goal of metatheory.2011-09-02
  • 0
    @gary - using metatheory brings up the same question again. Can I trust the metatheory? is it consistent? and so on2011-09-04
  • 0
    @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.2011-09-04
  • 0
    @leolol: yes; it is the same as the issue of infinite regress, and I don't see how it can be avoided.2011-09-11

1 Answers 1