Definitions
Let our propositional calculus be defined as follows:
Alphabet $D := \{p_i:i\in \mathbb{N}\}$.
Operators $\Omega := \Omega_0 \cup \Omega_2$ where $\Omega_0 := \{f\}$ and $\Omega_2 := \{\rightarrow\}$.
Axioms:
- AX1: $A\rightarrow(B\rightarrow A)$
- AX2: $(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B) \rightarrow (A\rightarrow C))$
- AX3: $((A\rightarrow f)\rightarrow f) \rightarrow A$
where $A$, $B$ and $C$ can be arbitrary formulas.
Modus ponens is the only inference rule. To be precise, a formula $A$ is a theorem (denoted $\vdash A$) if there exists a sequence of formulas $A_1, ..., A_n$ (called an inference sequence) such that $A_n=A$ and for all $i\in \{1,...,n\}$ the following holds:
- $A_i$ is an axiom, or
- there exists $j,k\in \{1,...,i-1\}$ such that $A_k=A_j\rightarrow A_i$.
Word and formula
A word is a nonempty and finite sequence of symbols from the set $D\cup \Omega \cup \{(,)\}$.
A word $A$ is a formula if there exists a finite sequence of words $A_1,...,A_m$ such that $A_m=A$ and for all $i \in \{1,...,m\}$ the following holds:
- $A_i=p_n$ for some $n\in \mathbb{N}$, or
- $A_i=f$, or
- $A_i=(A_j\rightarrow A_k)$ for some $j,k \in \{1,...,i-1\}$.
For brevity, the outermost parentheses can be omitted, so $(A \rightarrow B)$ is the same as $A \rightarrow B$.
Problem
Show that $\not\vdash f$.
Comments
This problem seems difficult because I somehow need to prove there exists no inference sequence that would prove $\vdash f$. Intuitively, it seems that for any inference sequence $A_1,...,A_n$, the formula $A_i$ always contains at least one arrow symbol for all $i\in \{1,...,n\}$, but I cannot figure out how to prove it.
(I believe I'm not supposed to use the soundness or completeness theorems in the proof, as they are introduced much later in the lecture notes.)
I'll note that all of the axioms are sound, in that none of them evaluate to f for any valuation of their variables.
(B→A), ((A→B)→(A→C)), and (A→C) do not have the same form of f. So, it is not possible to derive f such that it has the form indicated by 1., 3., or 4.
Consider the possibility that f has form A originating from axiom 1, or from axiom 3. In the first case, axiom schema 1 gets instantiated as the axiom (f→(B→f)). But, then nothing could get detached, since the axioms are sound. Thus, (B→f) would not be derivable, and neither would f. So, f cannot get derived that way. In the second case, axiom schema 3 gets instantiated as the axiom (((f→f)→f)→f). But, the antecedent of that axiom is ((f→f)→f), which is false. Since the axioms are sound, that does not permit a deduction of f. Thus, both possibilities 2., and 6. consider here cannot derive f.
Finally, we come to the possibility that f got derived having form C from axiom 2. Then axiom schema 2 gets instantiated as an axiom having the form ((A→(B→f))→((A→B)→(A→f))). In order to get to f, since all of the axioms are true, and the deduction rule of modus ponens is sound, it follows that (A→(B→f)), (A→B), and A all hold true. But, if A holds true, and (A→B) holds true, so does B. Then since B is true, (B→f) is false. Since (B→f) is false, and A is true, that would imply (A→(B→f)) as false. But, that is not possible since the axioms are sound.
Having eliminated all possible cases of how f could get deduced according to the definition of a proof, we conclude that f is not provable.