How can a formalist understand a metalogical proof such as the completeness theorem? These proofs exist exclusively outside of a logical system where the "rules of the game" are undefined. These sorts of metalogical theorems attest to the validity of the logic a formalist must hold dear, thus it seems problematic they are unjustifiable within this perspective.
$\begingroup$
$\endgroup$
2
asked Feb 12, 2019 at 0:04
-
$\begingroup$ This may be a question more suitable for philosophy.stackexchange.com. $\endgroup$– Thomas DavisFeb 12, 2019 at 0:12
-
4$\begingroup$ The short answer is "formalize the metatheory" $\endgroup$– Carl MummertFeb 12, 2019 at 0:45
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
7
Method A. By making the metatheory explicit. The completeness theorem is provable in ZFC, so if $\Phi$ is a statement of the completeness theorem in the language of ZFC then a formalist/finitist still recognizes the formal derivation that shows $\text{ZFC} \vdash \Phi$.
This method may not be very satisfying, because it doesn't help a finitist prove anything else. The next method does that.
Method B. Through conservation results. There is a system $\text{PRA}$ of arithmetic that is usually identified with finitistic reasoning. There is also a subsystem $\text{WKL}_0$ of second-order arithmetic with the following properties:
$\text{WKL}_0$ proves the completeness theorem for countable, syntactically consistent first-order theories (every countable first-order syntactically consistent theory has a model).
There is a finitistic proof that any $\Pi^0_2$ sentence of arithmetic that is provable in $\text{WKL}_0$ is provable in the finitistic system $\text{PRA}$. This kind of metatheorem is known as a `conservation result'.
So a formalist can work in $\text{WKL}_0$, and use the completeness theorem for countable theories, while knowing all the while that any $\Pi^0_2$ sentence that she proves is already finitistically provable. Because statements viewed as meaningful in finitism are going to be at worst $\Pi^0_2$, this means that any meaningful statement she proves from $\text{WKL}_0$ can be proved finitistically, and hence can be "accepted".
This method is sometimes known as 'reductionism'. The idea is that someone can use an "ideal" theory (e.g. $\text{WKL}_0$) to prove a wide variety of statements, knowing that some subclass of these statements (e.g. the $\Pi^0_2$ ones) that are proved in this way are already provable in a weaker "concrete" system that the person prefers.
answered Feb 12, 2019 at 0:19
-
1$\begingroup$ I'm not sure I see how this helps a finitist be comfortable with the completeness theorem. Is the idea that they could do a rudimentary model theoretic proof of consistency in WKL$_0$ and be content that it means there is a 'legit' PRA consistency proof out there? $\endgroup$ Feb 12, 2019 at 0:32
-
1$\begingroup$ It means that they can prove whatever they want in WKLo, and even use the completeness theorem (which is provable in WKLo anyway), and know that even though they are using axioms that are not finitisitic, any "meaningful" (i.e. $\Pi^0_2$) sentence that they happen to prove also has a finitistic proof (which can be mechanically extracted from the proof in WKLo). So they can be comfortable that, as long as they stick to WKLo, they don't have to worry about the completeness theorem proving any meaningful statements that they think are false. $\endgroup$ Feb 12, 2019 at 0:35
-
1$\begingroup$ So, I guess it's right that, if I can prove in WKLo that a given theory is semantically consistent, then I can prove in WKLo that the theory is syntactically consistent, and that latter syntactic claim is $\Pi^0_2$, so that means there is a finitistic proof that the theory is consistent. (Of course, WKLo doesn't prove too many theories are semantically or syntactically consistent). But the completeness theorem is usually read in the other direction - syntactic implies semantic consistency - and that direction is only useful for a finitist if it implies other, more meaningful statements. $\endgroup$ Feb 12, 2019 at 0:39
-
1$\begingroup$ Got it (and already +1'd before commenting). Yes, I guess that 's the soundness direction. (I also liked the analogy in the comment you deleted, that e.g. a person who doesn't believe in AC can and should use it freely in their attempts to prove the Riemann hypothesis.) $\endgroup$ Feb 12, 2019 at 1:13
-
1$\begingroup$ Also, out of curiosity, why is $\Pi_2$ considered the boundary for finitism? I would have thought $\Pi_1$. $\endgroup$ Feb 12, 2019 at 1:50