Creating Logic, Part 3 – Another Look at Logic Reading Notes

Creating Logic, Part 3 – Another Look at Logic Reading Notes

Logic is the study of the way humans think and argue, and in particular, it deals with the basic concepts of propositions and reasoning.

The basic concepts of logic include propositions, propositional logic, and the symbolic system of logic. A proposition is a statement that is determined to be true or false. Propositional logic is the field of logic that deals with propositions and uses logical operators to represent logical relations. The symbol system of logic is a system that defines symbols to express logical operations, and in propositional logic, logical operators such as “negation,” “logical conjunction,” and “logical disjunction” are used.

In addition to propositional logic, there are other fields of logic such as first-order predicate logic and higher-order logic. First-order predicate logic is a type of propositional logic that can express more complex logical relations by introducing predicates and variables. Higher-order logic deals with logic involving mathematical concepts such as sets and functions.

Logic also includes the study of methods for determining the truth or falsehood of propositions and for making correct inferences. For example, there are methods of determining the truth or falsity of propositions, such as truth tables and proofs. The truth table is a method of determining the truth of a proposition by testing all possible combinations of truth and falsehood for the proposition. Proof is the logical procedure for showing that a proposition is true, using axioms and rules of inference to derive the truth of the proposition.

Logic is also closely related to philosophy, mathematics, and artificial intelligence. In philosophy, the concepts of logic are used to make logical arguments, and in mathematics, logic is used to construct the basic system for deriving mathematical propositions. In artificial intelligence, it is the basis for reasoning and knowledge information processing techniques.

Mathematical theories on which logic is based include set theory, as described in “Overview of Set Theory and Reference Books,” algebra, as described in “Structures, Algorithms, and Functions,” and formal linguistics and semantics, as described in “Formal Languages and Mathematical Logic,” which can be found at See also.

we present reading notes from “Making Logic,” a well-known textbook on mathematical logic.

Following the previous Part 2, Expanding Logic, I will now discuss the reading notes in Part 3, Another Look at Logic.

Part III: Seeing Logic Through Another Set of Eyes

Chapter 9: Mastering the Natural Deduction Method
9.1 Creating the Natural Deduction Method

9.1.1 From evaluation to construction
Introduction
The argument “P → Q, Q → R, therefore (R → S) → (P → S)” is correct.
We can use tableaux to prove this.
Tabloid and truth table techniques are
For a given argument
In the “evaluation procedure” to judge whether a given argument is valid or not
So, is it possible to get (R→S)→(P→S) from P→Q and Q→R?
Drawing conclusions from premises step by step
In this chapter, we will create a procedure for actually drawing conclusions from given premises
Formulated by Gerhart Gentzen and organized for ease of use by Frederic B Fitch
Procedure
(1) Let P → Q (assumption)
(2) Let Q → R (assumption)
(3) Now, suppose that R → S (assumption)
(4) Further, suppose that P is P (assumption)
(5) By (4) and (1), it is Q.
(6) By (2) and (5), it is R.
(7) By (3) and (6), it is S.
(8) Therefore, since S can be derived under the assumption of P in (4), P → S
(9) Therefore, P → S can be derived under the assumption R → S in (3), so (R → S) → (P → S).
(10) From the above, we can derive (R→S)→(P→S) based on the assumption that P→Q and Q→R.
Let’s reflect on the procedure of deduction
(5) to derive Q from (4) and (1)
Q comes out logically from P and P → Q
P → Q, Q → R ⊨ (R → S) → (P → S), a fact on the same level as the fact that
The procedure of deduction is
The procedure of deduction is to bridge the gap between equations whose logical consequence is not immediately obvious with a simpler and more obvious logical consequence.
Conditions that the deductive procedure must satisfy
(a) The validity of the procedure must be obvious enough to be seen.
(b) A clear distinction must be made between permissible and impermissible transitions.
(c) The repertoire of permissible transitions is as small as possible.
In making deductions, the deductionist is making more assumptions.
(3) and (4)
Assumptions added by the deductioner must be cancelled somewhere before the deduction is completed.
(8) and (9)
9.1.2 First step toward formalization
Properly define the deduction rules and formalize the entire deduction to create a natural deduction.
Derived lines and premise bars
When making a deduction, you should
We need to write in a way that clearly shows which assumptions each expression is based on.
One way of writing
(1) P→Q (assumption) (2) Q→R (assumption) (3) R→S (assumption) (1),(2) (4) P (assumption) (1),(2),(3) (5) From Q (4) and (1) (1),(2),(3),(4) (6) From R (2) and (5) (1),(2),(3),(4) (7) From S (3) and (6) (1),( (8) P→S (1),(2),(3),(3) from (4) and (7) (9) (R→S)→(P→S) (1),(2) from (3) and (8)
Graphical representation of the above
The vertical line is called the derivation line.
Transformation of the expression made by the derivation line
Derivation under the assumption of (1) and (2)
Derivation assuming (1),(2),(3)
Derivation assuming (1),(“),(3),(4)
A new assumption is made for each derivation.
The second line from the left that leads from R→S to P→S
The rightmost derivation from P to S
The assumptions made in the leftmost derivation are also valid for the rightmost derivation.
Modification of display method
Dependencies of the derivation and assumptions that are alive in the derivation
Definition
A derivation D depends on another derivation D’.
⇔
A horizontal line going left from the derivation of D intersects the derivation of D’.
Example
D1 is dependent on D2 and D3, and D2 is dependent on D3
From the point of view of D3
D2 and D1 are “sub derivation
D2 is the “first order sub derivation
D1 is the second-order subderivation
Definition
A living assumption in derivation D is one of the following
(1) An assumption that is placed on the entire bank of D.
(2) An assumption that is written on top of the assumption bars of any derivation on which D depends.
9.1.3 Formulate a deduction rule
State the rules to be followed for deduction.
These rules in natural deduction
Premiss rule (Prem)
(1) When you start a deduction, you can write a line of deduction and write any number of logical expressions on the premise bar.
(2) When you start a new derivation in the middle of a deduction, you may write a derivation line and write only one logical expression on the premise bar.
Repetition Rule and Resurrection Rule
Rule of repetition (Rep)
In a derivation, you may write a formula on the premise bar of the derivation repeatedly.
Rule of reiteration (Reit)
In derivation D, you are free to use the assumptions on which the derivation depends (assumptions that are still alive in D).
You may bring in any equation on the derivation line to the left of D and use it in D.
Anywhere in derivation D, you may write any logical formula that already occurs in the derivation on which D depends.
If you apply the resurrection rule incorrectly, you will get into trouble.
Example
The part that derives P from Q does not depend on the derivation that derives P from P, so
You can’t resurrect P coming from there
9.1.4 →introduction rules and →elimination rules
→ removal rule (→elimination : → elim)
Example
Line 6 comes out of lines 4 and 5
Line 8 comes out of lines 6 and 7
Line 10 appears from lines 8 and 9
Which of the three “? What rules should we use to write what is done in the three “?
→ elimination rule (→ elim)
If A→B and A appear in the same derivation, you can add B to the derivation.
→Introduction rule (→ introduction : → intro)
What about the part “? What about the part “?
If we assume P, we get S, so we can say P → S without assuming P.
→Introduction rule (→intro)
If a derivation D contains as part of it a derivation from premise A to B (a first-order subderivation of D), then
A → B may be added as the next term in the derivation
B is derived under the assumption that A, but
A→B is derived without the assumption of A
If B can be derived by assuming A, then we can cancel assumption A and derive A→B
Eventually
9.1.5 Deduction Strategy
Tableau is a mechanical method that produces results whenever you apply the rules.
It can be done completely mechanically if you are willing to let the tableau get bigger
Natural deduction is like saying, “Derive … from … The starting point and the end point are specified, and you have to connect between them.
Which rules should be applied to which equations in what order?
What kind of new process should be created?
If you make the wrong choice, you will not be able to reach the desired equation.
It is possible to make the structure of deduction by natural deduction quite close to “how anyone can do it”.
Example
“Derive Q → (P → R) from P → (Q → R).”
Strategy: Build the deductive framework first.
A1,… If you want to deduce B from A1,…,An, you must first build a deduction framework for A1,…,An. An vertically on the premise bar, and write B at the bottom of the derivation line.
Strategy: How to get to →?
If you want to reach A→B, you can use A as a premise, construct a derivation with B at the bottom, and then try to get A→B by →intro.
1
2
Strategy: Resurrection is always OK
If you want to arrive at a formula, try another strategy, and then revive the formula you think will help.
Strategy: Removal is always OK
Whenever you can use the elimination rule, use it anyway.
9.1.6 Deduction, Theorems, and Proofs
Definition
(1) Derivation of B from A1,… (1) If there is a derivation of B from A1,…,An that does not depend on any other derivation
Let it be a derivation of B from A1,… When there is a derivation of B from A1,…,An and it does not depend on any other derivation, it is called deduction of B from A1,…,An ). ,An ).
(2) As in Exercise 64, there is a deduction without a premise bar in the leftmost derivation line.
This shows that P→(Q→P) could be deduced without any assumptions.
An expression with such a deduction without any assumptions is called a theorem, and its deduction is called a proof.
Proof: a sequence of logical formulas arranged according to some rule (i.e., inference rule)
Theorem: The last logical formula in the sequence.
On the other hand, there is a “metatheorem”.
A statement in meta-language Japanese of a certain fact that is actually true about a collection of logical formulas, the relationship between logical formulas, etc.
A proof is a statement of the correctness of the fact using the Japanese language and some auxiliary symbols (such as ⇔, ⊨⫤, etc.). Translated with www.DeepL.com/Translator (free version)

9.2 Inference Rules for Other Bindings

9.2.1 Introduction and Removal of Λ
Removal rule for Λ (Λ elim)
If AΛB appears as an item of a derivation, then both A and B can be added as items of the same derivation.
Rule for introducing Λ (Λ intro)
If both A and B appear as items of the same derivation, then AΛB may be added as an item of the derivation.
Strategy: How to get to Λ
If you want to get to AΛB, try to get A and B separately, and then use Λintro.
Is it possible to deduce with just the strategy?
Deduction from (P→Q)Λ(R→S) to (PΛR)→(QΛS)
(1) First, create a framework for deduction.
(2) To aim for →.
(PΛR)→(QΛS), we assume PΛR and derive QΛS
(3) To aim at Λ
To derive QΛS, we can derive Q and S respectively
(4) Resurrection is always OK
We can lead either Q or S.
But we need to use “Resurrection is always OK” to get the materials to derive them.
However, only one of (P→Q)Λ(R→S) can be resurrected.
Resurrect it.
(5) Removal can be done at any time
Remove Λ, also remove Λ from PΛR
(6) Once again, removal is OK even with iron
Remove → from P → Q and R → S
You have to use your head a little.
Derive P→(Q→R) from (PΛQ)→R.
Create a deductive framework, to get to →.
Use (PΛQ)→R to get R. Then if PΛQ comes out, →elim to get R
The problem is how to bring in PΛQ Since we have both P and Q in the premise, we can revive this and introduce Λ
9.2.2 Introducing and removing ↔︎
Rules for introducing ↔︎ (↔︎intro)
If A→B and B→A appear as one item in a derivation, then
We can add A↔︎B to that derivation.
A↔︎removal rule (↔︎elim)
If A↔︎B and A (or B) appear as one item in a derivation, then
If A↔︎B and A(or B) appear as one item in the derivation, you may add the other B(or A) to the derivation.
9.2.3 Introduction and removal of ¬.
¬Removal rule (¬elim)
If ¬¬A appears as an item in a derivation
A may be added to that derivation.
In short, double negation can be removed.
¬Introduction rule (¬intro)
If derivation D contains a contradiction derivation from A as an entry
¬You can add A as an entry in D
In other words
If it turns out that assuming A leads to a contradiction, you can claim that it is not A.
Derivation of Contradiction from A
A derivation that starts with the assumption that A is a logical formula and its negation both appear in the derivation
Strategy: How to get to ¬.
In order to get to ¬A, try to derive some contradiction from A
Example
Deduce ¬(PΛQ¬) from P→Q.
(1) Create a framework for the deduction first.
(2) To aim for →, you must
Assume that PˬQ
Lead to some contradiction (contradiction!)
(2) To go for →, assume PΛ¬Q, and derive some contradiction (contradiction!), and get ¬(PΛ¬Q) by the ¬introduction rule.
(3) What kind of contradiction do we derive (using resurrection and elimination rules)?
Strategy on how to make a contradiction
Example
Deduce ¬(PΛQ) from ¬(P→Q)
(1) Conventional strategy
(2) Contradiction is obtained if P↔︎Q is obtained for ¬(P↔︎Q) from the resurrection
Derive P↔︎Q.
(3) Resurrect PΛQ to derive Q and P respectively in each lower derivative.
Strategy: How to find the contradiction
Under the assumption of A, when you want to find a contradiction but can’t
Look at the logical formulas around A.
If there is a form ¬B there, try to get B.
9.2.4 Consecutive Words are Easy, but Elective Words are Complicated
Vintroduction Rule (Vintro)
If you can say A or B, you can say A or B.
If you already know A or B, you can say AⅤB
If A or B has been mentioned before as an item in the same derivation, you can add AⅤB
Strategy: How to get to V
To get to AⅤB, you only need to reach either A or B.
Example
Deduce P→(Q→R) from P→Q
(1) Create a framework for the deduction first
(2) To get to →.
(3)
V elimination rule
The problem is the V elimination rule
You can’t remove V from A V B and get A or B
Why?
A V B says nothing at all about which of the alternatives is true.
The V-removal rule for couplings is a statement of what more can be said from A and B, assuming they are true.
There is nothing more to be said about A and B from A V B alone.
With the help of other logical formulas
V elimination rule (Velim)
If A V B, A → C, and B → C already appear in the same derivation, then C can be added to that derivation.
We know that the two cases, A and B, have been exhausted, and
If we know that we have exhausted the cases of A and B, and we can deduce C in either case
You can always say “C” without any distinction.
Strategies for this rule
Strategy: If you want to start with V
In order to get to C from the selection A V B
First, derive the two equations A→C and B→C.
Example
Deduce (PⅤR)→(QⅤS) from P→Q and R→S
(1) Create a framework for deduction.
(2) How to get to →.
(3) If you start from V
9.2.5 Indirect proofs as a last resort
What to do if the previous strategies don’t work
Strategy: Indirect illumination as a last resort
When you want to get to A, but all other methods fail
First, derive a contradiction by assuming ¬A
Use ¬intro to get ¬¬A
Then use ¬elim to remove the double negative and get A.
Example
Deduction of the law of contradiction
Show that P→Q and ¬Q→¬P can be deduced from each other
(1)
(2)
(3)
(4)
Proof of the law of exclusivity
The law of exclusivity, P V ¬P, requires indirect proofs to create Proofs.
(1) Create a deductive framework, the last resort is indirect proof
¬Assume ¬(P V ¬P), derive ¬(P V ¬P) by deriving a contradiction, and eliminate the double negative
(2) How to make a contradiction
Since we have ¬(PⅤ¬P), we can derive a contradiction by generating PⅤ¬P.
(3) How to get to V
To get P V ¬P, we can use “How to get V” and get P or ¬P.
For now, we’ll use ¬P.
(4) How to achieve ¬?
To get ¬P, we can use “How to get ¬” and derive a contradiction by assuming P.
(5) How to make a contradiction
Since there is ¬(PⅤ¬P) under the premise bar, we will produce PⅤ¬P
Since we have P in the premise, we can get P V ¬P right away with Vintro

9.3 We might as well introduce a contradiction symbol

9.3.1 Superlative Deduction?
Trying to deduce half of Domorgan’s law, ¬PΛ¬Q to ¬(PΛQ)
(1)
Formulate a policy
(2)
Derive a contradiction from PⅤQ, follow “if you start from V”.
(3)
Contradiction!” denotes that A and ¬A appear simultaneously
→P→contradiction cannot be made by applying the rule of INTRO
(4)
Contradiction must be a contradiction of some kind.
(5)
9.3.2 Introducing Contradiction Symbols
Treat Contradiction! as if it were a single expression and make a deduction
Instead of ¬intro
¬intro* instead of ¬intro
¬elim* instead of ¬intro
Rewrite the above deduction Translated with www.DeepL.com/Translator (free version)

9.4 Extensions to Predicate Logic

9.4.1 Tribe Removal Rules and ∃ Removal Rules
Extending Natural Deduction to Predicate Logic
∀Tribe Removal Rule (∀elim)
| ∀𝛏A | | A[α/𝛏].
∃introduction rule (∃intro)
| A[α/𝛏] | | ∃𝛏A
(1) Deduce PaΛPb from ∀xPx.
(2) Deduce ∃xRaxa from Raaa.
(3) Deduce Pa→Ra from ∀x(Px→Qx) and ∀x(Qx→Rx).
To create a framework and to aim for →.
9.4.2 ∀ introductory rule
∀ intro rule ∀ intro
| A[α/𝛏] | | ∀𝛏A
Not always available.
It needs to be written
∀Tribe says the following
For any α chosen arbitrarily as a representative of all things
If we know that A[α/𝛏] is
then you can claim it for all things.
How can we make the conditional statement
What conditions should we impose on the ∀ introduction rule?
It does not follow from the fact that a is P and that all P is Q that ants and all things are Q
(1) The above deduction must be forbidden.
(2) a in the second line is not arbitrary, introduced as a representative of all things satisfying ∀x(Px→Qx)
a is a particular thing that satisfies P
Qa in line 4 is just saying that Qa holds for a particular a
Therefore, again no generalization is possible
(2) The above is good.
For all things, it is true that P and that if P, then Q.
Choose a arbitrarily as a representative of all things, and derive lines 3 and 4.
From here, Qa is derived.
The a in Qa has not lost its character as an arbitrarily chosen representative of all things.
There is no further information about what a is.
Finally, we can generalize to ∀xQx
Where do the above differences come from?
At the stage of introducing ∀.
In (1), a appears in the assumption that a is uncanceled (the expression with prem)
In (2), it does not appear in the assumption that a is not cancelled
A proviso to ∀intro
However, it is assumed that α does not appear in a premise that has not yet been cancelled until the stage where the rule is applied
(3) Correct deduction
In line 5, a appears in the premise.
This premise is cancelled in the last line, so it does not violate the proviso
(4) Incorrect deduction
Generalizing a fixed definite term that appears in a premise that is not cancelled
Introducing ∀ in line 10 violates the proviso
Another proviso
The rule for introducing ∀ requires one more proviso
To prevent false deductions like the one above
All people love me” does not imply “All people love Jody.
The above proviso is not violated.
The “a” doesn’t appear in the uncanceled premise.
The problem lies in the fact that you left out one thing when generalizing Laa’s a in line 3
∀introduction rule (∀intro)
| A[α/𝛏9] | | A𝛏A
However
(1) α is assumed not to appear in assumptions that have not yet been canceled at the time the rule is applied.
(2) α must not remain in ∀𝛏A
An individual definite term that can be generalized by the ∀ rule only conveys the information that “of course it can be said about an arbitrary thing”, and
When you replace “arbitrary” with “everything” (that is, when you introduce Tribe), it is a dummy that disappears from the stage.
Strategy: How to get to Tribe
To get to ∀𝛏A, we need
Derive A[α/𝛏] and apply the ∀ introduction rule to it.
However
Α must be chosen from among the individual definite terms in ∀𝛏A and the individual definite terms other than those that appear in the uncancelled assumptions in the derivation that yields ∀𝛏A.
9.4.3 The ∃ Removal Rule is More Complicated
We can’t extract any more definitive information about A and B from the unspecified information about AVB.
No more definitive information about A and B can be drawn from the unspecified information that there is something that we don’t know about, but is there anyway.
I don’t think we can extract any more information from the unspecified information that we don’t know which one it is, but it’s something.
The V elimination law approach
When A V B
Even if we don’t know whether A or B is true
Even if we don’t know whether A or B is true, if we can say that C is true anyway, whether it’s A or B
we can assert that C is definite.
Similarly, for ∃
We can say that there is a P
Even if we don’t know which one is that P
Even if you don’t know which one is the P, if you can say “whether it’s the P or not, it’s a C anyway
then it’s okay to claim it’s C.
∃ Removal Rule (∃elim)
Example of use
The ∃xQx in line 7 is derived only under the assumption that it is Pa.
The ∃xQx in line 8 is derived without the assumption of Pa
What is the ∃ removal rule?
Suppose we know that there is something A.
Let’s say that we know that there is a thing A, and if we name that thing A as α and reason about it, we get the thing C.
At this point, forgetting that you named the thing A as α
You can draw out the information C from the information that there is something A.
Example
Apparently, there is a person who drank the water here.
Let’s say that person is Jastomo.
All the people who drank mercury-contaminated water would have mercury coming out of their hair.
Mercury should come out of Yastumo’s head hair.
There must be at least one person whose hair is contaminated with mercury
Let’s consider the proviso
The name to be introduced above, “Yastumo” (or the individual definite term α), has the following two properties
(1) It is “arbitrary”, similar to the case of ∀introduction.
(2) It is “arbitrary”, similar to the ∀introduction case, except that in the ∀introduction case the individual definite term is literally arbitrary
In the case of ∃-removal, it is arbitrary insofar as it is A.
(2) The individual definite term is just a double that acts as a go-between for the conclusion C.
The only thing that is conveyed to the conclusion C is the information that “there is something A, whatever it is”.
The information about which is the A thing must not remain in the conclusion C.
The above shows that there are some conditions for the individual definite term α.
First of all, we can say the following from (1)
(a) α must not carry any more information than “something that is A”.
So α must not appear in a premise that remains uncancelled during ∃ elimination.
This is similar to ∀intro.
(b) Furthermore, α must not appear in ∃𝛏A either.
(c) Information about α must not remain in the conclusion C.
Therefore, α must not appear in C
Violating (a), (b), and (c) will result in the above mistakes
Examples of Using the ∃ Removal Rule
Let us deduce ∃x(PxⅤQx) from ∃xPx
(1) construction
(2)
(3)
Strategy: If you started with ∃.
In starting with an existential quantifier and deriving the target expression
Once you think you have to remove that existential quantifier
Attempt to create a subderivation that goals at that target expression and apply the ∃ removal rule.
Examples of how to use this strategy
(1) Make a deduction like the one above
(2)
(3)
(4)
9.4.4 Tackling de Morgan’s Law
Deduce ¬∀xPx from ∃x¬Px
Deduce ¬∀xPx from ∃x¬Px
(1) Apply “if you start with ∃” to get the desired expression using the ∃ elimination rule
(2) To derive ¬∀xPx, apply “To go for ¬” and assume ∀xPx to derive a contradiction
(3) Revive the equation that can be revived
Deduce ∃x¬Px from ¬∀xPx
(1) Follow the “Create a Deduction Framework”.
There is no rule that can be directly applied to an expression starting with the premise ¬∀.
(2) Introduce an indirect proof
(3) Revive what can be revived to create a contradiction.
We can derive ∀xPx somehow.
(4) To derive ∀xPx, derive Pa for any individual definite term a by “How to go for ∀” and apply the ∀ introduction rule to it
(5) Use indirect proof (assume ¬Pa and derive Maojun)
Strategy: If you want to start with ¬∀ and ¬∃.
There are no rules of inference that directly transform expressions of the form ¬∀A, ¬∃A.
Therefore, consider using these expressions in their entirety, deriving ∀A and ∃A and then contradicting them.
Then the deduction will be in the form of a completion proof.

9.5 Natural Deduction with Identity Symbols

= elimination rule (=elim)
A(α/β) denotes an expression in which the individual definite term β in equation A is replaced by the individual definite term α in several places (not necessarily all of them).
=introduction rule (=intro)
The expression with the form α=α can be left without any assumptions at any stage of the deduction.
What good is a rule like this?
Proof of ∀x(x=x)
(1)
Assume that a=a is A, and substitute a=b for the left-hand side of a.
(2) Translated with www.DeepL.com/Translator (free version)

Chapter 10: Approaching the Goal of Logic from a Syntax Perspective
10.1 The Idea of Axiomatic Systems

10.1.1 Enumerating All Logical Truths
From the semantics point of view, logical truths are regarded as a tautology (a valid formula in predicate logic).
Whether a given formula is a tautology or not can be checked by
truth table or tableau.
The above formulas are just a confirmation for each formula.
Isn’t it possible to grasp the whole tautology by saying, “This is the only tautology”?
There are infinitely many tautologies.
Inductive definitions are used to define infinite tautologies.
Methods for doing so “axiomatic system
(1) Select some representative tautologies as a starting point.
The starting point is called “axiom”.
(2) Formulate rules to create all the remaining tautologies from the representatives of the tautologies chosen as starting points.
The rules are called “rule 0f inference” or “rule of transformation”.
(3) Prove that all the logical formulas obtained by the above procedures are tautologies, and that all the tautologies are exhausted by the procedures.
The proof is called a “complete proof.
10.1.2 Axiomatic Systems of Propositional Logic
A system of axioms in propositional logic designed to capture all tautologies within the scope of propositional logic.
A1 P→(Q→P) A2 (P→(Q→R)→((P→Q)→(P→R)) A3 (P→(Q→R))→(Q→(P→R)) A4 (P→Q)→(¬Q→¬P) A5 ¬¬¬P→P A6 P→¬¬P R! We can extract B from A and A→B (separation rule: modus pones, MP for short) R2 P1 ,…. Suppose that Pn is a primitive expression. Suppose P1 ,…,Pn are primitive expressions. P1,…,Pn in one equation can be replaced by the ethical equations B1,…,Bn all at once. P1,…,Pn in one expression can be replaced by the ethical expressions B1,…,Bn all at once (substitution rule, rule of substition, RS for short).
In Frege’s axiomatic system, there is no logical fixed point such as V, and it is limited.
What do we do?
D1 AΛB=df¬(A→¬B) D2 AⅤB=df¬A→B D3 A↔︎B=df(A→B)Λ(B→A)
PⅤ¬P is another way to write ¬P→¬P
Axiomatic system APL (axiomatic system for propositional logic)
A1 A→(B→A) A2 (A→(B→C))→((A→B)→(A→C)) A3 (¬B→¬A)→((¬B→A)→B) R1 MP
Logical theorems not listed here are introduced by definitions D1-D3.
The axioms themselves are written using schematic letters A, B, etc.
A1 is not a single logical formula, but a set of countless logical formulas in the form of A→(B→A) such as P→(Q→P), (P→Q)→(R→(P→Q))
A1 says “any logical formula in the form of a deer is an axiom”.
A1 to A3 are sometimes called an axiom schema.
No more substitution rules
P → P is a tautology, but it is not part of APL retail
It is derived from one of the axioms of APL by applying it with inference rules
(1) P→(P→P)→P) ….. A1 (2) (P→((P→P)→P))→((P→(P→P))→(P→P)) ……. A2 (3) (P→(P→P)) →(P→P) …….. (4) P→(P→P) ……. A1 (5) P→P ……. (3)(4) to MP
10.1.3 Concepts defined for axiomatic systems
theorem and proof
For the axiomatic system APL, we define theorem and proof in APL as follows
Definition
(1) A finite sequence B1, B2,…,Bn of logical formulas satisfying the following conditions. (1) A finite sequence of logical formulas B1, B2,…,Bn (where the last Bn is C) is called a proof of C in APL.
Condition
Bi (but 1≤I≤n) is one of the following
(a) It is an axiom of APL
(b) It is a formula drawn from the preceding Bj and Bk by the inference rule MP.
(2) If there exists a proof of C, then C is a theorem of APL. Also, C is provable in APL.
The proof defined here is a sequence of logical expressions that satisfy certain conditions.
Theorem is the “logical formula itself” at the end of the sequence.
This is completely different from “theorem 25” and its proofs, which are “statements of facts about the properties of logical expressions in Japanese” and “theorems and proofs as proofs of their correctness.
Therefore, it is expressed as “theorem” or “proof”.
Example of proof from axioms
The above derivation of P → P satisfies the condition of proof in APL.
Theorem in APL
(1) (P→(Q→R))→((P→Q)→(P→Q)) ………. A2 (2) ((P→(Q→R))→((P→Q)→(P→R)))→((Q→R)→((P→(Q→R))→((P→Q)→(P→R)))) …… A1 (3) (Q→R)→((P→(Q→R))→((P→Q)→(P→R))) ……… MP from (1) and (2) (4) Omitted below
The (P→Q)→((Q→R)→(P→R)) that will appear now is theorem of APL.
Soundness and Completeness of Axiomatic Systems
The aim of creating an axiomatic system is to count up all tautologies
The following two things must hold
(1) Any tautology can be found by starting from one of the above three forms of axioms and transforming it by MP.
(2) Any logical formula that comes out in this way is a tautology.
The logical formula A is a tautology of AgaAPL ⇔ A is a tautology
Definition
Axiom K is “sound” if A is theorem of K ⇒ A is tautological. Conversely, axiom K is “complete” if A is tautological ⇒ A is theorem of K.
A system is said to be complete if it is sound and complete.
10.1.4 Deduction from Assumptions
I was just messing around and got it!
Axiomatic systems also give us a different way of looking at the concept of logical consequence.
Example: Math problem
Let Sinθ+cosθ=√2. Find sin2θ in this case.
Squaring both sides anyway
sin2θ + 2sinθcosθ + cos2θ = 2
That reminds me, “sin2θ + cos2θ = 1
Substitute
1 + 2sinθcosθ = 2
2sinθcosθ = 1
That reminds me, “2sinθcosθ = sin2θ”.
Substitute
sin2θ = 1
The answer is 1
I don’t know what the equation means, but
I was transforming it in the dark and got the answer I was aiming for.
Now let’s review the proof of P→P
Even if you only look at the form of the equation, you can construct a proof.
Consideration of the psychological conditions of “→” being “if” or “A → B” is irrelevant to the construction of proof.
Proof is from a position of total ignorance of meaning and truth, i.e., from a position of syntax.
Deduction from assumptions
The mathematical example just given
(1) The starting point sinθ+cosθ=√2 is an expression which is an assumption given in the problem
The equation assumed to be valid only for this problem
(2) The other equations sin2θ+cos2θ=1 and 2sinθcosθ=sin2θ are so-called “formulas”.
Formulas that can be used at any time
Formulas that can be used in any problem
What we usually call “solving a proof problem” is
What we usually call “solving a proof problem” is to derive a target formula from a specific formula given in the problem (this is called an assumption).
At that time, we introduce a formula that can be used at any time, called a formula, to derive the target formula.
Using the tool of axiomatic systems, we can reconsider “proof” as a process of arriving at a target formula starting from a given specific assumption.
This is called “deduction”, not “proof”.
The previous example
Deduction from sinθ+cosθ=√2 to sin2θ=1
Two formulas are used in this process (axioms in logic)
Definition
(1) Let Γ be a set of logical formulas, and let B1,B2,…,Bn(Bn) be a finite sequence of logical formulas satisfying the following conditions (1) Let Γ be a set of logical formulas, and let B1, B2,…, Bn (where Bn is C) be a finite sequence of logical formulas, B1, B2,…, Bn (where Bn is C), satisfying the following condition.
Condition
Bi (but 1≤I≤n) is one of the following
(1) It is an axiom of APL
(2) It is an element of Γ
(3) It is a formula induced by the inference rule MP from the preceding Bj and Bk.
(2) If there exists a deduction from Γ to C, then C is deduced from Γ. (2) When there exists a deduction from Γ to C, C is deduced from Γ, or deducible, and is written as Γ⊢C
⊢:turnstile
A logically elaborated view of the concept “C logically emerges from Γ”.
It is similar to the double turnstile “⊨”, but they are completely different.
Deduction is also nothing more than a sequence of logical formulas that satisfy certain conditions
Examples of deduction from assumptions
Show that P→Q, P→(Q→R) ⊢ P→R
(1) P→Q …….. Assumption (2) P→(Q→R) ……. Assumption (3) (P→(Q→R))→((P→Q)→(P→R)) ……. A2 (4) (P→Q)→(P→R) ……. (2)(3)MP (5) P→R …… (1)(4)MP
Indicates that P→Q, O→R, and P⊢R
(1) P→Q ….. Assumption (2) P ……. Assumption (3) Q ……. (1)(2)MP (4) Q→R …… Assumption (5) R …… (3)(4) Assumption
Proof is a special case of deduction
Difference between the two
Deduction starts with several equations other than retail as assumptions.
In Proof, only axioms are used.
Proof is a special case of deduction that starts with zero assumptions
In Γ⊢C, proof is when Γ is the empty set.
Therefore
The fact that C is a theorem is written “⊢C”.
Properties of deduction
The following holds for deduction from Γ
Theorem 37.
(1) A ∈ Γ ⇒ Γ⊢A (2) Γ⊢A and Γ ⊆ Δ ⇒ Δ⊢A (3) Γ⊢A ⇒ Γ’⊢A (4) There is a suitable finite set Γ’ such that Γ’ ⊆ Γ ⊢A ⇒ Γ⊢A (5) Γ⊢A and Γ⊢A → B ⇒ Γ⊢B (6) {Δ for all logical formulas B contained in Γ⊢A and Γ ⊢B} ⇒ Δ⊢A (7) {Γ⊢A and Δ,A⊢B} ⇒ Γ,A⊢B
10.1.5 Deduction Theorem
For “⊢” defined above, the following facts hold
Theorem 38: Deduction theorem
Γ,A⊢C ⇔ Γ⊢A→C
Deduction theorem is useful
It is hard to make a proof of the transitive law (P→Q)→((Q→R)→(P→R))
If we use the deduction theorem repeatedly
⊢(P→Q)→((Q→R)→(P→R))
P→Q⊢(Q→R)→(P→R)
P→Q, Q→R⊢P→R
P→Q, Q→R, P⊢R
If we show that there is a deduction to R assuming that P→Q, Q→R, P
(P→Q)→((Q→R)→(P→R)), we can say that there exists a proof
Proof of the Deduction Theorem
Prove the direction Γ,A⊢C ⇒ Γ⊢A→C Translated with www.DeepL.com/Translator (free version)

10.1.6 Use of theorem in deduction and derivation rules
Once you have shown the existence of a proof, use theorem as a diagram.
Example
Show the double negative rule (⊢¬¬P→P)
By the deduction theorem
We can show that ¬¬P⊢P
(1) ¬¬P ……. Assumption (2) (¬P→¬¬P)→((¬P→¬P)→P) ……… A3 (3) ¬¬P→(¬P→¬¬P) …….. A1 (4) ¬P→¬¬P …… (1)(3)MP (5) (¬P→¬¬P)→P ……… (2)(4)MP (6) ¬P→((¬P→¬P)→¬P) …… A1 (7) (¬P→((¬P→¬P)→¬P))→((¬P→(¬P→¬P))→(¬P→¬P)) …… A2 (8) (¬P→(¬P→¬P))→(¬P→¬P) ……. (6)(7)MP (9) ¬P→(¬P→¬P) …… A1 (10) ¬P→¬P …… (8)(9)MP (11)P …….. (5)(10)MP
In (6) to (10), the P in the proof of P→P is replaced by ¬P and repeated again.
Theorems that are known to have proof can be used freely in deduction and proof, just like axioms.
Furthermore
Once the proof of P → P has been made
If we replace the “P” in the proof with “(Q→¬R)”, we can use it as a proof for (Q→¬R)→(Q→¬R).
There is a proof for ¬¬P → P
Once proofed, it is allowed to be used as a “diagram”.
(1) ¬¬¬P (2) (¬P→¬¬¬P)→((¬P→¬P)→P) ……. A3 (3) ¬¬P→(¬P→¬¬P) …….. A1 (4) ¬P→¬¬P …….. (1)(3)MP (5) (¬P→¬P)→P ……. (2)(4)MP (6) ¬P→¬P ……… theorem1 (7) P …… (5)(6)MP
Break off ¬P→¬P proof
Derivation rules
Examples
Suppose we know that P→Q, Q→R, and P⊢R.
Call this deduction D
When doing other deductions, if three formulas P→Q, Q→R, and P appear in a column of logical formulas
If we continue to write R in that column, it does not violate the condition for a proper deductionw@.
Then
If it turns out that P→Q, Q→R, and P⊢R
If we know that P→Q, Q→R, and P⊢R, we can treat the rule “If P→Q, Q→R, and P, we can extract R” as if it were an inference rule analogous to MP.
Furthermore, we can change the primitive commands P, Q, and R into other logical formulas all at once.
This means that
You can think of it as getting an inference rule that says, “A→B, B→C, and from A you can extract C.”
These are rules derived from the axiomatic system APL
Derived rules so far
D1 You may extract A→C from A→B, A→(B→C) (page 254) D2 You may extract A→B, B→C, C from A (page 254) D3 You may extract B→A from A (Exercise 77, (1)) D4 You may extract (A→B)→B from A (Exercise 77, (2)) D5 You may extract A→B D6 A→B, B→C to A→C (page 256) D7 A→(B→C), B, A to C (Exercise 78(2)(a)) D8 A→(A→B), A to B (Exercise 78(2)(b)) (2)(b) of Exercise 78) D9 ¬B→¬A, you may withdraw B from A (2)(c) of Exercise 78) D10 ¬B→¬A, you may withdraw A→B from A (2)(c) of Exercise 78) D11 ¬¬A, you may withdraw A from A (page 258)
10.1.7 Natural deduction is a kind of axiomatic system
There are various axiomatic systems
There are many axiomatic systems in propositional logic.
Examples of axiomatic systems different from APL
Meredith’s axiomatic system M
A1 (((P→Q)→(¬R→¬S))→R)→T)→((T→P)→(S→P)) R1 MP R2 RS
It is necessary to distinguish which axiomatic system
⊢APLB or ⊢MB
Natural deduction is also an axiomatic system
Taking Meredith’s axiomatic system one step further, an axiomatic system without any axioms
Natural deduction
No axioms, just rules of inference

10.2 Syntax and Semantics

10.2.1 Two ways of thinking about logical consequence
Goals of Logic
The goal was to investigate what is logical correctness, (what does it mean to come out logically)
There are two ways to answer those questions
Semantic Consequences
One is “the concept of logical consequence with semantics as a tool.”
Logical formulas A1, A2,… ,C comes out logically from An, which means that
A1,A2,… ,C is also always true under a truth assignment/model where An is all true.
Under this idea, the fact that C is logically true means that
C will always be true under any truth-value assignment/model.
(In other words) “C is a tautology/validity formula”.
These logical consequences or logical truths can be viewed as
This way of thinking about logical consequence and logical truth is based on the perspective of what interpretation to assign to symbols.
The department in charge of assigning meanings to symbols and the various things that derive from them
Truth tables and models belong to semantics.
Concepts such as tautology, valid expressions, and logical equivalence all belong to semantics because they are related to truth.
The concept of logical consequence displayed by “⊨”
This line of thought is based on the intuition that the concept of logical consequence should be revealed by the meaning of a logical definite term.
The concept of syntactic consequence
A different way of looking at the concept of logical consequence than the above
The concept of logical consequence is based on the intuition that it is only a matter of “the form of the expression” whether it appears logically or not.
Under this idea
Logical formulas A1, A2,… The fact that C comes out of An logically means that
In the axiomatic system APL (or ND), if A1, A2,… In the axiomatic system APL (or ND), there exists a deduction of C assuming A1,A2,…,An.
A1,A2,…. An and the axiomatic system of APL as a starting point, apply the inference rules in order and replace them to arrive at C
That the logical formula C is a logical truth.
That there is a deduction of C that makes no assumptions.
(In other words) that C is a theorem.
In the process of constructing a deduction
The process of constructing a deduction does not require any consideration of meaning or truth conditions.
Example
MP of inference rule: “We may deduce B from A and A→B”
Not “A and A→B are true, so if we have A and A→B, we may also write B.”
If an expression of the form A and A→B appears in the deduction, you may take out the part B and write it next.
A position that views language purely as a series of figures, and considers logic by focusing only on how the symbols are arranged and in what form.
Why do we do the “P→P” proof in APL?
It is necessary to distinguish between syntax and semantics.
The syntax perspective
P→P is a sequence of shapes
It has no meaning, so it is not self-evident
A “proof” is nothing more than a sequence of expressions that satisfy certain conditions
What we can learn by making proofs of P→P
It does not mean that P→P is true or tautological
By transforming the expression from the axioms according to the rules, we can arrive at the sequence of symbols P→P
It is not obvious whether or not the symbol sequence P→P can be obtained from the axioms given in APL by simply rewriting the formal symbols.
Semantics perspective
It is obvious that P → P is true
Why has the syntax position been established?
It has to do with the fact that modern logic arose in mathematics.
In mathematics, proofs and deductions are made for numbers and sets.
What do you do when you want to investigate a mathematical proof with confidence?
The only way is to use mathematics to look at the proof itself.
View a proof as a sequence of figures constructed according to strict rules.
10.2.2 The Concept of Contradiction Captured in Syntax
Logic has three objects of study
(1) The concept of logical consequence
(2) The concept of logical truth
(3) The concept of logical contradiction
There are two approaches to these
Semantics that focuses on the meaning of logical definitions
Syntax, which ignores the meaning and focuses on the graphic transformation game-like aspect of logic
Research objects (1) and (2) are described above.
The remaining (3), the concept of logical contradiction
Position of Semantics
Definition
A set of formulas Γ is semantically inconsistent (written as Γ⊨).
⇔
There is no truth-value assignment/model that makes all expressions belonging to Γ true at the same time.
If Γ is semantically consistent, then Γ is satisfiable or consistent.
Syntax’s position
Definition
A set of expressions Γ is syntactically inconsistent (written as Γ⊢).
⇔
There exists a logical formula A such that Γ⊢A and Γ⊢¬A.
We say that Γ is inconsistent when Γ is syntactically consistent
These definitions lead to a very similar result
Theorem 39.
(1) Γ is semantically inconsistent ⇒ for any formula B, Γ⊨B
(2) Γ is syntactically inconsistent ⇒ for any expression B, Γ⊢B
(3) Γ is syntactically inconsistent ⇒ for any formula B, Γ⊢B
If we want to prove that Γ is syntactically consistent, we need only one logical formula that cannot be deduced from Γ
Syntactic inconsistency
We can define syntactic inconsistency for axiomatic systems as well as for formula sets.
Theorem
An axiom system K is syntactically inconsistent
⇔
There is no logical formula A in K such that ⊢A and ⊢¬A.
Theorem 41.
APL is inconsistent.
10.2.3 Why is completeness important?
Summary of syntax and semantics approach
Do the logical consequences of semantics and syntax ever overlap?
Yes, for APL and ND.
When a complete proof works
There is an overlap between the semantic and syntactic ways of thinking about “logically emerges”.
Overlap does not mean that the concept of semantic consequence and the concept of syntactic consequence are the same concept.
It means that the sets of each other coincide in extent. Translated with www.DeepL.com/Translator (free version)

10.3 Completeness proofs for axiomatic systems of propositional logic

10.3.1 Completeness theorems and the advantages of proofs by Henkin
Proof of the Low Completeness Theorem
Strong Completeness Theorem
A claim that the set of theorems of an axiomatic system coincides exactly with the set of tautologies.
The foregoing is a special case of the above
The notion of logical induction captured by semantics and that captured by syntax coincide exogenously.
The completeness theorem is a theorem that acts as a bridge between syntax and semantics.
What we are going to prove is a slightly stronger result.
Theorem 42
Strong completeness theorem
Why is it strong?
Γ can be an infinite set
Γ⊢B is
There is a deduction of B such that every process is an element of Γ
We do not require that every element of Γ be used in the deduction of B
Γ⊨B ⇐ Γ⊢B
Proof of
When B1 is retail, all the axioms of APL are tautological
When B1 is an element of Γ, then by assumption V was a truth assignment such that it satisfies Γ, so B1 is true under V
C, which is derived from B1 under MP, is also true
Γ⊨B ⇒ Γ⊢B
Proof of Completeness
Leon Henkin’s proof
It is superior in the following two respects
(1)
Γ⊢B is a deduction from the hypothesis Γ to B.
(1) Γ⊢B is a deduction from hypothesis Γ to B, but the deduction is meaningless without the deduction of any axiom system.
Essentially, we need to prove completeness for all axioms.
It is desirable that the proof should be such that as few points as possible are affected by the special circumstances of the axiomatic system here.
(2)
Henkin’s Illumination is Extensible
It can be applied to axiomatic systems in various logics (e.g., modal logic).
10.3.2 Outline of Henkin’s proof
Henkin’s Theorem
First prove the completeness of APL
Can be rewritten as ND with a few modifications
Theorem 43.
For any set of logical formulas Γ and logical formula A, the following holds
Γ⊨A ⇔ Γ⋃{¬A} is not satisfiable (semantically contradictory)
Theorem 40.
For any set of logical formulas Γ and logical formula A, the following holds
Γ⊢A ⇔ Γ⋃{¬A} is syntactically inconsistent.
Theorem 44: Henkin’s Theorem
A set of logical formulas Γ is syntactically inconsistent ⇒ Γ is satisfiable
We need only prove that a syntactically consistent set of logical formulas always has a truth-value assignment that makes all the logical formulas in it true at the same time.
How do we prove Henkin’s theorem?
If we prove Henkin’s theorem, then we have a strong completeness proof.
The proof strategy is as follows
(1) To prove Henkin’s theorem, we need
(1) To prove Henkin’s theorem, we need to show that there is a truth-value assignment such that all logical formulas in a syntactically consistent set Γ can be true.
The most straightforward way is
The most straightforward way is to give a procedure for making such a truth assignment depending on Γ.
(2) By the way, just saying “it is syntactically consistent” does not give enough information about Γ.
There is too little information about Γ, and
We can’t construct such a truth assignment directly from Γ.
(3) Then, we can expand Γ in a certain way
(3) So we expand Γ in a certain way to create a proof-friendly set Γ* that completely contains Γ.
(4) Because of the way Γ* is constructed
(4) Because of the way Γ* is constructed, it is easy to construct a truth assignment that makes all the logical expressions in it true.
to be true.
(5) Since Γ* contains Γ
the truth assignment made in (4) will make all the formulas in Γ true.
Extremely consistent set
A provably convenient set Γ* that contains Γ in its entirety
a set that completely contains Γ as a subset and is
consistent
In a sense, the set is so close to the limit that there is no larger set.
Definition
The set of logical formulas Δ is maximally inconsistent.
⇔
Δ is syntactically inconsistent, and Δ⋃{A} is syntactically inconsistent for every logical formula A that is not an element of Δ.
If you add even one more formula that you don’t include, you instantly have a contradiction.
If we are dealing with Γ itself
If we are dealing with Γ itself, there is no way to construct a truth assignment that makes all of its expressions true.
If we extend Γ to the maximal inconsistent set Γ*, then
A truth-value assignment that makes all expressions in Γ* true is always easy to obtain by the same procedure
since Γ⊆ Γ*.
Since this truth-value assignment makes all expressions in Γ true
We know that Γ is satisfiable.
To prove that Tablau’s method is reliable
We will do the same thing with the extension of the open path to the Hinticka set
Two auxiliary theorems
To make Henkin’s theorem rain, we need to prove the following two auxiliary theorems
Auxiliary Theorem 44-1: Lindenbaum’s lemma
If Γ is a set of syntactically consistent expressions, then
When Γ is a set of syntactically inconsistent expressions, there exists at least one maximal inconsistent set Γ* such that Γ is a subset.
Auxiliary Theorem 44-2 : Satisfiability of Extremely Consistent Sets Auxiliary Theorem
Given a maximally consistent set Γ*, we have
Given an extreme-consistent set Γ*, a coherent truth-value assignment is determined that makes all expressions in Γ* true.
That is, the maximally consistent set is satisfiable.
10.3.3 Proof of Auxiliary Theorem 44-1
We give a two-step proof
(1) Given an arbitrary inconsistent set of expressions Γ, give a procedure for expanding it to Γ*.
(2) Show that Γ* is indeed an extremal inconsistent set when Γ is expanded according to the procedure.
Procedure for extending Γ to Γ*
The set of all logical formulas is enumerable.
All logical formulas can be enumerated in a row, numbered by a natural number.
Suppose we are given a single column enumerating all the logical formulas
We start with the consistent Γ, and take the logical formulas from this column in order.
If it is consistent to add it to Γ, then add it to Γ.
Repeat the above operation to expand Γ.
This operation leads to the maximally consistent set Γ*.
The concrete procedure
(1) Let Γ0=Γ.
(2) Assume that A is the i-th logical formula to appear in the enumeration of logical formulas.
Then
If Γi⋃{Ai} is syntactically consistent, let it be Γi+1
If Γi⋃{Ai} is syntactically inconsistent, then let Γi+1= Γi
Proof that Γ* is maximally inconsistent
(1) Proof that Γ* is maximally inconsistent
(2) Proof that Γ* is maximal.
10.3.4 Proof of Auxiliary Theorem 44-2
Two auxiliary theorems
Proof of Auxiliary Theorem 44-2
10.3.5 What follows immediately from the complete theorem
Theorem 45.
Adding any logical formula to APL that is not provable in APL as an axiomatic scheme is syntactically inconsistent
Another proof of the compactness theorem
Compactness Proof
Every finite subset of Γ is satisfiable
⇔
Γ is satisfiable
The above can be proved as a byproduct of the completeness theorem
Proof
Every finite subset of Γ is satisfiable
⇒ Every finite subset of Γ is consistent (by conformance)
⇒ Every finite subset of Γ is consistent (due to the finiteness of deduction)
⇒ Γ is satisfiable (by the completeness theorem)

Summary of Part III

In the next article, I will discuss my reading notes on Part 4 – Logic is Interesting from Here on Out: Non-Classical Logic.