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

Question

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?

Answer 1

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.

Answer 2

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).