In logic there are no morals. Everyone is at liberty to build his own logic, i.e. his own language, as he wishes. All that is required of him is that, if he wishes to discuss it, he must state his methods clearly, and give syntactical rules instead of philosophical arguments.
- Carnap, The Logical Syntax of Logic [3]

How do you build a logic?

The main references of this book are Carnap’s The Logical Syntax of Language. [3] and Harrison’s Handbook of Practical Logic and Automated Reasoning [2].

What does it mean to “build a logic”?

It may seem strange to say that we can “build a logic”. What does that even mean? Different people will have different conceptions of logic. Some will think of it as a sort of trascendental concept that governs existence and reality; others see of it as the underlying rules that capture rational human thought; and yet others see of logic as a foundation which we build mathematics.

These are all valid ways to think about logic, but I want to hone in and talk on a specific tradition of logic: formal symbolic logic. When I say “logic”, what I really mean is a special kind of constructed language (a conlang, if you will). The point of this language is to talk precisely and unambiguously about some area of study, be it reality, rational human thought or mathematics.

To give a sense of the clarity gained from using a specialised language, consider the sentence “Everyone loves someone.” You can interpret this sentence in two ways:

1. For everyone, there is someone that they like.
2. There is a single someone which everyone loves. [Add image of the two cases, ensure you label who trixy is]

There ambiguity revolves around how ”everyone” interacts with the word “someone”. However, if you are privy with predicate logic, you can write both interpretations unambiguously:

1. $\forall x. \exists y. \text{Loves}(x,y)$
2. $\exists y. \forall x. \text{Loves}(x,y)$

These sentences in a symbolic language is sometimes called “formulae” (sing. ”formula”) and I will be calling sentence in symbolic language as “formulae”. Don’t worry if you don‘t understand what those formulae mean. The point of this example is to show that a symbolic language can be used clarify sentences in natural language.

So now two motivating question arise:

1. How might one create a symbolic language?
2. How do we make this symbolic language mean what we care about?

Derivation

If all this symbolic language did was clarify and mean things, it would be pretty limited language. Statements about the reality, rational human thoughts or mathematical theorem don’t just sit in isolation, but rather they often imply or infer each other.

An (deductive) inference is a process* which starts from some sentences (which we call “premises”) and allows you to take for granted a sentence (which we call the “conclusion”).

Consider the following argument: 1. Trixy is a bird. 2. If Trixy is a bird, then it can fly. C. Trixy can fly. Here we can take sentence (C) for granted if we are given sentences (1) and (2). Furthermore, we can chain these inference together and treat “Trixy can fly” as a premise in another argument. A chain of inferences rules is often called a “proof” or a “derivation”.

An important note is that meaning of the sentences doesn’t matter for a (deductive) inference — what really matters is the grammar of sentences and the form of the argument.
Consider the same argument but with nonsense words: 1’. Glarj is a nork. 2’. If Glarj is a nork, then it can gruw. C’. Glarj can gruw. It is intuitive (at least to me) that (C’) can be taken for granted given (1’) and (2’).

Here our symbolic language would shine again, because we can make exact what are the rules of inferences. A common notation is to use an inference line: [Where does this originate from?] \(\dfrac{\text{P 1} \qquad \text{P 2} \quad \cdots \quad \text{P n}}{\text{Conclusion}}\) So our modus ponens example can be written as: \(\dfrac{A \to B\qquad A}{B}\)Here $A$ and $B$ are metavariables, which are meant to stand in for any formula in our symbolic language.

Here we have more motivating questions:

1. How do we declare rules of inference in our symbolic language?

Some caveats

Some books may introduce inference as “guaranteeing the truth of a conclusion given the truth of the premises”. This is called validity —the idea that the conclusion cannot be false given that the premises are true.

However, I have been really careful not to say the word “truth” or “validity” when talking about derivations and instead have been using words like “given” or “taken for granted”.

In symbolic logic, a formula being true and a formula having a derivation are two very distinct ideas.

The interaction between truth and derivation is explored with Soundness and Completeness. Soundness means that if you get a derivation of a formula, then you can be sure that the formula is true, i.e. the rules of inference are valid. Completeness means that if a formula is true then it has a derivation, i.e. everything that can be shown true has a proof.

A question then arises:

1. Given some inference rules, how does a derivation of a formula interact with the truth of the formula?

Outline

This series is loosely divided into the following sections:

1. Building Words
2. Building Sentences
3. Building Meaning
4. Building Derivations
5. Digression: Meta-Building
6. Soundness and Completeness
7. Computability and Decideability
8. Doubting the Assumption

Footnotes

*I chose the term “process” as a compromise between being easy for laypeople to understand and not being circular. I do not want to say, for example, “an inference is where you obtain the conclusion from the premise”. Alternative words would be ”a function”, “a map”, ”a (syntactic) transformation”, “an argument form”. Each may make more sense to you if you have a linguistic, mathematics, computer science or philosophy background.