4
$\begingroup$

I don't really know much about formal logic. But there is a kind-of-philosophical question that has always been bothering me. It seems to me that, in the context of mathematical logic, we are permitted to use mathematics and "common" logic to reason about logical systems we study. I want to know if my understanding is correct. More precisely, I want to know the answers to the following (very vague) questions.

Consider a statement A about a deduction system $\mathcal{D}$. For instance, A is the statement that a certain formula is formally provable from $\mathcal{D}$.

(1) Is it true that this statement A and a proof of it are on the meta-mathematical level?

(2) What are the rules that we are permitted to use to prove statement A? I will illustrate this by an example: in proving Goedel's Completeness Theorem, mathematical induction (a mathematical construct, supposedly having some mathematical content, at least meta-mathematically) and proof-by-contradiction (a logical construct) are apparently being used. Base upon this example, let me rephrase question (2) in the following smaller parts:

(2.a) Is there an agreement among practitioners of mathematical logic on the kinds of ordinary mathematics that are allowed?

(2.b) Consider a certain piece of mathematics, denoted by $\mathcal{M}$, together with the collection $\mathfrak{F}(\mathcal{M})$ of formalizations\axiomatizations of $\mathcal{M}$. Is it a sensible question to ask about the dependencies of the deduction system $\mathcal{D}$ upon each $\mathcal{F}\in\mathfrak{F}(\mathcal{M})$ based on the results about $\mathcal{D}$ that are deducible from $\mathcal{M}$? Here, the word "deducible" should be taken to mean "meta-mathematically deducible" if the answer to (1) is yes. More specifically, can we make sense of the following diagram or perhaps the reversed arrow?

$\{\text{dependencies of }\mathcal{D}\text{ on }\mathcal{F}\in\mathfrak{F}(\mathcal{M})\}\longrightarrow\{\text{results }A\text{ about }\mathcal{D}\text{ deducible from }\mathcal{M}\}$.

If we can, what kind of structures do these things have? This is the place in my question where I think category theory or homotopy theory might be relevant.

(2.c) As for the logical constructs, it seems we are allowed to use usual, everyday logic. But if we were to prove something about a formal logical system that is somewhat intuitionistic where proof-by-contradiction is not formally available, it would lead to a philosophical problem of using a meta-mathematical reasoning framework (everyday human logic, so to speak) where proof-by-contradiction is allowed to deduce results about a formal system where proof-by-contradiction is not allowed.

I would really appreciate it if you could also give me some references.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ Does this answer to a similar question help? (You might just read the last sentence first.) $\endgroup$
    – Andrej Bauer
    Commented Nov 11, 2020 at 19:40
  • $\begingroup$ It helps. I understand the inevitability of leaving philosophical questions to philosophers and the methodology of thinking about and doing research in mathematical logic as one would in any mathematical discipline (cue: "mathematical" is the adjective in front of "logic") using human logic and ordinary mathematics. $\endgroup$
    – Wei
    Commented Nov 11, 2020 at 21:56
  • 1
    $\begingroup$ One point there is, why do you expect logicians to have different standard for doing mathematics than all the other mathematicians? Do you think it's somehow their task to "build a foundation"? I think that's a very misguided task. $\endgroup$
    – Andrej Bauer
    Commented Nov 11, 2020 at 23:09
  • $\begingroup$ That's a good point! I did have the impression that one of logicians' job was to create a formal foundation from scratch but soon realized the difficulty of not using mathematics and then the ambiguity of logical operations permitted to use. Now I understand, or at least, I can agree with your stand on this issue. $\endgroup$
    – Wei
    Commented Nov 12, 2020 at 4:55
  • $\begingroup$ You may be interested to read about reverse mathematics. All known theorems about logic that have practical implications (e.g. Godel's semantic completeness theorem and syntactic incompleteness theorems) can be proven in ACA0, which is conservative over PA. This at least makes these theorems very convincing and not open to doubt. It also turns out that all practical applications of real analysis can be derived from theorems of ACA0, though it's not relevant to your question. $\endgroup$
    – user21820
    Commented Aug 2, 2021 at 18:24

1 Answer 1

Reset to default
2
$\begingroup$

So in a usual mathematical proof you choose some system if axioms from which you prove it. For instance, there are claims about the natural numbers you can prove in ZFC but not from the axioms of Peano Arithmetic.

Exactly the same thing is true when you prove things about a formal system (eg proof system or logic). There aren't abstract proofs just floating out there in no system at all you always have to specify the meta-system in which you are proving your results in (at a formal level when you prove things about proofs you are usually treating the proof relation just as a particular sort of relation on integers which are regarded as coding sentences or sequences of sentences) and depending on which system you use at the meta-level you may be able to prove different things. So strictly speaking results should always be of the form ZFC (or PA or ...) proves such and such about logic/proof system blah. But that's frequently omitted when it won't cause a confusion.

As for your later questions about proving things about intuitionistic logic classically that really depends on your motivations for caring about intuitionistic logic. A philosopher who is using intuitionistic logic because they think classical logic is suspect and inferences in it not truth preserving would, of course, only trust results about intuitionism proved intuitionisticly (very few people seem to really take that position even in philosophy). OTOH if your interest is in the practical use of intuitionistic logic in certain CS applications you'll be happy with proofs about it in ZFC.

Does that kinda answer your question?

Improve this answer
$\endgroup$
4
  • $\begingroup$ Thanks! It makes sense to explicitly specify the ambient assumptions (e.g. ZFC, etc.) under which we prove things about a formal system. You said that "if your interest is in the practical use of intuitionistic logic in certain CS applications you'll be happy with proofs about it in ZFC." Could you enlighten why this is the case? $\endgroup$
    – Wei
    Commented Jan 20, 2021 at 7:22
  • $\begingroup$ Because if you are interested in the applications I'm presuming what you care about is being convinced that it actually works and ZFC appears not to prove false claims about the integers. So if you provide in ZFC that you can decide a question of intuitionistic entailment about such and such length inputs in in k^2 steps you really will be able to. $\endgroup$
    – Peter Gerdes
    Commented Jun 1, 2021 at 19:09
  • $\begingroup$ I realized I could have given a better answer. Suppose that you prove some result about an intuitionistic system I in ZFC, e.g.,the double negation of anything provable in classical logic is provable in I. If you later find a finite instance where that claim actually fails you can turn it into a proof of contradiction in ZFC itself (ok, if it's not a pure existential statement you'd show that ZFC has no standard model but still an earthshattering mathematical result) $\endgroup$
    – Peter Gerdes
    Commented Aug 11, 2022 at 13:11
  • $\begingroup$ Also, I should add, that all the big sets and cardinal stuff doesn't really come into play. Since you are interested in results (codeable as) statements about the natural numbers ZFC is just a conveinient way to state a theory that extends PA with some strong (regular) induction...indeed you can probably find a reference somewhere where someone has shown that ZFC is conservative over so and so's arithmetic $\endgroup$
    – Peter Gerdes
    Commented Aug 11, 2022 at 13:14

You must log in to answer this question.

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