0

I would like to know: How to find out in what particular formal system I am working (what axioms, rules of inference and formal language am I assuming) when they don't specify me in a school? For example, in what particular formal system in mathematics are located the following statements?:

1) 4+5=9

2) 2x-1=7

TKN
  • 757
  • 3
    It almost never matters, even in professional mathematics. When it does matter, the practitioners are very much aware of the way that it matters. – Ian Aug 26 '19 at 12:05
  • Why would you be using a formal system at all, unless you were taking a course on formal systems and logic? Most subjects in mathematics do not require the use of formal systems. Good thing, seeing as formal systems were only invented quite recently. – bof Aug 26 '19 at 14:57
  • Isn't it necessary to know in which particular formal system I'm working to be able to prove anything? – TKN Aug 26 '19 at 16:24
  • Surprisingly, no. This is partly because most proofs aren't actually "formal" in the sense of formal systems in the first place. Most proofs are humans talking to humans, giving a rather detailed sketch of how you might construct a formal proof, once you had already bootstrapped our colloquial discourse about things like "sets that aren't stupidly huge" into your formal system of choice. Proofs that explicitly care about the underlying formal system rarely arise outside of logic. – Ian Aug 27 '19 at 01:41
  • (That said, independence results, like showing that ZFC is independent of the continuum hypothesis, do ripple out into "general mathematics". For example there are a variety of slightly esoteric results in analysis which require CH or its negation.) – Ian Aug 27 '19 at 01:46
  • Do I understand it right, that the usual reason for not using formal proofs in mathematics is that it would be too lengthy for people to create such a proofs? Or the reason is that in the math not everything is possible to prove by a formal proof? – TKN Aug 27 '19 at 08:30
  • 1
    Mostly the former, though Godel's incompleteness theorems mean that there is a little bit of the latter too. Related to the former is the fact that a formal system typically carries with it a bunch of baggage about "arbitrary decisions", which don't really mean anything. This generates a vast sea of valid-but-meaningless theorems that the formal system can't really distinguish from "mathematical" theorems. – Ian Aug 27 '19 at 10:16
  • 1
    Could you please give me some example of such "arbitrary decisions" and "valid-but-meaningless theorems" that we would not use in informal proof? For example some link where the informal proof is compared with the same proof which is formal, to have an idea what you are specifically talking about? – TKN Aug 27 '19 at 10:36
  • In ZFC for example you answer the question of whether $A \in B$ for literally every pair of sets $A,B$, even when these sets are really encodings for objects that don't actually behave very much like sets, e.g. real numbers. – Ian Aug 27 '19 at 10:48

0 Answers0