Logical system: proving sentence is not deductible

Question

Note: This is a part of my homework.

I have an formal system L(↑,↓,→) with Modus ponens and following three axioms:

1. ↑↑↓↓φ
2. (↑↓φ → ↑ψ)
3. ((φ→ψ)→(↑ψ→↑φ))

And I need to decide, if it's possible to derive following statements from described formal system:

1. ↑↓A
2. ↓A
3. (↓A → ↓A)

It seems it's impossible. However, I must prove why it's impossible. I don't quite get this part from the lecture. The trick was somehow to redefine the operators (until all of the axioms stays tautology) and then do some magic.

I'll be glad for any advice.

Answer 1

HINT

Try to do this as follows:

1. First, specify a domain of objects that the variables could represent and that the operators work on. For binary logics, the objects would be $T$ and $F$ (or $1$ and $0$), so you could stick with that, but there is nothing against using more than two objects, e.g. using $X$, $Y$, and $Z$, or $1$, $2$, $3$, and $4$. This does not have to be meaningful: it's just some domain of objects.

2. Define $\downarrow$ and $\uparrow$ as unary functions, and $\rightarrow$ as a binary function, over this domain. For example, if your domain is $X$, $Y$, and $Z$, you could define the $\uparrow$ as:

\begin{array}{c|c} A & \uparrow A\\ \hline X & Y\\ Y & Z\\ Z & X\\ \end{array}

again, none of this has to be meaningful ... but you want to try and define the operators in such a way that:

3a. Every expression that has the form of any of the three axioms will always evaluate to the same outcome. For example, maybe you can make it so that any expression $\uparrow \uparrow \downarrow \downarrow A$ evaluates to $X$, no matter what $A$ is, and that the other two axioms also evaluate to $X$, no matter the value of $A$. As such, we can see the axioms as '$X$-necessities': statements that always have the value of $X$

3b. When you use Modus Ponens, i.e. when you go from $A \rightarrow B$ and $A$ to $B$, it is the case that whenever $A \rightarrow B$ and $A$ have the value as identified in 3a, then $B$ will have that same value as well (and therefore: when $A \rightarrow B$ and $A$ are '$X$-necessities', $B$ will have to be a '$X$-necessity' as well)

3c. Finally, show that the statements that you want to prove are not deducible are not $X$-necessities

It will take a bit of trial and error to define the operators in such a way that this all works out. I would first see if you can make it work with just two objects, since adding objects to the domain creates exponentially more work. But there is on guarantee that you can make it work with just two objects, even if the statements are indeed not deducible, and so you may have to go to three or more (or even infinite ...)

But, if you can make everything work out as described above, then that is your proof: since the axioms are all $X$-necessities, and since by using Modus Ponens you can only infer further $X$-necessities from $X$-necessities, anything that is not a $X$-necessity is therefore not deducible in this system.

Answer 2

$\newcommand{\u}{{\uparrow}}\newcommand{\d}{{\downarrow}}$This question has been running through my mind a bit, so here's an attempt to implement Bram28's suggestion. I have not succeeded in giving a semantics for this language that simultaneously shows that none of the three formulas are derivable from the axioms, despite a fair number of tries. I also haven't quite pinned down where the difficulty comes from... perhaps someone else can add their answer in this regard. However, it becomes much easier if we regard the first formula as separate from the second and third.

Let us start with the (relatively) easy: formula 2 and 3. In this case we can take the domain $\{\top, \bot\}$ just like in conventional logic. In this interpretation of our logic, the truth value of a formula is inductively defined as $$ \begin{align*} [\u \phi] &= \top\\ [\d \phi] &= \bot\\ [\phi \to \psi] &= [\psi]. \end{align*} $$ You can easily check that your axioms are satisfied; anything starting with an $\u$ is satisfied, and both the implications resolve to formulas starting with an $\u$ as well. Furthermore, note that modus ponens holds: if $[\phi] = \top$, and $[\phi \to \psi] = \top$, then trivially $[\psi] = \top$ -- that is just the second assumption. However, formulas two and three are not tautologies -- in fact, both evaluate to $\bot$, always.

This leaves the formula $\u\d A$. This one is a bit harder. We use the domain $\{0, 1, 2\}$, where 2 represents "truth", i.e. the axioms should evaluate to 2, the formula $\u\d A$ should not (always) evaluate to 2, and if both $[\phi]$ and $[\phi \to \psi]$ equal 2, then so should $[\psi]$. We choose the following interpretation: $$ \begin{align*} [\u \phi] &= \min([\phi] + 1, 2)\\ [\d \phi] &= 0\\ [\phi \to \psi] &= \begin{cases} 2 &\text{if $[\phi] \leq [\psi]$,}\\ 0 &\text{otherwise.} \end{cases} \end{align*} $$ Now we once again check by hand: the first axiom is satisfied, as any formula that starts with $\u\u$ is a tautology (note that actually you can prove this from the axioms, so this is a necessity). The second axiom is satisfied: $[\u\d\phi] = 1$, and $[\u\psi] \geq 1$, so $[\u\d\phi\to\u\psi] = 2$. Then consider the third axiom: we have $[\phi \to \psi] \in \{0, 2\}$; if it equals zero, the proposition will necessarily evaluate to $2$, so let us consider the case when $[\phi \to \psi] = 2$. Then $[\phi] \leq [\psi]$ by definition, and therefore also $[\u\phi] \leq [\u\psi]$ as the interpretation of $\u$ is monotone. Hence $[\u\phi \to \u\psi] = 2$, and the third axiom also always evaluates to 2.

Finally, modus ponens holds: if $[\phi]$ evaluates to 2, and $[\phi \to \psi]$ evaluates to 2, then $[\phi] \leq [\psi]$ and hence $[\psi]$ evaluates to 2.

However, the first formula in the list never evaluates to 2: in fact, it always evaluates to 1.

Note that in the first interpretation, the first formula does hold; and in the second interpretation, the final formula does not hold. Purely based on experimentation I feel that the two approaches are not commensurable, and would not be surprised if the smallest domain that shows all three formulas underivable has at least 4 elements.