\[ \newcommand{\negp}{\neg p} \newcommand{\negq}{\neg q} \newcommand{\negr}{\neg r} \newcommand{\r}{\rightarrow} \newcommand{\rl}{\leftrightarrow} \newcommand{\any}{\forall} \]
Proposition is a statement which got a determined truth value. Atomic Proposition is proposition which is indivisible, Compound Proposition is combined by atomic propositions.
There’re five basic operations affected on propositions, one unary operation and four binary operation, the binary operation are also called Connective. Operations includes negation \(\neg p\), conjunction \(p \land q\), disjunction \(p\lor q\), implication \(p\rightarrow q\), and equivalence \(p\leftrightarrow q\).
In the implication connective, \(p\) is called antecedent, \(q\) is called seccedent. The implication is false if and only if \(p=1,\ q=0\). In other words, the truth table of this
==TODO: Draw truth table for implication, and develop the method of auto-generating truth table.==
This implies an important feature about implication, which usually called implication identity: \[ p\r q \quad=\quad \negp\lor q \] This is important in the transformation of logic expression, which converts the abstract implication into simple disjunction.
A variable that represents a proposition is called proposition variable, and the const proposition is called proposition const. We defined the proposition formula recursively like this:
Only those symbol string can be generated from those two rules are proposition formula.
Notice that the proposition formula is just the form of proposition but not the actual proposition. For instance, the formula \(A: p\r q\) is a proposition formula, only when we let \(p=\text{It's sunny}\), \(q=\text{we're going to hiking}\), or let \(p=\text{One works hard}\), \(q=\text{One gets grade 4.0}\), then the formula becomes a proposition after the assignment. This shows that multiple different propositions can be abstracted into the same proposition formula. This distinction is quite important because this drived the grammar from specific semantic, which makes the inference a pure symbol conversion process.
For the convenience of further discription, the proposition variable and its negation are called literal uniformly, because of there’s no difference in the formula for weather a variable got a negation symbol right before it.
A set of connective is functionally complete, if any logic function can be expression only by its elements. If any connective in the set can’t be generated by others in the set, it’s called minimal functionally complete set.
For example, The set \(\{\neg, \land, \lor\}\) is functionally complete (because any truth table can be expressed as PDNF) but not minimal, because conjuction and disjuction can expressed each other based on the De Morgan’s Law (with the help with negation): \[ p\land q = \neg(\negp\lor\negq), \quad\quad p\land q = \neg(\negp\land\negq) \] By deleting one of these two, the set \(\{\neg, \land\}\) or \(\{\neg,\lor\}\) is minial functionally complete. This can be proved by further methods.
We noticed that we can’t use only one connective to express all the logic function based on the most basic \(\{\neg, \land, \lor\}\), but it’s possible to use \(\r\), this is demonstrated as followed:
Ex. \(\{\r\}\) is the minimal functionally complete set.
Prov. noticed that \[ p\r(q\r p) = \negp\lor(\negq\lor p) = \neg q \] This shows \(\neg\) can be generated from \(\r\).
What’s more, \[ p\lor q = \neg(\negp)\lor q=\negp\r q \] This shows \(\lor\) can be generated from \(\neg\) and \(\r\). As we proved before, \(\neg\) can be expressed by \(\r\). So \(\lor\) can be expressed by pure \(\r\).
Noticed that \(\{\neg, \lor\}\) is the functionally complete, so \({\r}\) is also functionally complete, and it must be minimal because only one element in this set.
Normal form is a formula form with special character, the most important normal form in proposition formula are Disjunctive Normal Form (DNF) and Conjunction Normal Form (CNF). Because of the similarity, we only emphasize DNF in this part.
Disjunctive normal form are defined as the disjunction of the conjunction of literals.
Ex. \[ A(p,q,r) = (p\land q)\lor(p\land\negq)\lor(\neg p\land q\land r) \] is a DNF expression, the subformula \(p\land q, \ p\land \negq, \ \negp\land q\land r\) are all conjunctions, and \(A\) is the disjunction of them.
If all the variable occurs exactly once in each conjuction in DNF, it’s called Principal DNF (PDNF). The DNF above is not PDNF, but it’s possible to convert it into the PDNF. Actually, any satiable formula can be converted to PDNF by truth table or propositional equivlance calculus. The detalied technique will be describe in PDNF Transformation.
PDNF form play a significant role in the automatic prove like SAT Algorithm.
Def. Let \(A_i, C\) be the proposition formula, if \(\bigwedge A_i\r C\) is tautology, we’ll say that \(A_i\) infers \(C\), notes as
\[ \bigwedge A_i \Rightarrow C \]
OR
\[ \cfrac{A_1,\ A_2,\ ... ,\ A_n}{C} \]
The tautology \(\bigwedge A_i\r C\) is called the formal structure of the inference process.
Based on the definition, to check if an inference is valid, we just need to check whether the formal structure is tautology, but in the most cases it’s not possible, because the predicate will replace the over-simplification concept design - proposition, there’s no method to check if a predicate is tautology.
A group of pre-proved inference rules are given here to help the prove of inference: \[ \begin{align} &\text{Replacement Rule:} &&A = B &&\Rightarrow \quad A\r B \\~\\ &\text{Modus Ponens:} &&p,\ p\r q &&\Rightarrow \quad q \\ &\text{Modus tollens:} &&p\r q,\ \negq &&\Rightarrow \quad \negp \\~\\ &\text{Conjunction Introduction:} &&p,\ q &&\Rightarrow \quad p\land q \\ &\text{Conjunction Elimination:} &&p\land q &&\Rightarrow \quad p \\ &\text{Disjunction Introduction:} &&p &&\Rightarrow \quad p\lor q \\~\\ &\text{hypothetical syllogism:} &&p\r q，q\r r &&\Rightarrow \quad r \\ &\text{Disjunctive syllogism:} &&p\lor q, \negq &&\Rightarrow \quad p \\~\\ &\text{Constructive Diellma:} &&p\lor s,\ p\r q,\ s\r t &&\Rightarrow \quad q\lor t \\ &\text{Distructive Diellma:} &&\negq\lor\neg t,\ p\r q,\ s\r t &&\Rightarrow \quad \negp\lor\neg s \\ \end{align} \]
The proposition logic model the proof process by atomic proposition, which is a
Concept “For any \(x\)” is called Universal Quantifier or Generality Quantifier, notes as \(\any x\).
Concept “Exist \(x\)” is called Existential Quantifier, notes as \(\exists x\).
Term is defined recursively:
Afterwards Predicate Formula is defined as the connection of Term through three ways:
\(\exists x: ax^2+bx+c\)
\[ \begin{align} \text{Quantifer Negation:} \qquad\\ &\neg\any x:B(x) = \exists x: \neg B(x) \\ &\neg\exists x:B(x) = \any x: \neg B(x) \\ \text{Quantifer Exchange:} \qquad\\ &\any x \any y:A(x,y) = \any y\any x:A(x,y) \\ &\exists x \exists y:A(x,y) = \exists y\exists x:A(x,y) \\ \text{Quantifer Elimination:} \qquad\\ &\any xB = B \\ &\exists xB = B \\ \text{Name Replacement:} \qquad\\ &\any x \any y:A(x,y) = \any y\any x:A(x,y) \\ &\exists x \exists y:A(x,y) = \exists y\exists x:A(x,y) \\ \end{align} \]
Like the
Universal/Existential Substitution/Generalization Rule:
Universal Substitution Rule:
For any individual constant \(e\), \(\any x:A(x)\Rightarrow A(e)\).
For any individual variable \(y\), if \(y\) does not occurs in the scope of \(x\), \(\any x: A(y)\Rightarrow A(y)\).
Universal Generalization Rule: \[ B\r A(x) \Rightarrow B\r \any x:A(x) \]
Existential Substitution Rule: \[ \exists x:A(x)\Rightarrow A(e) \] where \(e\) is a new individual constant notation which different from any in original expression.
Existential Generalization Rule:
For any individual constant \(e\), \(A(e)\Rightarrow \exists x:A(x)\).
For any individual variable \(y\), \(A(y)\Rightarrow \exists x:A(x)\).