How can I prove false is not a theorem? 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.)
Let $V(E)$ for a propositional expression $E$ be defined as:


$1$ if every bivalent valuation of $E$ is true
$0$ if any bivalent valuation of $E$ is false


given that $'f'$ valuates to false.  So for example, $V(\ulcorner A \lor (A \to f) \urcorner)$ has 2 valuations:  $\top \lor (\top \to \bot) = \top$ as well as $\bot \lor (\bot \to \bot) = \top$, so its valuation is $1$.

Prove that the valuation of every axiom is $1$ (keep in mind that for example, an instance of AX1 might be $(X \to Y) \to ((M \to N) \to (X \to Y))$, that is the $A$ and $B$ in the axiom are expressions not propositional variables).

Prove that modus ponens preserves positive valuations:  if $A \to B$ and $A$ has positive valuations, then $B$ must have a positive valuation.  Same cavaet, $A$ and $B$ are expressions not propositional variables.

Put that together to make an inductive argument that no provable expression has a valuation of $0$.  Combine that with the valuation of $\ulcorner f \urcorner$.
None of the axioms are f.  So, f could only get deduced by uses of detachment (i. e. modus ponens).
Every detachment of a formula has one of the following forms 1. (B→A) originating from axiom 1.  2. A originating from axiom 1.  3. ((A→B)→(A→C)) originating from axiom 2.  4. (A→C) originating from axiom 2.  5. C originating from axiom 2.  6. A originating from axiom 3.


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.