Properties of maximal $AX$-consistent sets in Epistemic Logic

logicmodal-logicsolution-verification

This post is regarding the proof of Lemma $3.1.2$ in Reasoning about Knowledge, by Fagin, Halpern, Moses, & Vardi.

Lemma: Suppose that the language $\mathcal{L}$ consists of a countable set of formulas and is closed with respect to propositional connectives. In a consistent axiom system $AX$ that includes
every instance of $(A1)$ and $(R1)$ for the language $\mathcal{L}$, every $AX$-consistent set $F \subseteq L$ can be extended to a maximal $AX$-consistent set with respect to $L$. In addition, if $F$ is a maximal $AX$-consistent set, then it satisfies the following properties:

  1. for every formula $\varphi\in\mathcal{L}$, exactly one of $\varphi$ and $\lnot\varphi$ is in $F$,
  2. $\varphi\land\psi\in F$ iff $\varphi\in F$ and $\psi\in F$,
  3. if $\varphi$ and $\varphi\to\psi$ are both in $F$, then $\psi$ is in $F$,
  4. if $\varphi$ is provable in $AX$, then $\varphi\in F$.

For context, here are some definitions (and notation) from previous sections:

(a) $A1$ refers to Axiom $1$ – all tautologies of propositional calculus.
(b) $R1$ refers to Rule $1$ – modus ponens.
(c) An axiom system $AX$ consists of a collection of axioms and inference rules. An axiom is a formula, and an inference rule has the form "from $\varphi_1, \ldots, \varphi_k$ infer $\psi$." where $\varphi_1,\ldots,\varphi_k,\psi$ are formulas of $\mathcal{L}_n$. A proof in $AX$ consists of a sequence of formulas, each of which is either an instance of an axiom in $AX$ or follows by an application of an inference rule. A proof is said to be a proof of the formula $\varphi$ if the last formula in the proof is $\varphi$. We say $\varphi$ is provable in $AX$, and write $AX \vdash \varphi$, if there is a proof of $\varphi$ in $AX$.

I understand the construction and proof of the first part of the lemma, i.e. showing the existence of and constructing a maximally consistent set $F$. I have trouble proving properties 1 to 4, i.e. properties of maximally consistent sets.

Here's what I've tried (please help me fill in the gaps if any):

Suppose $F$ is a maximal $AX$-consistent set.

  1. If $\varphi\in\mathcal{L}$, we show that one of $F\cup \{\varphi\}$ and $F\cup \{\lnot\varphi\}$ is $AX$-consistent. Assume to the contrary that neither of them is $AX$-consistent. Let $\beta$ denote the conjunction of all formulas in $F$, i.e. $\beta = \bigwedge_{\alpha\in F}\alpha$. By definition, $F\cup \{\varphi\}$ and $F\cup \{\lnot\varphi\}$ are not $AX$-consistent means that $AX\vdash \lnot (\beta\land\varphi)$ and $AX\vdash \lnot (\beta\land\lnot\varphi)$ respectively. We can rewrite $AX\vdash \lnot (\beta\land\varphi)$ as $AX\vdash \lnot\beta\lor\lnot\varphi$, and $AX\vdash \lnot (\beta\land\lnot\varphi)$ as $AX\vdash \lnot \beta\lor\varphi$. Consider the following two propositional tautologies:

    $(T1).\quad$ $\vDash ((p \lor q)\land (p\lor \lnot q))\to p$
    $(T2).\quad$ $\vDash p \to (q \to (p\land q))$
    Using uniform substitution in (T2), with $AX\vdash \lnot\beta\lor\lnot\varphi$ and $AX\vdash \lnot \beta\lor\varphi$, we can conclude $AX\vdash (\lnot\beta\lor\lnot\varphi) \land (\lnot \beta\lor\varphi)$. Using uniform substitution in (T1), we get $AX\vdash ((\lnot\beta\lor\lnot\varphi) \land (\lnot \beta\lor\varphi)) \to \lnot\beta$. Due to Modus Ponens, we get $AX\vdash\lnot\beta$ from $AX\vdash ((\lnot\beta\lor\lnot\varphi) \land (\lnot \beta\lor\varphi)) \to \lnot\beta$ and $AX\vdash (\lnot\beta\lor\lnot\varphi) \land (\lnot \beta\lor\varphi)$. $AX\vdash\lnot\beta$ implies that $F$ is not $AX$-consistent (if it were, $\lnot\beta$ would not be provable). This is a contradiction. If $F\cup \{\varphi\}$ is $AX$-consistent, then $\varphi\in F$ since $F$ is a maximal $AX$-consistent set. Similarly, if $F\cup \{\lnot\varphi\}$ is $AX$-consistent, then $\lnot\varphi\in F$ since $F$ is a maximal $AX$-consistent set. So, one of $\varphi$ and $\lnot\varphi$ is in $F$ (we cannot have both, for then $F$ would not be $AX$-consistent).

  2. To show this, we use part (1). Suppose $\varphi\land\psi\in F$. Then we must have $\varphi\in F$, because otherwise we will have $\lnot\varphi\in F$ (due to (1)) and $F$ would not be $AX$-consistent. Similarly we must have $\psi\in F$. For the other direction, suppose $\psi\in F$ and $\varphi\in F$. If $\varphi\land\psi \notin F$, then $\lnot(\varphi\land\psi)\in F$ (due to (1)) and $F$ would not be $AX$-consistent. So, $\varphi\land\psi \in F$.

  3. To show this, we use part (1). Suppose $\varphi\in F$ and $\varphi\to\psi\in F$. If $\psi\notin F$, then $\lnot\psi\in F$ and $F$ would not be $AX$-consistent. So, $\psi\in F$.

  4. Suppose $\varphi$ is provable in $AX$, i.e. $AX\vdash\varphi$. So, $\lnot\varphi$ is not $AX$-consistent. We must have $\varphi\in F$, otherwise $\lnot\varphi\in F$ (due to (1)) which would be a contradiction.

My proof of (1) is pretty detailed (or so I think), but of the remaining parts is comparatively short. I also do not feel as convinced with my proofs of (2), (3), (4) as I do with the proof of (1). Could you please let me know if I'm missing something, and if certain parts can be justified in more detail? Thanks a lot!

Best Answer

Here is my try in the inverted order.

4 Let $\varphi$ be provable. This means that $F \cup \varphi$ is consistent, which implies $\varphi \in F$ by maximality.

3 Let $\varphi, \varphi\rightarrow \psi \in F$. Since $F$ contain all propositional tautologies, $\varphi \rightarrow ((\varphi \rightarrow \psi) \rightarrow \psi) \in F$. From the fact that $F$ is closed under $R1$ we conclude that $(\varphi \rightarrow \psi) \rightarrow \psi \in F$ and, further, $\psi \in F$.

2 Similar reasoning to 2 with $(\varphi \land \psi) \rightarrow \varphi \in F$.

1 Let $\varphi \in F$. Then by consistency we yield $\lnot \varphi \not \in F$. In the other direction, let $\varphi \not \in F$. By maximality this means that $F \cup \{\varphi\}$ is not consistent. By the definition of consistency, this means that $\lnot \varphi$ is provable, and by 4 this implies that $\lnot \varphi \in F$.

Related Question