1
$\begingroup$

There are various reasons why one would want to reject the law of the excluded middle when doing "normal" mathematics, which I won't get to here, but accepting those, does the same reasoning hold when thinking about metamathematics? Of course, there are many different "levels" of intuitionism and constructivism, but it seems strange to me that a constructionist would rely on results like the Löwenheim–Skolem theorem, when it uses LEM at the metamathematical level. Isn't assuming LEM, even if at a metamathematical level, begging the question for an intuitionist? Are there philosophical reasons to believe that it may be more or less acceptable to use LEM at the metamathematical level from a constructive standpoint?

Furthermore, is there a computational interpretation of metamathematics in general? Its just a hunch, but it seems to me like metamathematics, and using LEM at the metamathematical level might be related to oracles in some way, but I have no sources for this.

$\endgroup$
8
  • 1
    $\begingroup$ Do you have any sources for this? Or examples of claimed intuitionistic proofs where LEM in meta-mathematics is used? Otherwise I would just say No, LEM is not supposed to be used in Intuitionistic mathematics, not even on meta level. And the Löwenheim-Skolem theorem is very unconstructive in its normal form. $\endgroup$
    – Ove Ahlman
    Feb 15, 2016 at 14:37
  • $\begingroup$ Robert Harper uses it here as an analogy to Church's law being provably false within ETT, but true metamathematically. However, he seems to be accepting of the implications of the Löwenheim–Skolem theorem nevertheless (namely, Skolem's paradox), which prompted the question. Whereas others seem to reject the validity of the paradox entirely. My question is, what philosophical differences lead to these separate conclusions on the use of LEM? $\endgroup$
    – Nathan BeDell
    Feb 15, 2016 at 15:23
  • $\begingroup$ For some metamathematical results proved in a constructive way, you can see Anne Troelstra & Dirk van Dalen, Constructivism in mathematics: An Introduction (1988). $\endgroup$
    – Mauro ALLEGRANZA
    Feb 15, 2016 at 20:18
  • $\begingroup$ I would say there is no point rejecting the law of excluded middle because they would need to present a situation or something where something is what it is AND at the sametime is what it isn't, and show that is neither too. This in on itself is insane. $\endgroup$
    – Zelos Malum
    Mar 8, 2016 at 15:07
  • 1
    $\begingroup$ If a theorem derives a contradiction in intuitionistic logic, it is false, by definition. Intuitionistic logic takes the law of non-contradiction as an axiom, but not the law of the excluded middle. They are not equivalent in the intuitionistic context because double negation elimination is not an axiom. $\endgroup$
    – Nathan BeDell
    Mar 8, 2016 at 16:41

2 Answers 2

Reset to default
1
$\begingroup$

This is more a philosophical question than a mathematical one. If you think that even logic (reasoning about formal systems) is just a symbol game that is played with the inference rules of the meta-system, then the question is meaningless as we simply play and never question the rules.

However, if you believe that PA is either consistent (there is no sentence over PA that it both proves and disproves) or inconsistent (there is some sentence over PA that it both proves and disproves), in the sense that one of the two possibilities actually is a fact in the real world, then you essentially have accepted LEM for a $Σ_1$-sentence about the real world (suitably understood). This is equivalent to accepting that an given program on an input either halts or does not halt. Once you do this the next natural step is to ask about the halting behaviour of programs that have access to the halting oracle. Each step of their execution is well-defined, since it is either computable or it requires asking the halting oracle one question, which we have already agreed has a well-defined answer. And so naturally you get the next Turing jump. And you can continue this reasoning for finitely many jumps. In this sense it seems that the meta-system you would have to accept is not only classical but has the same strength as ACA. (See this post for a more detailed analysis.)

Indeed, intuitionistic logic corresponds directly to programs via the BHK interpretation, and every invocation of LEM corresponds to an oracle query in the program. A proof can also be understood via game semantics where "$\forall$" gets the Refuter's move while "$\exists$" gives the Prover's move, and LEM asks the Refuter to choose between two cases. The distinction between "$\forall$" and LEM is that for the quantifier the Refuter must give evidence that the object he provides is of the claimed type, and the Prover can make use of this evidence in her game play, whereas for LEM the Refuter does not have to give any evidence whatsoever of the choice. Notice that "$A \to B$" can only be used in implication elimination when you have also deduced "$A$", which means you have evidence for "$A$" that can be fed to the program that witnesses "$A \to B$". Likewise for universal quantifier elimination. Not so for LEM, which means that a proof that uses LEM corresponds to a program execution that will get stuck at the invocations of LEM until someone feeds it the evidence needed (for one of the cases) to continue along.

$\endgroup$
1
$\begingroup$

There is a metamathematical/philosophical use of the law of excluded middle in authors like Errett Bishop that has been spotted by Sam Sanders. Namely, such authors believe that mathematics is either classical (using LEM) or constructive (eschewing LEM). No middle ground! That's a metamathematical reliance on the excluded third.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .