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\}$.


  • 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$.


Show that $\not\vdash f$.


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.)

  • $\begingroup$ Are you allowed to use soundness : every theorem of the calculus is a tautology ? $\endgroup$ – Mauro ALLEGRANZA Sep 30 '18 at 16:25
  • $\begingroup$ @MauroALLEGRANZA No, I think not because it comes much later in the lecture notes. $\endgroup$ – Smi Sep 30 '18 at 16:31
  • 2
    $\begingroup$ Well, even if you aren't supposed to cite the soundness theorem, the easiest way to prove this might be to first prove the soundness theorem and then use it. $\endgroup$ – Eric Wofsey Sep 30 '18 at 19:06
  • $\begingroup$ Hmm, okay. The proof for the soundness theorem is included in the lecture notes, though, and there's a remark in the lecture notes saying this task "is fairly difficult", so I guess a proof that avoids citing soundness theorem won't be trivial. $\endgroup$ – Smi Sep 30 '18 at 19:41
  • $\begingroup$ If we restore parentheses to the axiom schema, then one can figure out that every theorem starts with '(' and ends with ')'. f doesn't start with '(' or with ')'. That said, if you can't use soundness, I'm not sure how to go about showing that every theorem starts with '(' and ends with ')'. $\endgroup$ – Doug Spoonwood Oct 1 '18 at 5:01

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$.

  • $\begingroup$ I like this, and I think it works, but it basically proves soundness, and assigns a value to 'f'. I have to wonder if another way works better. We don't assign a value to f, and prove consistency. Then, since (f→A) is a theorem, we could deduce A. And that would contradict consistency, since A is a theorem and so is (A→f). The difficulty I have though lies in that I don't know how to prove consistency without proving or assuming soundness. $\endgroup$ – Doug Spoonwood Oct 1 '18 at 21:02
  1. None of the axioms are f. So, f could only get deduced by uses of detachment (i. e. modus ponens).
  2. 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.

  • $\begingroup$ Your statement (2) is wrong. For instance, if the formula $A$ itself is an implication, then you might deduce $A$ via axiom 1, and then deduce the consequent of $A$ from $A$. So, you need to rule out not just any of these formulas being $f$ themselves but also not being any nested sequence of implications whose final consequence is $f$. $\endgroup$ – Eric Wofsey Sep 30 '18 at 19:03
  • $\begingroup$ And in fact you can't rule that out, since (for instance) $f\to(p_1\to f)$ is an axiom whose final consequent is $f$. And there are more complicated formulas too like $p_1\to((p_1\to f)\to f)$ which are theorems and have $f$ as a final consequent. So, I am skeptical that any simple syntactic analysis like this can work. $\endgroup$ – Eric Wofsey Sep 30 '18 at 19:11
  • $\begingroup$ In any case, if you are going to use the fact that the axioms are true for all valuations and that modus ponens is sound, there is of course a much easier proof which is just to observe that $f$ is not true for all valuations. $\endgroup$ – Eric Wofsey Sep 30 '18 at 19:22
  • $\begingroup$ @EricWofsey I think the nested sequence of implications gets covered by cases 2., 4., and 5. "since (for instance) f→(p1→f) is an axiom whose final consequent is f." f is not an instance of axiom, and thus there is no valid way to use the formula (f→(p1→f)) in any detachment. So, (p1→f) cannot get derived, nor can f from that axiom. "(p1→((p1→f)→f))" sure, but so what? p1, effectively being a propositional constant, is not an axiom. So, you can't derive anything from that. $\endgroup$ – Doug Spoonwood Sep 30 '18 at 19:26
  • $\begingroup$ But it is extremely non-obvious that something like that must be the case for every nested sequence of implications ending in $f$ which is a theorem. (For one thing, you have not actually proved that $p_1$ is not a theorem. Of course this follows from soundness, but if you're going to use soundness then the problem itself is immediately trivial.) $\endgroup$ – Eric Wofsey Sep 30 '18 at 19:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.