week1
week2
week3
week4
week5
Week6
week7 The Limits of Matrices
Decide which logic can be reach via matrices and which is not.
matrix logic
Those logics can be decided by a matrix!
- CL, K3, LP, FDE
- universal logic
A matrix can determine a logic, but usually it is not the only matrix that determine this logic.
Another very important example is the empty logic, which is not a matrix logic. We can prove it by thinking of argument $p/p$. So there is a property of matrix logic: every matrix logic must contain arguments like $p/p$.
Reflexivity
By abstracting one of the feature of matrix, we consider reflexive logic: all arguments with form $A/A$ is valid in the logic. Hence every matrix logic is reflexive.
So we can consider the weakest reflexive logic(WRL), which only contains arguments like $A/A$.
Monotonicity
Now thinking of such kind of question: Is every reflexive logic a matrix logic? The answer is no, because WRL is not a matrix logic, which means $A/A$ cannot cover all arguments in matrix logic.
rule instance: it consist of some premise-arguments and a conclusion-argument. It is usually written in this kind of form:
\(\frac{p/q}{p \land q/r}\) \(\frac{p/p \quad p/q}{p,q/p}\) \(\frac{}{q \to r/s}\)
A logic obeys a rule instance if either:
- there exists premise-argument that invalid in the logic.
- the conclusion-argument is valid in the logic.
A rule consist of some rule instances, and a logic obeys a rule means it obeys every rule instances in the rule.
Now we can start with an important rule: monotonicity, which consist of rule instances of this kind of form:
\[\frac{\Gamma/A}{\Sigma/A}\]where $\Gamma \subseteq \Sigma$.
Using this rule we can define monotonic logic.
It’s easy to show that every matrix logic is monotonic. So here we are: every matrix logic is reflexive and monotonic.
Transitivity
However, we can still construct some logics that are reflexive and monotonic, but not a matrix logic. For example, the L1 logic, it contains $\Gamma/A$ iff either:
- $A$ is a member of $\Gamma$
- $A$ is $q$ and $p \in \Gamma$
- $A$ is $r$ and $q \in \Gamma$
It’s easy to check that L1 is reflexive and monotonic, but not a matrix logic.
Transitivity is a rule consist of rule instances in the form:
\[\frac{\Gamma/A \quad \Gamma,A/B}{\Gamma/B}\]Also, it’s easy to show that L1 is not transitive and every matrix logic is transitive.
Substituion Invariance
Substitution invariance is also a rule, which consist of rule instances in the form:
\[\frac{\Gamma/A}{\Sigma/B}\]with a substitution $s$ such that
- $s : \Gamma \to \Sigma$.
- $s(A) = B$.
It’s still easy to show that every matrix logic is substitution invariant.
week8
Models and proofs
In model-theoretic, we assume an counterexample to an argument, and say an argument is valid when it has no counterexample.
In proof-theoretic, we set up proofs, and say an argument is valid when it has at least one proof.
A natural deduction system
The basic building blocks in NJ is taking a sentence and supposing it. Every natural deduction has a top and a bottom. The top is what we supposing and the bottom is the conclusion.
For each connectives, NJ includes two kinds of rules: introduction and elimination. For example, for the $\land$:
\(\land I: \frac{A\quad B}{A \land B}\) \(\land E_l: \frac{A\land B}{A}\) \(\land E_r: \frac{A\land B}{B}\)
Let’s think about the meaning of these connectives. In the previous chapters we use structures to do this. Here, we use the rules to give meaning.
For $\lor$:
\(\lor I_l: \frac{A}{A\lor B}\) \(\lor I_r: \frac{B}{A\lor B}\) \(\lor E^n : \frac{A \lor B \quad \begin{array}{c} [A]^n \\ \vdots \\ C \end{array} \quad \begin{array}{c} [B]^n \\ \vdots \\ C \end{array}}{C}\)
Discharging an assumption: like classification and discussion. To draw a conclusion $C$ from $A\lor B$, we can assume $A$ and get $C$ and then assume $B$ then get $C$. Every discharging rule must have a label.
\[\to I^n : \frac{\begin{array}{c} [A]^n \\ \vdots \\ B \end{array}}{A \to B}\] \[\to E : \frac{A \to B \quad A}{B}\]Falsum elimination: \(\bot E : \frac{\bot}{A}\)
Verum introduction: \(\top I : \frac{}{\top}\)
Negation:
\[\neg I^n : \frac{\substack{[A]^n \\ \vdots \\ \bot}}{\neg A} \qquad\qquad \neg E : \frac{\neg A \quad A}{\bot}\]related links: https://incredible.pm
Two variantions
There are two variantions of NJ. The first one is NM: just remove the rule $\bot E$ from NJ.
Another variantion is NK, by adding rule LEM
\[LEM: \frac{}{A \lor \neg A}\]week9 Intuitionistic logic
How to get a logic from a natural deduction system
In a natural deduction system, a proof is the process from premises(open assumptions) to the conclusion. Given a proof, then the smallest argument of it is $\Gamma / A$, where $\Gamma$ is the set of open assumptions and $A$ is the conclusion.
We say a proof is a proof of an argument $\Sigma/B$ $\iff$ the smallest argument of the proof is $\Gamma/A$, where $\Gamma\subseteq \Sigma$ and $A=B$.
The logic determined by a proof system consist of all arguments that has a proof in the system.
Different proof system may result the same logic.
NK results in classic logic.
The logic resulted by NJ is called intuitionistic logic. The logic resulted by NM is called minimal logic.
Minimal, intuitionistic, and classical logics
Thinking of the relationship between NM, NJ and NK. Regarding them as set of proofs, then $NM\subseteq NJ \subseteq NK$, which means minimal logic $\subseteq$ intuitionistic logic $\subseteq$ classic logic.
From all we have learned, we can know that CL is very strong, and it has property called Post completeness, which means the only logic that is reflexive, monotonic, transitive, substitution invariant, and properly stronger than CL is the universal logic.
The logic determined by a natural deduction system also has the 4 properties: reflexive, monotonic, transitive and substitution invariant.
Philosophical issues
This is one thing some people mean by “realism”: the belief that there are unknowable truths.
Intuitionistic vs classical logics
An argument is an instance of modus ponens when it has the form $A\to B, A/B$.
CL validates modus ponens, which means it validates every instance of modus ponens. Similarly, for the matrix logic K3, it validates modus ponens. But LP and FDE can not validate modus ponens.
Considering NM, NJ and NK, it’s easy to see that minimal logic, intuitionistic logic and classical logic all validate modus ponens.
Conditional proof is not an argument like modus ponens, it’s a rule. A rule instance is an instance of conditional proof when it fits the form:
\[\frac{\Gamma,A/B}{\Gamma/A\to B}\]which means we can get a proof(argument) from another proof(argument).
CL and LP obey the rule but K3 and FDE and don’t obey it. Just considering the counterexample. Noticing that empty logic also obey the rule, because it doesn’t validate argument.
Also, the three logics from natural deduction system all obey conditional proof.
In the above case, minimal logic and intuitionistic logic sounds more like CL, but turning around, for the De Mogan’s Law, thes two logics cannot fit all the laws.
Sum up
- proof system NM, NJ and NK
- thier resulted logic: minimal, intuitionistic, and CL
- the properties of minimal and intuitionistic logics
Quiz:
- In intuitionistic logic, negation can be added, but can not be eliminated
- Noticing that for the conditional proof, we can use multiple premises
week10 Intuitionistic models
模型论(model-theoretic lens)到底怎么理解？
Valuations in structures is a kind of model.
key:
- what a model is?(finally i begin to get the answer haha)
- what is an counterexample in the model?
The models
For the intuitionistic logic, the model we will build consist of a frame and a valuation on it.
So what is a frame? In fact some points and arrows between points. For example:
The key for a frame is its points and reachability relationship between them. The set of points can be finite or infinite.
We will have 2 values in the model: Y and ?. For a sentence A, it may take different value at different points, for example we can write $M(A,x)=Y$.
We assume each point a set of atomic sentences, which means at the point these atomic sentences get value Y. But there are some constraints for the atomic valuation: since we can think of the frame as knowledge that never lose, so if $M(A,x)=Y$ and $xRy$, then we must have $M(A,y)=Y$. (called persistence when A extended to compound sentences)
An intuitionistic model is a frame, plus a valuation on the frame.
For the compound sentences:
$M(\neg A,x)=Y$ iff every $y$ that reachable from $x$ has $M(A,y)=?$.
$M(A\to B,x)=Y$ iff every $y$ that reachable from $x$ has $M(A,y)=Y \implies M(B,y)=Y$.
counterexamples
Special kinds of models
Total models means for any $x$ and $y$, whether $xRy$ or $yRx$.
This model determines a stronger logic than intuitionistic logic. Here is an extra argument, since it has a counterexample but it’s not a total model. And we can prove this argument don’t have a total model as a counterexample. The logic is called LC.
One-point models means those models only contains one point. It’s easy to see that all one-point models are total. It determines the CL and properly stronger than LC. Just check this argument and its counterexample in CL:
For those logics between intuitionistic logic and CL, also with properties reflexive, monotonic, transitive, and substitution invariant, they are known as intermediate logics.
Sum up 10
上一周我们用证明论构造了 intuitionistic logic, 本周我们用模型论构造了这个逻辑。每个模型都由 frame 和一些 points 构成。再加上由 reachability 给出的对 valuations 的限制，我们可以给出 counterexample 的定义。