# When proving statements on a logical system, do we use intuitive “meta” logic, or do we use the deduction rules from the system?

I'm new to the subject, but I'm currently reading into lecture notes about propositional- and predicate logic. I'm especially interested in the borderline between logic and language. Please correct, if some of the things I state here are wrong.

One can make statements about anything in the world being imaginable, and this statement (whatever a statement is in some language) can be true or false (or possible something in between). We have an intuitive understanding about the validity of some statements we can make in a language, provided other statements are already true.

All cats live on earth.
Simon is a cat.
THEREFOR Simon lives on earth.


I understand logical systems to formalize this process of determining the validity of a sentence (no matter wether it describes a cat or some manifold) - correct me, if I'm wrong here.

AFAIK, when "inventing" a logical system, we write down some definitions (how are certain objects called, for example logical symbols, predicates, or formulas, or what is their structure). This is fine for me, because definitions are just an agreement on how to call something. My brain is kind of powerful enough to live in a world where I call the objects I perceive the way I want to call them).

Next, I write down how true and false statements follow from previous sentences. My current understanding is as well that I have to assume these rules, they can't be deduced from any meta language or principle. One simply has to start somewhere. Is that right?

At this point, most lecture notes I encountered begin talking about things like soundness, completeness, or consistency, and the equivalence of the syntactic and the semantic truths. And they begin to draw conclusions about the logical system.

My question now is: For any statement of the logical system which isn't either a definition or one of the deduction rules of the logical system, do I only employ the deduction rules of the logical system to prove them - or do I have to use some kind of intuitive meta logic (the one I talked about in the beginning) to prove them?

• I comment because this user has very basic misconceptions about first-order logic, and refuses to even listen to expert logicians, hence it is necessary to inform other readers of this question (also about logic) about that. In particular, it is always the case that people who cannot correctly perform formal first-order reasoning cannot properly handle the distinction between the formal system and the meta-system, which is obviously closely related to the common confusions regarding the incompleteness theorems. So, no, you are wrong that it is not connected to your question. – user21820 Aug 22 '20 at 14:40
• As for whether I disagree with the answers, yes in fact the post here by the user with basic misconceptions about logic is simply wrong, but I can't be bothered to spend my time explaining why because every time I do so I get harassed and spammed. And I am not the only one; this has happened to many logicians on Math SE since many years ago and it's still the same today. The other answer is not wrong, but it also does not address your question. If you really want a proper answer to your question, let me know. – user21820 Aug 22 '20 at 14:43
• It's not connected in the sense that its content doesn't match, so it doesn't help getting an anwer to the question. It however can tell me something about the credibillity of the user. Can you write in an answer how exactly the distinction between system and metasystem is relevant for my particular question? Can you – Quantumwhisp Aug 22 '20 at 14:49
• Sure, I can. Give me a few minutes. – user21820 Aug 22 '20 at 14:51
• @user21820 This question, nor any of the answers concern any propositions concerning completeness or Goedel numbers. You have engaged in an ad hominem attack instead of addressing the question. No comment made in another place is an answer to this question. – Doug Spoonwood Aug 22 '20 at 16:05

I understand logical systems to formalize this process of determining the validity of a sentence (no matter wether it describes a cat or some manifold) - correct me, if I'm wrong here.

You are correct. In particular, a formal system just prescribes what sentences you can deduce. The system does not ascribe any meaning to the symbols or the sentences; it just tells you what you can deduce. If you want to ascribe any meaning to them, you of course cannot do so inside that system but have to do it outside it. In a Hilbert-style system, what sentences you can deduce are prescribed using the modus-ponens rule and the axioms. Other formal systems (such as Fitch-style systems) have different kinds of inference rules.

AFAIK, when "inventing" a logical system, we write down some definitions (how are certain objects called, for example logical symbols, predicates, or formulas, or what is their structure).

It depends on what exactly you mean by "logical system". If you mean "foundational system", then what matters is that proofs are computably verifiable. That is, every sentence that can be proven by the system has that provability witness by a (finite) string called a proof, and there is a single proof verifier program that given any input pair of strings $$(p,x)$$ will always halt and its output is "yes" iff $$p$$ is a valid proof over the system of sentence $$x$$. This is the most general notion of foundational system that can ever be used by humans (as far as we know).

Note that FOL theories with a computably decidable set of axioms and a suitable deductive system are all encompassed by the above notion, as are all other foundational systems that have been proposed in mathematical history, including non-classical theories and type theories.

If, however, you mean "abstract formal system" such as a general FOL theory (which perhaps may have an uncomputable or uncountable language or axioms), then you necessarily must work within a meta-system (which I shall call MS from now on), even if you do not do it formally. Note that MS is invariably itself a foundational system as per the above notion.

Next, I write down how true and false statements follow from previous sentences. My current understanding is as well that I have to assume these rules, they can't be deduced from any meta language or principle. One simply has to start somewhere. Is that right?

Yes, these are the inference rules I mentioned earlier. But it is not so accurate to say "how true and false statements follow from [...]". Remember, a formal system merely prescribes the syntactic rules, and there is no notion of "true" or "false". You can only assign that kind of semantic meaning from the outside, whether within MS or within natural language in the real world.

Also, yes, rules and axioms cannot be 'deduced' in any meaningful sense. If you think very carefully about it, you will see that there are fundamental concepts in logic that cannot be non-circularly defined or justified, as I sketch in this post.

For any statement of the logical system which isn't either a definition or one of the deduction rules of the logical system, do I only employ the deduction rules of the logical system to prove them - or do I have to use some kind of intuitive meta logic (the one I talked about in the beginning) to prove them?

This part doesn't really make sense. As per what I said above, given any computable formal system, whether a string $$x$$ is a theorem (i.e. proven sentence) over the system or not is definitively either true or false (whether or not we can figure out which it is), and this is simply whether or not there is a proof $$p$$ such that the proof verifier for that system outputs "yes" on the input $$(p,x)$$. It does not matter whether you can figure out whether such a $$p$$ exists, or whether you can figure this out but cannot find such a $$p$$, or how you manage to find $$p$$ (if you do). Even if you use incorrect reasoning and chance upon such a $$p$$, you can run the proof verifier and confirm that it is indeed a proof of $$x$$. The proof stands regardless of how you obtain it.

Nevertheless, maybe what you are asking is how we know that a formal system is meaningful. Well, you can either handwave and say that it seems good, or you can perhaps say something like "it proves theorems that seem true when interpreted in this particular way in the real world" so it is even empirically supported, as mentioned in the second part of this post about axiomatization of naturals.

Or, you can work within MS and prove that a formal system $$S$$ is sound, for some definition of "sound" that you define within MS. That is, if you and someone else agrees that your chosen MS is meaningful, then you can proceed to find a proof of some sentence over MS that $$S$$ is sound, where "sound" is some property that you can express within MS.

For example, you can prove (within MS) that FOL is sound, meaning that given any first-order structure $$M$$ and any set $$A$$ of sentences over $$M$$ that are true in $$M$$ (FOL structures, sentences and truth are all defined within MS as well), every sentence that can be proven from $$A$$ using a deductive system for FOL is also true in $$M$$.

For another example, you can define arithmetical soundness of a formal system $$S$$ as the property that there is a translation $$t$$ from arithmetical sentences (i.e. sentences in the language of PA) such that, for every arithmetical sentence $$Q$$, if $$S$$ proves $$t(Q)$$ then $$Q$$ is true in $$(\mathbb{N},0,1,+,·,<)$$ (of course this structure is also constructed within MS).

You might ask, how can we know that our chosen MS itself is meaningful? We cannot know non-circularly, as mentioned earlier. Nor can we talk about its soundness in absolute terms. But for any reasonable MS we have a translation of arithmetical sentences (because we want MS to be able to perform basic arithmetical reasoning), and so we can at least talk about whether MS is arithmetically inconsistent, namely whether it proves $$t(0=1)$$. That is a well-defined question, and we hope that MS does not do that! But as Godel-Rosser essentially showed, any such reasonable MS cannot even prove that it is arithmetically consistent, unless it is actually arithmetically inconsistent... (This is the incompleteness theorem.)

Lastly, I will note that most logic texts use a reasonably powerful MS such as ZFC or at least ZC. This is because they want to prove such things as the compactness theorem for FOL even for uncountable theories, and this needs a fair bit of set-theoretic assumptions. But if you only want to prove facts about countable theories you may be able to make do with a much weaker MS such as ACA (see this post).

• I guess the answer to my question then is that I have to use a MS (I called it "meta" logic") to prove statements like completeness or soundness of a formal system, and that I can't apply the deduction rules of the formal system to statements ON the formal system. I'm interested in why that is the case -and if the answer is "because then it would be circullary", why would that be bad? In a way the motivation for this question is that I'm looking for the most basic meta system possible. – Quantumwhisp Aug 23 '20 at 9:39
• @Quantumwhisp: Correct, simply because you always have to work within MS. If in that work you define and reason about some formal system S, you are following the deductive rules of MS, nothing else. It doesn't make sense to ask whether you can use something else, because you chose to work within MS. If you do not want to work within MS, you have to decide on something else. But if you are not confident in your ability to choose an MS that is meaningful, then just stick to what logicians use (namely ZFC) and simply take note of when you use certain powerful axioms of ZFC such as replacement. – user21820 Aug 23 '20 at 10:00
• If you just want to prove completeness and soundness of a reasonable deductive system for FOL (like all those currently in use), ACA is good enough, which is why I mentioned it right at the end, and gave some further details in the linked post. In some sense I would say that ACA is the bare minimum MS that is meaningful and able to prove basic facts about countable FOL theories. – user21820 Aug 23 '20 at 10:03
• I must emphasize that there is no circularity in using MS to reason about MS itself. There is only the impossibility of MS justifying itself as meaningful. For example, ACA (using a standard deductive system for FOL) can very well prove (after proving completeness of that deductive system for FOL) that if ACA itself is consistent then it has a model. What ACA cannot do is to prove that ACA itself is consistent (unless ACA is in fact inconsistent). – user21820 Aug 23 '20 at 10:11
• @user21820 In principle my question was answered. But "I must emphasize that there is no circularity in using MS to reason about MS itself" seems like a contradiction again. If an MS is a foundational system, I would need another MS' to reason about MS. – Quantumwhisp Aug 24 '20 at 6:04

You could think of logic, e.g., first order/Predicate logic, as a game that you play to produce new propositions. Like any game, you need to start somewhere; you need starting pieces and basic rules, so to speak. In the case of Predicate, the starting pieces are the propositions, constructed from constants, variables, quantifiers, predicates, and logical operators. The “rules of play” are then the rules of inference/deduction. They aren’t god-given or self-evident, i.e., aren’t canonical; people choose what rules to play with based on their goals and beliefs (cf. natural deduction vs sequent calculus vs Hilbert system). As an example, some people allow Predicate to have the Law of the Excluded Middle, while many others refuse it. In a system of the former type there will be propositions that follow non-constructively from the axioms, while in the latter there might not (because, for instance, an argument for Q of the form $$(P \vee \neg P) \Rightarrow Q,\, \therefore Q$$ might not exhaust all cases on $$P$$).

So, in short, like playing a game, you must use the established rules of inference, on whatever kinds of propositions are allowed, to produce new propositions that the system (Predicate, e.g.) accepts/acknowledges. In fact, there are many gamifications of logic that make what I said about quite literal, one of which is here.

Edit(To better address the question of whether one must only use the axioms when producing theorems): You could "break the rules", so to speak, and use a non-axiomatic/theorem statement to "prove" things, but you can't be guaranteed that it is a valid rule of inference unless you accept it as one or later deduce it from the axioms. This lead to, for example, the adoption of the Axiom of Choice into the ZF system of set theory (creating ZFC) because many "proofs" involved choice functions whose existence couldn't be guaranteed.

• That means for example that if my logical system doesn't allow for the law of the excluded middle, then I can't make use of this law, when I for example want to prove the consistancy of the logical system itself. Is that right? – Quantumwhisp Aug 22 '20 at 14:47
• As a note, you could use it to prove things, but you couldn't be guaranteed that it is a valid rule of inference unless you accept it as one or deduce it from the axioms. This lead to, for example, adopting the Axiom of Choice into the ZF system of set theory (creating ZFC) because many "proofs" involved choice functions whose existence couldn't be guaranteed; see here, for example. – SBRJCT Aug 22 '20 at 15:44
• As for using it, in your example, to prove statements about the system itself, I believe you'd essentially be considering it as an axiom in a larger system so that it is actually acting as valid rule of inference. This is way out of my wheelhouse, but I know, for example, that while ZFC can't prove its own consistency, by adding another axiom (there is an inaccessible ordinal), you can prove the consistency of ZFC. But again, it involved adding an axiom. – SBRJCT Aug 22 '20 at 16:05